Add solver for integer AND (#4681)

This omits certain inference schemas (sum and bitwise lemmas) which depends on an option that will be added later.

6 files changed, 435 insertions, 3 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 0774d60af..5cddccc58 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -300,6 +300,8 @@ libcvc4_add_sources(
   theory/arith/linear_equality.h
   theory/arith/matrix.cpp
   theory/arith/matrix.h
+  theory/arith/nl/iand_solver.cpp
+  theory/arith/nl/iand_solver.h
   theory/arith/nl/nl_constraint.cpp
   theory/arith/nl/nl_constraint.h
   theory/arith/nl/nl_lemma_utils.cpp
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index c104cb3e7..c09f8bbf3 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -651,6 +651,25 @@ header = "options/smt_options.h"
   help       = "attempt to solve BV formulas by translation to integer arithmetic (experimental)"
 
 [[option]]
+  name       = "iandMode"
+  category   = "undocumented"
+  long       = "iand-mode=mode"
+  type       = "IandMode"
+  default    = "VALUE"
+  read_only  = true
+  help       = "Set the refinement scheme for integer AND"
+  help_mode  = "Refinement modes for integer AND"
+  [[option.mode.VALUE]]
+  name = "value"
+  help = "value-based refinement"
+  [[option.mode.SUM]]
+  name = "sum"
+  help = "use sum to represent integer AND in refinement"
+  [[option.mode.BITWISE]]
+  name = "bitwise"
+  help = "use bitwise comparisons on binary representation of integer for refinement (experimental)"
+  
+[[option]]
   name       = "solveIntAsBV"
   category   = "undocumented"
   long       = "solve-int-as-bv=N"
diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp
new file mode 100644
index 000000000..fd6eedc5a
--- /dev/null
+++ b/src/theory/arith/nl/iand_solver.cpp
@@ -0,0 +1,258 @@
+/*********************                                                        */
+/*! \file iand_solver.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of integer and (IAND) solver
+ **/
+
+#include "theory/arith/nl/iand_solver.h"
+
+#include "options/arith_options.h"
+#include "options/smt_options.h"
+#include "preprocessing/passes/bv_to_int.h"
+#include "theory/arith/arith_msum.h"
+#include "theory/arith/arith_utilities.h"
+#include "util/iand.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+namespace nl {
+
+IAndSolver::IAndSolver(TheoryArith& containing, NlModel& model)
+    : d_containing(containing),
+      d_model(model),
+      d_initRefine(containing.getUserContext())
+{
+  NodeManager* nm = NodeManager::currentNM();
+  d_true = nm->mkConst(true);
+  d_false = nm->mkConst(false);
+  d_zero = nm->mkConst(Rational(0));
+  d_one = nm->mkConst(Rational(1));
+  d_two = nm->mkConst(Rational(2));
+  d_neg_one = nm->mkConst(Rational(-1));
+}
+
+IAndSolver::~IAndSolver() {}
+
+void IAndSolver::initLastCall(const std::vector<Node>& assertions,
+                              const std::vector<Node>& false_asserts,
+                              const std::vector<Node>& xts)
+{
+  d_iands.clear();
+
+  Trace("iand-mv") << "IAND terms : " << std::endl;
+  for (const Node& a : xts)
+  {
+    Kind ak = a.getKind();
+    if (ak != IAND)
+    {
+      // don't care about other terms
+      continue;
+    }
+    size_t bsize = a.getOperator().getConst<IntAnd>().d_size;
+    d_iands[bsize].push_back(a);
+  }
+
+  Trace("iand") << "We have " << d_iands.size() << " IAND terms." << std::endl;
+}
+
+std::vector<NlLemma> IAndSolver::checkInitialRefine()
+{
+  Trace("iand-check") << "IAndSolver::checkInitialRefine" << std::endl;
+  std::vector<NlLemma> lems;
+  NodeManager* nm = NodeManager::currentNM();
+  for (const std::pair<const unsigned, std::vector<Node> >& is : d_iands)
+  {
+    // the reference bitwidth
+    unsigned k = is.first;
+    for (const Node& i : is.second)
+    {
+      if (d_initRefine.find(i) != d_initRefine.end())
+      {
+        // already sent initial axioms for i in this user context
+        continue;
+      }
+      d_initRefine.insert(i);
+      Node op = i.getOperator();
+      // initial refinement lemmas
+      std::vector<Node> conj;
+      // iand(x,y)=iand(y,x) is guaranteed by rewriting
+      Assert(i[0] <= i[1]);
+      // conj.push_back(i.eqNode(nm->mkNode(IAND, op, i[1], i[0])));
+      // 0 <= iand(x,y) < 2^k
+      conj.push_back(nm->mkNode(LEQ, d_zero, i));
+      conj.push_back(nm->mkNode(LT, i, twoToK(k)));
+      // iand(x,y)<=x
+      conj.push_back(nm->mkNode(LEQ, i, i[0]));
+      // iand(x,y)<=y
+      conj.push_back(nm->mkNode(LEQ, i, i[1]));
+      // x=y => iand(x,y)=x
+      conj.push_back(nm->mkNode(IMPLIES, i[0].eqNode(i[1]), i.eqNode(i[0])));
+      Node lem = conj.size() == 1 ? conj[0] : nm->mkNode(AND, conj);
+      Trace("iand-lemma") << "IAndSolver::Lemma: " << lem << " ; INIT_REFINE"
+                          << std::endl;
+      lems.push_back(lem);
+    }
+  }
+  return lems;
+}
+
+std::vector<NlLemma> IAndSolver::checkFullRefine()
+{
+  Trace("iand-check") << "IAndSolver::checkFullRefine";
+  Trace("iand-check") << "IAND terms: " << std::endl;
+  std::vector<NlLemma> lems;
+  for (const std::pair<const unsigned, std::vector<Node> >& is : d_iands)
+  {
+    // the reference bitwidth
+    unsigned k = is.first;
+    for (const Node& i : is.second)
+    {
+      Node valAndXY = d_model.computeAbstractModelValue(i);
+      Node valAndXYC = d_model.computeConcreteModelValue(i);
+      if (Trace.isOn("iand-check"))
+      {
+        Node x = i[0];
+        Node y = i[1];
+
+        Node valX = d_model.computeConcreteModelValue(x);
+        Node valY = d_model.computeConcreteModelValue(y);
+
+        Trace("iand-check")
+            << "* " << i << ", value = " << valAndXY << std::endl;
+        Trace("iand-check") << "  actual (" << valX << ", " << valY
+                            << ") = " << valAndXYC << std::endl;
+        // print the bit-vector versions
+        Node bvalX = convertToBvK(k, valX);
+        Node bvalY = convertToBvK(k, valY);
+        Node bvalAndXY = convertToBvK(k, valAndXY);
+        Node bvalAndXYC = convertToBvK(k, valAndXYC);
+
+        Trace("iand-check") << "  bv-value = " << bvalAndXY << std::endl;
+        Trace("iand-check") << "  bv-actual (" << bvalX << ", " << bvalY
+                            << ") = " << bvalAndXYC << std::endl;
+      }
+      if (valAndXY == valAndXYC)
+      {
+        Trace("iand-check") << "...already correct" << std::endl;
+        continue;
+      }
+
+      // ************* additional lemma schemas go here
+      if (options::iandMode() == options::IandMode::SUM)
+      {
+        // add lemmas based on sum mode
+      }
+      else if (options::iandMode() == options::IandMode::BITWISE)
+      {
+        // add lemmas based on sum mode
+      }
+      else
+      {
+        // this is the most naive model-based schema based on model values
+        Node lem = valueBasedLemma(i);
+        Trace("iand-lemma")
+            << "IAndSolver::Lemma: " << lem << " ; VALUE_REFINE" << std::endl;
+        lems.push_back(lem);
+      }
+    }
+  }
+
+  return lems;
+}
+
+Node IAndSolver::convertToBvK(unsigned k, Node n) const
+{
+  Assert(n.isConst() && n.getType().isInteger());
+  NodeManager* nm = NodeManager::currentNM();
+  Node iToBvOp = nm->mkConst(IntToBitVector(k));
+  Node bn = nm->mkNode(kind::INT_TO_BITVECTOR, iToBvOp, n);
+  return Rewriter::rewrite(bn);
+}
+
+Node IAndSolver::twoToK(unsigned k) const
+{
+  // could be faster
+  NodeManager* nm = NodeManager::currentNM();
+  Node ret = nm->mkNode(POW, d_two, nm->mkConst(Rational(k)));
+  ret = Rewriter::rewrite(ret);
+  return ret;
+}
+
+Node IAndSolver::twoToKMinusOne(unsigned k) const
+{
+  // could be faster
+  NodeManager* nm = NodeManager::currentNM();
+  Node ret = nm->mkNode(MINUS, twoToK(k), d_one);
+  ret = Rewriter::rewrite(ret);
+  return ret;
+}
+
+Node IAndSolver::mkIAnd(unsigned k, Node x, Node y) const
+{
+  NodeManager* nm = NodeManager::currentNM();
+  Node iAndOp = nm->mkConst(IntAnd(k));
+  Node ret = nm->mkNode(IAND, iAndOp, x, y);
+  ret = Rewriter::rewrite(ret);
+  return ret;
+}
+
+Node IAndSolver::mkIOr(unsigned k, Node x, Node y) const
+{
+  Node ret = mkINot(k, mkIAnd(k, mkINot(k, x), mkINot(k, y)));
+  ret = Rewriter::rewrite(ret);
+  return ret;
+}
+
+Node IAndSolver::mkINot(unsigned k, Node x) const
+{
+  NodeManager* nm = NodeManager::currentNM();
+  Node ret = nm->mkNode(MINUS, twoToKMinusOne(k), x);
+  ret = Rewriter::rewrite(ret);
+  return ret;
+}
+
+Node IAndSolver::iextract(unsigned i, unsigned j, Node n) const
+{
+  NodeManager* nm = NodeManager::currentNM();
+  //  ((_ extract i j) n) is n / 2^j mod 2^{i-j+1}
+  Node n2j = nm->mkNode(INTS_DIVISION_TOTAL, n, twoToK(j));
+  Node ret = nm->mkNode(INTS_MODULUS_TOTAL, n2j, twoToK(i - j + 1));
+  ret = Rewriter::rewrite(ret);
+  return ret;
+}
+
+Node IAndSolver::valueBasedLemma(Node i)
+{
+  Assert(i.getKind() == IAND);
+  Node x = i[0];
+  Node y = i[1];
+
+  Node valX = d_model.computeConcreteModelValue(x);
+  Node valY = d_model.computeConcreteModelValue(y);
+
+  NodeManager* nm = NodeManager::currentNM();
+  Node valC = nm->mkNode(IAND, i.getOperator(), valX, valY);
+  valC = Rewriter::rewrite(valC);
+
+  Node lem = nm->mkNode(
+      IMPLIES, nm->mkNode(AND, x.eqNode(valX), y.eqNode(valY)), i.eqNode(valC));
+  return lem;
+}
+
+bool oneBitAnd(bool a, bool b) { return (a && b); }
+
+}  // namespace nl
+}  // namespace arith
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/arith/nl/iand_solver.h b/src/theory/arith/nl/iand_solver.h
new file mode 100644
index 000000000..b526dac57
--- /dev/null
+++ b/src/theory/arith/nl/iand_solver.h
@@ -0,0 +1,127 @@
+/*********************                                                        */
+/*! \file iand_solver.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Solver for integer and (IAND) constraints
+ **/
+
+#ifndef CVC4__THEORY__ARITH__NL__IAND_SOLVER_H
+#define CVC4__THEORY__ARITH__NL__IAND_SOLVER_H
+
+#include <map>
+#include <vector>
+
+#include "context/cdhashset.h"
+#include "expr/node.h"
+#include "theory/arith/nl/nl_lemma_utils.h"
+#include "theory/arith/nl/nl_model.h"
+#include "theory/arith/theory_arith.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+namespace nl {
+
+/** Integer and solver class
+ *
+ */
+class IAndSolver
+{
+  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+
+ public:
+  IAndSolver(TheoryArith& containing, NlModel& model);
+  ~IAndSolver();
+
+  /** init last call
+   *
+   * This is called at the beginning of last call effort check, where
+   * assertions are the set of assertions belonging to arithmetic,
+   * false_asserts is the subset of assertions that are false in the current
+   * model, and xts is the set of extended function terms that are active in
+   * the current context.
+   */
+  void initLastCall(const std::vector<Node>& assertions,
+                    const std::vector<Node>& false_asserts,
+                    const std::vector<Node>& xts);
+  //-------------------------------------------- lemma schemas
+  /** check initial refine
+   *
+   * Returns a set of valid theory lemmas, based on simple facts about IAND.
+   *
+   * Examples where iand is shorthand for (_ iand k):
+   *
+   * 0 <= iand(x,y) < 2^k
+   * iand(x,y) <= x
+   * iand(x,y) <= y
+   * x=y => iand(x,y)=x
+   *
+   * This should be a heuristic incomplete check that only introduces a
+   * small number of new terms in the lemmas it returns.
+   */
+  std::vector<NlLemma> checkInitialRefine();
+  /** check full refine
+   *
+   * This should be a complete check that returns at least one lemma to
+   * rule out the current model.
+   */
+  std::vector<NlLemma> checkFullRefine();
+
+  //-------------------------------------------- end lemma schemas
+ private:
+  // The theory of arithmetic containing this extension.
+  TheoryArith& d_containing;
+  /** Reference to the non-linear model object */
+  NlModel& d_model;
+  /** commonly used terms */
+  Node d_zero;
+  Node d_one;
+  Node d_neg_one;
+  Node d_two;
+  Node d_true;
+  Node d_false;
+  /** IAND terms that have been given initial refinement lemmas */
+  NodeSet d_initRefine;
+  /** all IAND terms, for each bit-width */
+  std::map<unsigned, std::vector<Node> > d_iands;
+
+  /**
+   * convert integer value to bitvector value of bitwidth k,
+   * equivalent to Rewriter::rewrite( ((_ intToBv k) n) ).
+   */
+  Node convertToBvK(unsigned k, Node n) const;
+  /** 2^k */
+  Node twoToK(unsigned k) const;
+  /** 2^k-1 */
+  Node twoToKMinusOne(unsigned k) const;
+  /** make iand */
+  Node mkIAnd(unsigned k, Node x, Node y) const;
+  /** make ior */
+  Node mkIOr(unsigned k, Node x, Node y) const;
+  /** make inot */
+  Node mkINot(unsigned k, Node i) const;
+  /** extract from integer
+   *  ((_ extract i j) n) is n / 2^j mod 2^{i-j+1}
+   */
+  Node iextract(unsigned i, unsigned j, Node n) const;
+  /**
+   * Value-based refinement lemma for i of the form ((_ iand k) x y). Returns:
+   *   x = M(x) ^ y = M(y) =>
+   *     ((_ iand k) x y) = Rewriter::rewrite(((_ iand k) M(x) M(y)))
+   */
+  Node valueBasedLemma(Node i);
+}; /* class IAndSolver */
+
+}  // namespace nl
+}  // namespace arith
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__ARITH__IAND_SOLVER_H */
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index 5ded7d3d0..bd48a726a 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -40,6 +40,7 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing,
       d_model(containing.getSatContext()),
       d_trSlv(d_model),
       d_nlSlv(containing, d_model),
