From 505b9011424ff74ab9058e52367aa84cfe10663d Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 30 May 2023 18:18:50 +0000
Subject: [PATCH] Restore AIG support

This reverts commit 0efb169b74c699c5978aa92006b9cb1387bfc901. Still
requires creating a more modern form of the code removed in
4691a716fcd1e69e942eb13ee137123e43e6419b to actually create a solver
(plus corresponding command-line options).
---
 src/solvers/Makefile          |   4 +-
 src/solvers/prop/aig.cpp      | 183 +++++++++++
 src/solvers/prop/aig.h        | 157 +++++++++
 src/solvers/prop/aig_prop.cpp | 598 ++++++++++++++++++++++++++++++++++
 src/solvers/prop/aig_prop.h   | 133 ++++++++
 5 files changed, 1073 insertions(+), 2 deletions(-)
 create mode 100644 src/solvers/prop/aig.cpp
 create mode 100644 src/solvers/prop/aig.h
 create mode 100644 src/solvers/prop/aig_prop.cpp
 create mode 100644 src/solvers/prop/aig_prop.h

diff --git a/src/solvers/Makefile b/src/solvers/Makefile
index e2d0662981d..495e771e6eb 100644
--- a/src/solvers/Makefile
+++ b/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 \
diff --git a/src/solvers/prop/aig.cpp b/src/solvers/prop/aig.cpp
new file mode 100644
index 00000000000..a164b379db0
--- /dev/null
+++ b/src/solvers/prop/aig.cpp
@@ -0,0 +1,183 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#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;
+}
diff --git a/src/solvers/prop/aig.h b/src/solvers/prop/aig.h
new file mode 100644
index 00000000000..373216557a5
--- /dev/null
+++ b/src/solvers/prop/aig.h
@@ -0,0 +1,157 @@
+/*******************************************************************\
+
+Module: AND-Inverter Graph
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+/// \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
diff --git a/src/solvers/prop/aig_prop.cpp b/src/solvers/prop/aig_prop.cpp
new file mode 100644
index 00000000000..9b8e90427e4
--- /dev/null
+++ b/src/solvers/prop/aig_prop.cpp
@@ -0,0 +1,598 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#include "aig_prop.h"
+
+#include <set>
+#include <stack>
+
+// Tries to compact AIGs corresponding to xor and equality
+// Needed to match the performance of the native CNF back-end.
+#define USE_AIG_COMPACT
+
+// Use the Plaisted-Greenbaum encoding, again, needed to match the
+// native CNF back-end.
+#define USE_PG
+
+literalt aig_prop_baset::land(const bvt &bv)
+{
+  literalt literal=const_literal(true);
+
+  // Introduces N-1 extra nodes for N bits
+  // See convert_node for where this overhead is removed
+  forall_literals(it, bv)
+    literal=land(*it, literal);
+
+  return literal;
+}
+
+literalt aig_prop_baset::lor(const bvt &bv)
+{
+  literalt literal=const_literal(true);
+
+  // Introduces N-1 extra nodes for N bits
+  // See convert_node for where this overhead is removed
+  forall_literals(it, bv)
+    literal=land(neg(*it), literal);
+
+  return neg(literal);
+}
+
+literalt aig_prop_baset::lxor(const bvt &bv)
+{
+  literalt literal=const_literal(false);
+
+  forall_literals(it, bv)
+    literal=lxor(*it, literal);
+
+  return literal;
+}
+
+literalt aig_prop_baset::land(literalt a, literalt b)
+{
+  if(a.is_true() || b.is_false())
+    return b;
+  if(b.is_true() || a.is_false())
+    return a;
+
+  if(a==neg(b))
+    return const_literal(false);
+  if(a==b)
+    return a;
+
+  return dest.new_and_node(a, b);
+}
+
+literalt aig_prop_baset::lor(literalt a, literalt b)
+{
+  return neg(land(neg(a), neg(b))); // De Morgan's
+}
+
+literalt aig_prop_baset::lxor(literalt a, literalt b)
+{
+  if(a.is_false())
+    return b;
+  if(b.is_false())
+    return a;
+  if(a.is_true())
+    return neg(b);
+  if(b.is_true())
+    return neg(a);
+
+  if(a==b)
+    return const_literal(false);
+  if(a==neg(b))
+    return const_literal(true);
+
+  // This produces up to three nodes!
+  // See convert_node for where this overhead is removed
+  return lor(land(a, neg(b)), land(neg(a), b));
+}
+
+literalt aig_prop_baset::lnand(literalt a, literalt b)
+{
+  return !land(a, b);
+}
+
+literalt aig_prop_baset::lnor(literalt a, literalt b)
+{
+  return !lor(a, b);
+}
+
+literalt aig_prop_baset::lequal(literalt a, literalt b)
+{
+  return !lxor(a, b);
+}
+
+literalt aig_prop_baset::limplies(literalt a, literalt b)
+{
+  return lor(neg(a), b);
+}
+
+literalt aig_prop_baset::lselect(literalt a, literalt b, literalt c)
+{  // a?b:c=(a AND b) OR (/a AND c)
+  if(a.is_true())
+    return b;
+  if(a.is_false())
+    return c;
+  if(b==c)
+    return b;
+
+  // This produces unnecessary clauses and variables
+  // See convert_node for where this overhead is removed
+
+  return lor(land(a, b), land(neg(a), c));
+}
+
+void aig_prop_baset::set_equal(literalt a, literalt b)
+{
+#ifdef USE_AIG_COMPACT
+  // The compact encoding should reduce this
+  l_set_to_true(lequal(a, b));
+
+#else
+  // we produce two constraints:
+  // a|!b   !a|b
+
+  l_set_to_true(lor(pos(a), neg(b)));
+  l_set_to_true(lor(neg(a), pos(b)));
+#endif
+}
+
+tvt aig_prop_solvert::l_get(literalt a) const
+{
+  return solver.l_get(a);
+}
+
+propt::resultt aig_prop_solvert::prop_solve()
+{
+  status() << "converting AIG, "
+           << aig.nodes.size() << " nodes" << eom;
+  convert_aig();
+
+  return solver.prop_solve();
+}
+
+/// Compute the phase information needed for Plaisted-Greenbaum encoding
+/// \par parameters: Two vectors of bools of size aig.nodes.size()
+/// \return These vectors filled in with per node phase information
+void aig_prop_solvert::compute_phase(
+  std::vector<bool> &n_pos,
+  std::vector<bool> &n_neg)
+{
+  std::stack<literalt> queue;
+
+  // Get phases of constraints
+  for(aig_plus_constraintst::constraintst::const_iterator
+      c_it=aig.constraints.begin();
+      c_it!=aig.constraints.end();
+      c_it++)
+    queue.push(*c_it);
+
+  while(!queue.empty())
+  {
+    literalt l=queue.top();
+    queue.pop();
+
+    if(l.is_constant())
+      continue;
+
+    bool sign=l.sign();
+    unsigned var_no=l.var_no();
+
+    // already set?
+    if(sign?n_neg[var_no]:n_pos[var_no])
+      continue; // done already
+
+    // set
+    sign?n_neg[var_no]=1:n_pos[var_no]=1;
+
+    const aigt::nodet &node=aig.nodes[var_no];
+
+    if(node.is_and())
+    {
+      queue.push(node.a^sign);
+      queue.push(node.b^sign);
+    }
+  }
+
+  // Count
+  unsigned pos_only=0, neg_only=0, mixed=0;
+
+  for(unsigned n=0; n<aig.nodes.size(); n++)
+  {
+    if(aig.nodes[n].is_and())
+    {
+      if(n_neg[n] && n_pos[n])
+        mixed++;
+      else if(n_pos[n])
+        pos_only++;
+      else if(n_neg[n])
+        neg_only++;
+    }
+  }
+
+  statistics() << "Pos only: " << pos_only << "\n"
+               << "Neg only: " << neg_only << "\n"
+               << "Mixed: " << mixed << eom;
+}
+
+
+/// Compact encoding for single usage variable
+/// \par parameters: Two vectors of unsigned of size aig.nodes.size()
+/// \return These vectors filled in with per node usage information
+void aig_prop_solvert::usage_count(
+  std::vector<unsigned> &p_usage_count,
+  std::vector<unsigned> &n_usage_count)
+{
+  for(aig_plus_constraintst::constraintst::const_iterator
+      c_it=aig.constraints.begin();
+      c_it!=aig.constraints.end();
+      c_it++)
+  {
+    if(!((*c_it).is_constant()))
+    {
+      if((*c_it).sign())
+      {
+        ++n_usage_count[(*c_it).var_no()];
+      }
+      else
+      {
+        ++p_usage_count[(*c_it).var_no()];
+      }
+    }
+  }
+
+  for(unsigned n=0; n<aig.nodes.size(); n++)
+  {
+    const aigt::nodet &node=aig.nodes[n];
+
+    if(node.is_and())
+    {
+      if(node.a.sign())
+      {
+        ++n_usage_count[node.a.var_no()];
+      }
+      else
+      {
+        ++p_usage_count[node.a.var_no()];
+      }
+
+      if(node.b.sign())
+      {
+        ++n_usage_count[node.b.var_no()];
+      }
+      else
+      {
+        ++p_usage_count[node.b.var_no()];
+      }
+    }
+  }
+
+
+  #if 1
+  // Compute stats
+  unsigned unused=0;
+  unsigned usedOncePositive=0;
+  unsigned usedOnceNegative=0;
+  unsigned usedTwicePositive=0;
+  unsigned usedTwiceNegative=0;
+  unsigned usedTwiceMixed=0;
+  unsigned usedThreeTimes=0;
+  unsigned usedMore=0;
+
+  for(unsigned n=0; n<aig.nodes.size(); n++)
+  {
+    switch(p_usage_count[n] + n_usage_count[n])
+    {
+    case 0: ++unused; break;
+    case 1:
+      if(p_usage_count[n]==1)
+        ++usedOncePositive;
+      else
+        ++usedOnceNegative;
+      break;
+
+    case 2 :
+      if(p_usage_count[n]>=2)
+      {
+        ++usedTwicePositive;
+      }
+      else if(n_usage_count[n]>=2)
+      {
+        ++usedTwiceNegative;
+      }
+      else
+      {
+        assert(p_usage_count[n]==1 && n_usage_count[n]==1);
+        ++usedTwiceMixed;
+      }
+      break;
+    case 3: ++usedThreeTimes; break;
+    default: ++usedMore; break;
+    }
+  }
+
+  statistics() << "Unused: " << unused << " "
+               << "Used once: " << usedOncePositive + usedOnceNegative
+               << " (P: " << usedOncePositive
+               << ", N: " << usedOnceNegative << ") "
+               << "Used twice: "
+               << usedTwicePositive + usedTwiceNegative + usedTwiceMixed
+               << " (P: " << usedTwicePositive
+               << ", N: " << usedTwiceNegative
+               << ", M: " << usedTwiceMixed << ") "
+               << "Used three times: " << usedThreeTimes << " "
+               << "Used more: " << usedMore
+               << eom;
+  #endif
+}
+
+/// Convert one AIG node, including special handling of a couple of cases
+/// \par parameters: The node to convert, the phases required and the usage
+///   counts.
+/// \return The node converted to CNF in the solver object.
+void aig_prop_solvert::convert_node(
+  unsigned n,
+  const aigt::nodet &node,
+  bool n_pos, bool n_neg,
+  std::vector<unsigned> &p_usage_count,
+  std::vector<unsigned> &n_usage_count)
+{
+  if(p_usage_count[n]>0 || n_usage_count[n]>0)
+  {
+    literalt o=literalt(n, false);
+    bvt body(2);
+    body[0]=node.a;
+    body[1]=node.b;
+
+#ifdef USE_AIG_COMPACT
+    // Inline positive literals
+    // This should remove the overhead introduced by land and lor for bvt
+
+    for(bvt::size_type i=0; i < body.size(); i++)
+    {
+      literalt l=body[i];
+
+      if(!l.sign() &&                      // Used positively...
+         aig.nodes[l.var_no()].is_and() && // ... is a gate ...
+         p_usage_count[l.var_no()] == 1 && // ... only used here.
+         n_usage_count[l.var_no()] == 0)
+      {
+        const aigt::nodet &rep=aig.nodes[l.var_no()];
+        body[i]=rep.a;
+        body.push_back(rep.b);
+        --i;                         // Repeat the process
+        --p_usage_count[l.var_no()]; // Supress generation of inlined node
+      }
+    }
+
+    // TODO : Could check the array for duplicates / complementary literals
+    // but this should be found by the SAT preprocessor.
+    // TODO : Likewise could find things that are constrained, esp the output
+    // and backwards constant propagate.  Again may not be worth it.
+
+    // lxor and lselect et al. are difficult to express in AIGs.
+    // Doing so introduces quite a bit of overhead.
+    // This should recognise the AIGs they produce and
+    // handle them in a more efficient way.
+
+    // Recognise something of the form:
+    //
+    //  neg(o)=lor(land(a,b), land(neg(a),c))
+    //      o =land(lneg(land(a,b)), lneg(land(neg(a),c)))
+    //
+    // Note that lxor and lselect generate the negation of this
+    // but will still be recognised because the negation is
+    // recorded where it is used
+
+    if(body.size() == 2 && body[0].sign() && body[1].sign())
+    {
+      const aigt::nodet &left=aig.nodes[body[0].var_no()];
+      const aigt::nodet &right=aig.nodes[body[1].var_no()];
+
+      if(left.is_and() && right.is_and())
+      {
+        if(left.a==neg(right.a))
+        {
+          if(p_usage_count[body[0].var_no()]==0 &&
+             n_usage_count[body[0].var_no()]==1 &&
+             p_usage_count[body[1].var_no()]==0 &&
+             n_usage_count[body[1].var_no()]==1)
+          {
+            bvt lits(3);
+
+            if(n_neg)
+            {
+              lits[0]=left.a;
+              lits[1]=right.b;
+              lits[2]=o;
+              solver.lcnf(lits);
+
+              lits[0]=neg(left.a);
+              lits[1]=left.b;
+              lits[2]=o;
+              solver.lcnf(lits);
+            }
+
+            if(n_pos)
+            {
+              lits[0]=left.a;
+              lits[1]=neg(right.b);
+              lits[2]=neg(o);
+              solver.lcnf(lits);
+
+              lits[0]=neg(left.a);
+              lits[1]=neg(left.b);
+              lits[2]=neg(o);
+              solver.lcnf(lits);
+            }
+
+            // Supress generation
+            --n_usage_count[body[0].var_no()];
+            --n_usage_count[body[1].var_no()];
+
+            return;
+          }
+        }
+      }
+    }
+
+
+    // Likewise, carry has an improved encoding which is generated
+    // by the CNF encoding
+    if(body.size() == 3 && body[0].sign() && body[1].sign() && body[2].sign())
+    {
+      const aigt::nodet &left=aig.nodes[body[0].var_no()];
+      const aigt::nodet &mid=aig.nodes[body[1].var_no()];
+      const aigt::nodet &right=aig.nodes[body[2].var_no()];
+
+      if(left.is_and() && mid.is_and() && right.is_and())
+      {
+        if(p_usage_count[body[0].var_no()]==0 &&
+           n_usage_count[body[0].var_no()]==1 &&
+           p_usage_count[body[1].var_no()]==0 &&
+           n_usage_count[body[1].var_no()]==1 &&
+           p_usage_count[body[2].var_no()]==0 &&
+           n_usage_count[body[2].var_no()]==1)
+        {
+          literalt a=left.a;
+          literalt b=left.b;
+          literalt c=mid.a;
+
+          if(a==right.b && b==mid.b && c==right.a)
+          {
+            // A (negative) carry -- 1 if at most one input is 1
+            bvt lits(3);
+
+            if(n_neg)
+            {
+              lits[0]=a;
+              lits[1]=b;
+              lits[2]=o;
+              solver.lcnf(lits);
+
+              lits[0]=a;
+              lits[1]=c;
+              lits[2]=o;
+              solver.lcnf(lits);
+
+              lits[0]=b;
+              lits[1]=c;
+              lits[2]=o;
+              solver.lcnf(lits);
+            }
+
+            if(n_pos)
+            {
+              lits[0]=neg(a);
+              lits[1]=neg(b);
+              lits[2]=neg(o);
+              solver.lcnf(lits);
+
+              lits[0]=neg(a);
+              lits[1]=neg(c);
+              lits[2]=neg(o);
+              solver.lcnf(lits);
+
+              lits[0]=neg(b);
+              lits[1]=neg(c);
+              lits[2]=neg(o);
+              solver.lcnf(lits);
+            }
+
+            // Supress generation
+            --n_usage_count[body[0].var_no()];
+            --n_usage_count[body[1].var_no()];
+            --n_usage_count[body[2].var_no()];
+
+            return;
+          }
+        }
+      }
+    }
+
+    // TODO : these special cases are fragile and could be improved.
+    // They don't handle cases where the construction is partially constant
+    // folded.  Also the usage constraints are sufficient for improvement
+    // but reductions may still be possible with looser restrictions.
+#endif
+
+    if(n_pos)
+    {
+      bvt lits(2);
+      lits[1]=neg(o);
+
+      forall_literals(it, body)
+      {
+        lits[0]=pos(*it);
+        solver.lcnf(lits);
+      }
+    }
+
+    if(n_neg)
+    {
+      bvt lits;
+
+      forall_literals(it, body)
+        lits.push_back(neg(*it));
+
+      lits.push_back(pos(o));
+      solver.lcnf(lits);
+    }
+  }
+}
+
+void aig_prop_solvert::convert_aig()
+{
+  // 1. Do variables
+  while(solver.no_variables()<=aig.nodes.size())
+    solver.new_variable();
+
+  // Usage count for inlining
+
+  std::vector<unsigned> p_usage_count;
+  std::vector<unsigned> n_usage_count;
+  p_usage_count.resize(aig.nodes.size(), 0);
+  n_usage_count.resize(aig.nodes.size(), 0);
+
+  this->usage_count(p_usage_count, n_usage_count);
+
+
+  #ifdef USE_PG
+  // Get phases
+  std::vector<bool> n_pos, n_neg;
+  n_pos.resize(aig.nodes.size(), false);
+  n_neg.resize(aig.nodes.size(), false);
+
+  this->compute_phase(n_pos, n_neg);
+  #endif
+
+  // 2. Do nodes
+  for(std::size_t n=aig.nodes.size() - 1; n!=0; n--)
+  {
+    if(aig.nodes[n].is_and())
+    {
+#ifdef USE_PG
+      convert_node(
+        n, aig.nodes[n], n_pos[n], n_neg[n], p_usage_count, n_usage_count);
+#else
+      convert_node(n, aig.nodes[n], true, true, p_usage_count, n_usage_count);
+#endif
+    }
+  }
+  // Skip zero as it is not used or a valid literal
+
+
+  // 3. Do constraints
+  for(const auto &c_it : aig.constraints)
+    solver.l_set_to(c_it, true);
+
+  // HACK!
+  aig.nodes.clear();
+}
diff --git a/src/solvers/prop/aig_prop.h b/src/solvers/prop/aig_prop.h
new file mode 100644
index 00000000000..335f224747c
--- /dev/null
+++ b/src/solvers/prop/aig_prop.h
@@ -0,0 +1,133 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+
+#ifndef CPROVER_SOLVERS_PROP_AIG_PROP_H
+#define CPROVER_SOLVERS_PROP_AIG_PROP_H
+
+#include <cassert>
+
+#include <util/threeval.h>
+#include <solvers/prop/prop.h>
+
+#include "aig.h"
+
+class aig_prop_baset:public propt
+{
+public:
+  explicit aig_prop_baset(aigt &_dest):dest(_dest)
+  {
+  }
+
+  bool has_set_to() const override { return false; }
+  bool cnf_handled_well() const override { return false; }
+
+  literalt land(literalt a, literalt b) override;
+  literalt lor(literalt a, literalt b) override;
+  literalt land(const bvt &bv) override;
+  literalt lor(const bvt &bv) override;
+  void lcnf(const bvt &clause) override { assert(false); }
+  literalt lxor(literalt a, literalt b) override;
+  literalt lxor(const bvt &bv) override;
+  literalt lnand(literalt a, literalt b) override;
+  literalt lnor(literalt a, literalt b) override;
+  literalt lequal(literalt a, literalt b) override;
+  literalt limplies(literalt a, literalt b) override;
+  literalt lselect(literalt a, literalt b, literalt c) override; // a?b:c
+  void set_equal(literalt a, literalt b) override;
+
+  void l_set_to(literalt a, bool value) override { assert(false); }
+
+  literalt new_variable() override
+  {
+    return dest.new_node();
+  }
+
+  size_t no_variables() const override
+  { return dest.number_of_nodes(); }
+
+  const std::string solver_text() override
+  { return "conversion into and-inverter graph"; }
+
+  tvt l_get(literalt a) const override
+  { assert(0); return tvt::unknown(); }
+
+  resultt prop_solve() override
+  { assert(0); return resultt::P_ERROR; }
+
+protected:
+  aigt &dest;
+};
+
+class aig_prop_constraintt:public aig_prop_baset
+{
+public:
+  explicit aig_prop_constraintt(aig_plus_constraintst &_dest):
+    aig_prop_baset(_dest),
+    dest(_dest)
+  {
+  }
+
+  aig_plus_constraintst &dest;
+  bool has_set_to() const override { return true; }
+
+  void lcnf(const bvt &clause) override
+  {
+    l_set_to_true(lor(clause));
+  }
+
+  void l_set_to(literalt a, bool value) override
+  {
+    dest.constraints.push_back(a^!value);
+  }
+};
+
+class aig_prop_solvert:public aig_prop_constraintt
+{
+public:
+  explicit aig_prop_solvert(propt &_solver):
+    aig_prop_constraintt(aig),
+    solver(_solver)
+  {
+  }
+
+  aig_plus_constraintst aig;
+
+  const std::string solver_text() override
+  {
+    return
+      "conversion into and-inverter graph followed by "+
+      solver.solver_text();
+  }
+
+  tvt l_get(literalt a) const override;
+  resultt prop_solve() override;
+
+  void set_message_handler(message_handlert &m) override
+  {
+    aig_prop_constraintt::set_message_handler(m);
+    solver.set_message_handler(m);
+  }
+
+protected:
+  propt &solver;
+
+  void convert_aig();
+  void usage_count(
+    std::vector<unsigned> &p_usage_count, std::vector<unsigned> &n_usage_count);
+  void compute_phase(std::vector<bool> &n_pos, std::vector<bool> &n_neg);
+  void convert_node(
+    unsigned n,
+    const aigt::nodet &node,
+    bool n_pos,
+    bool n_neg,
+    std::vector<unsigned> &p_usage_count,
+    std::vector<unsigned> &n_usage_count);
+};
+
+#endif // CPROVER_SOLVERS_PROP_AIG_PROP_H