Restore AIG support

src/solvers/Makefile

@@ -141,8 +141,8 @@ SRC = $(BOOLEFORCE_SRC) \
       floatbv/float_bv.cpp \
       floatbv/float_utils.cpp \
       floatbv/float_approximation.cpp \
-      lowering/functions.cpp \
-      bdd/miniBDD/miniBDD.cpp \
+      prop/aig.cpp \
+      prop/aig_prop.cpp \
       prop/bdd_expr.cpp \
       prop/cover_goals.cpp \
       prop/literal.cpp \

src/solvers/prop/aig.cpp

@@ -0,0 +1,183 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include "aig.h"
+
+#include <cassert>
+#include <ostream>
+#include <string>
+
+std::string aigt::label(nodest::size_type v) const
+{
+  return "var("+std::to_string(v)+")";
+}
+
+std::string aigt::dot_label(nodest::size_type v) const
+{
+  return "var("+std::to_string(v)+")";
+}
+
+void aigt::get_terminals(terminalst &terminals) const
+{
+  for(nodest::size_type n=0; n<nodes.size(); n++)
+    get_terminals_rec(n, terminals);
+}
+
+const aigt::terminal_sett &aigt::get_terminals_rec(
+  literalt::var_not n,
+  terminalst &terminals) const
+{
+  terminalst::iterator it=terminals.find(n);
+
+  if(it!=terminals.end())
+    return it->second; // already done
+
+  assert(n<nodes.size());
+  const aig_nodet &node=nodes[n];
+
+  terminal_sett &t=terminals[n];
+
+  if(node.is_and())
+  {
+    if(!node.a.is_constant())
+    {
+      const std::set<literalt::var_not> &ta=
+        get_terminals_rec(node.a.var_no(), terminals);
+      t.insert(ta.begin(), ta.end());
+    }
+
+    if(!node.b.is_constant())
+    {
+      const std::set<literalt::var_not> &tb=
+        get_terminals_rec(node.b.var_no(), terminals);
+      t.insert(tb.begin(), tb.end());
+    }
+  }
+  else // this is a terminal
+  {
+    t.insert(n);
+  }
+
+  return t;
+}
+
+void aigt::print(
+  std::ostream &out,
+  literalt a) const
+{
+  if(a==const_literal(false))
+  {
+    out << "FALSE";
+    return;
+  }
+  else if(a==const_literal(true))
+  {
+    out << "TRUE";
+    return;
+  }
+
+  literalt::var_not node_nr=a.var_no();
+
+  {
+    const aig_nodet &node=nodes[node_nr];
+
+    if(node.is_and())
+    {
+      if(a.sign())
+        out << "!(";
+      print(out, node.a);
+      out << " & ";
+      print(out, node.b);
+      if(a.sign())
+        out << ")";
+    }
+    else if(node.is_var())
+    {
+      if(a.sign())
+        out << "!";
+      out << label(node_nr);\
+    }
+    else
+    {
+      if(a.sign())
+        out << "!";
+      out << "unknown(" << node_nr << ")";
+    }
+  }
+}
+
+void aigt::output_dot_node(
+  std::ostream &out,
+  nodest::size_type v) const
+{
+  const aig_nodet &node=nodes[v];
+
+  if(node.is_and())
+  {
+    out << v << " [label=\"" << v << "\"]" << "\n";
+    output_dot_edge(out, v, node.a);
+    output_dot_edge(out, v, node.b);
+  }
+  else // the node is a terminal
+  {
+    out << v << " [label=\"" << dot_label(v) << "\""
+        << ",shape=box]" << "\n";
+  }
+}
+
+void aigt::output_dot_edge(
+  std::ostream &out,
+  nodest::size_type v,
+  literalt l) const
+{
+  if(l.is_true())
+  {
+    out << "TRUE -> " << v;
+  }
+  else if(l.is_false())
+  {
+    out << "TRUE -> " << v;
+    out << " [arrowhead=odiamond]";
+  }
+  else
+  {
+    out << l.var_no() << " -> " << v;
+    if(l.sign())
+      out << " [arrowhead=odiamond]";
+  }
+
+  out << "\n";
+}
+
+void aigt::output_dot(std::ostream &out) const
+{
+  // constant TRUE
+  out << "TRUE [label=\"TRUE\", shape=box]" << "\n";
+
+  // now the nodes
+  for(nodest::size_type n=0; n<number_of_nodes(); n++)
+    output_dot_node(out, n);
+}
+
+void aigt::print(std::ostream &out) const
+{
+  for(nodest::size_type n=0; n<number_of_nodes(); n++)
+  {
+    out << "n" << n << " = ";
+    literalt l;
+    l.set(n, false);
+    print(out, l);
+    out << "\n";
+  }
+}
+
+std::ostream &operator << (std::ostream &out, const aigt &aig)
+{
+  aig.print(out);
+  return out;
+}