+      d_iandSlv(containing, d_model),
       d_builtModel(containing.getSatContext(), false)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
@@ -96,8 +97,9 @@ std::pair<bool, Node> NonlinearExtension::isExtfReduced(
   if (n != d_zero)
   {
     Kind k = n.getKind();
-    return std::make_pair(k != NONLINEAR_MULT && !isTranscendentalKind(k),
-                          Node::null());
+    return std::make_pair(
+        k != NONLINEAR_MULT && !isTranscendentalKind(k) && k != IAND,
+        Node::null());
   }
   Assert(n == d_zero);
   if (on.getKind() == NONLINEAR_MULT)
@@ -402,6 +404,7 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
                                       std::vector<NlLemma>& wlems)
 {
   std::vector<NlLemma> lemmas;
+
   if (options::nlExt())
   {
     // initialize the non-linear solver
@@ -411,6 +414,10 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
     // process lemmas that may have been generated by the transcendental solver
     filterLemmas(lemmas, lems);
   }
+  
+  // init last call with IAND
+  d_iandSlv.initLastCall(assertions, false_asserts, xts);
+  
   if (!lems.empty())
   {
     Trace("nl-ext") << "  ...finished with " << lems.size()
@@ -445,7 +452,16 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
       return lems.size();
     }
   }
-
+  //-----------------------------------initial lemmas for iand
+  lemmas = d_iandSlv.checkInitialRefine();
+  filterLemmas(lemmas, lems);
+  if (!lems.empty())
+  {
+    Trace("nl-ext") << "  ...finished with " << lems.size() << " new lemmas."
+                    << std::endl;
+    return lems.size();
+  }
+  
   // main calls to nlExt
   if (options::nlExt())
   {
@@ -559,6 +575,9 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
       filterLemmas(lemmas, wlems);
     }
   }
+  // run the full refinement in the IAND solver
+  lemmas = d_iandSlv.checkFullRefine();
+  filterLemmas(lemmas, wlems);
 
   Trace("nl-ext") << "  ...finished with " << wlems.size() << " waiting lemmas."
                   << std::endl;
diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h
index cb436bda7..ed1838b4b 100644
--- a/src/theory/arith/nl/nonlinear_extension.h
+++ b/src/theory/arith/nl/nonlinear_extension.h
@@ -25,6 +25,7 @@
 #include "context/cdlist.h"
 #include "expr/kind.h"
 #include "expr/node.h"
+#include "theory/arith/nl/iand_solver.h"
 #include "theory/arith/nl/nl_lemma_utils.h"
 #include "theory/arith/nl/nl_model.h"
 #include "theory/arith/nl/nl_solver.h"
@@ -303,6 +304,12 @@ class NonlinearExtension
    * constraints involving nonlinear mulitplication, Cimatti et al., TACAS 2017.
    */
   NlSolver d_nlSlv;
+  /** The integer and solver
+   *
+   * This is the subsolver responsible for running the procedure for
+   * constraints involving integer and.
+   */
+  IAndSolver d_iandSlv;
   /**
    * The lemmas we computed during collectModelInfo, to be sent out on the
    * output channel of TheoryArith.