src/solvers/prop/aig.h

@@ -0,0 +1,157 @@
+/*******************************************************************\
+
+Module: AND-Inverter Graph
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// AND-Inverter Graph
+
+#ifndef CPROVER_SOLVERS_PROP_AIG_H
+#define CPROVER_SOLVERS_PROP_AIG_H
+
+#include <vector>
+#include <set>
+#include <map>
+
+#include <solvers/prop/literal.h>
+
+class aig_nodet
+{
+public:
+  literalt a, b;
+
+  aig_nodet()
+  {
+  }
+
+  bool is_and() const
+  {
+    return a.var_no()!=literalt::unused_var_no();
+  }
+
+  bool is_var() const
+  {
+    return a.var_no()==literalt::unused_var_no();
+  }
+
+  void make_and(literalt _a, literalt _b)
+  {
+    a=_a;
+    b=_b;
+  }
+
+  void make_var()
+  {
+    a.set(literalt::unused_var_no(), false);
+  }
+};
+
+class aigt
+{
+public:
+  aigt()
+  {
+  }
+
+  ~aigt()
+  {
+  }
+
+  typedef aig_nodet nodet;
+  typedef std::vector<nodet> nodest;
+  nodest nodes;
+
+  void clear()
+  {
+    nodes.clear();
+  }
+
+  typedef std::set<literalt::var_not> terminal_sett;
+  typedef std::map<literalt::var_not, terminal_sett> terminalst;
+
+  // produces the support set
+  // should get re-written
+  void get_terminals(terminalst &terminals) const;
+
+  const aig_nodet &get_node(literalt l) const
+  {
+    return nodes[l.var_no()];
+  }
+
+  aig_nodet &get_node(literalt l)
+  {
+    return nodes[l.var_no()];
+  }
+
+  nodest::size_type number_of_nodes() const
+  {
+    return nodes.size();
+  }
+
+  void swap(aigt &g)
+  {
+    nodes.swap(g.nodes);
+  }
+
+  literalt new_node()
+  {
+    nodes.push_back(aig_nodet());
+    literalt l;
+    l.set(nodes.size()-1, false);
+    return l;
+  }
+
+  literalt new_var_node()
+  {
+    literalt l=new_node();
+    nodes.back().make_var();
+    return l;
+  }
+
+  literalt new_and_node(literalt a, literalt b)
+  {
+    literalt l=new_node();
+    nodes.back().make_and(a, b);
+    return l;
+  }
+
+  bool empty() const
+  {
+    return nodes.empty();
+  }
+
+  void print(std::ostream &out) const;
+  void print(std::ostream &out, literalt a) const;
+  void output_dot_node(std::ostream &out, nodest::size_type v) const;
+  void output_dot_edge(
+    std::ostream &out, nodest::size_type v, literalt l) const;
+  void output_dot(std::ostream &out) const;
+
+  std::string label(nodest::size_type v) const;
+  std::string dot_label(nodest::size_type v) const;
+
+protected:
+  const std::set<literalt::var_not> &get_terminals_rec(
+    literalt::var_not n,
+    terminalst &terminals) const;
+};
+
+std::ostream &operator << (std::ostream &, const aigt &);
+
+class aig_plus_constraintst:public aigt
+{
+public:
+  typedef std::vector<literalt> constraintst;
+  constraintst constraints;
+
+  void clear()
+  {
+    aigt::clear();
+    constraints.clear();
+  }
+};
+
+#endif // CPROVER_SOLVERS_PROP_AIG_H