pow2 -- final changes (#6800)

This commit adds the remaining changes for a working and integrated `pow2` solver.

In particular, it adds a rewrite and a lemma that identify `pow2(x)` with `0` whenever `x<0`.
Regressions are added as well, including `pow2-native-0.smt2` that shows the semantics of `pow2` on negative values.

The next steps are new rewrites and and more lemma schemas. 

20 files changed, 121 insertions, 12 deletions

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index e6de0d162..0228f6045 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -135,6 +135,7 @@ const static std::unordered_map<Kind, cvc5::Kind> s_kinds{
     {PLUS, cvc5::Kind::PLUS},
     {MULT, cvc5::Kind::MULT},
     {IAND, cvc5::Kind::IAND},
+    {POW2, cvc5::Kind::POW2},
     {MINUS, cvc5::Kind::MINUS},
     {UMINUS, cvc5::Kind::UMINUS},
     {DIVISION, cvc5::Kind::DIVISION},
@@ -410,6 +411,7 @@ const static std::unordered_map<cvc5::Kind, Kind, cvc5::kind::KindHashFunction>
         {cvc5::Kind::PLUS, PLUS},
         {cvc5::Kind::MULT, MULT},
         {cvc5::Kind::IAND, IAND},
+        {cvc5::Kind::POW2, POW2},
         {cvc5::Kind::MINUS, MINUS},
         {cvc5::Kind::UMINUS, UMINUS},
         {cvc5::Kind::DIVISION, DIVISION},
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 8c011aece..ec4ab6ae6 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -565,6 +565,8 @@ Command* Smt2::setLogic(std::string name, bool fromCommand)
     {
       // integer version of AND
       addIndexedOperator(api::IAND, api::IAND, "iand");
+      // pow2
+      addOperator(api::POW2, "pow2");
     }
   }
 
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 1f64bd23d..9f19acaab 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -681,9 +681,8 @@ void Smt2Printer::toStream(std::ostream& out,
   case kind::IS_INTEGER:
   case kind::TO_INTEGER:
   case kind::TO_REAL:
-  case kind::POW: 
-    out << smtKindString(k, d_variant) << " ";
-    break;
+  case kind::POW:
+  case kind::POW2: out << smtKindString(k, d_variant) << " "; break;
   case kind::IAND:
     out << "(_ iand " << n.getOperator().getConst<IntAnd>().d_size << ") ";
     stillNeedToPrintParams = false;
@@ -1152,6 +1151,7 @@ std::string Smt2Printer::smtKindString(Kind k, Variant v)
   case kind::MULT:
   case kind::NONLINEAR_MULT: return "*";
   case kind::IAND: return "iand";
+  case kind::POW2: return "POW2";
   case kind::EXPONENTIAL: return "exp";
   case kind::SINE: return "sin";
   case kind::COSINE: return "cos";
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index b0453fad4..6eda6283c 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -393,6 +393,12 @@ RewriteResponse ArithRewriter::postRewritePow2(TNode t)
     // pow2 is only supported for integers
     Assert(t[0].getType().isInteger());
     Integer i = t[0].getConst<Rational>().getNumerator();
+    if (i < 0)
+    {
+      return RewriteResponse(
+          REWRITE_DONE,
+          nm->mkConst<Rational>(Rational(Integer(0), Integer(1))));
+    }
     unsigned long k = i.getUnsignedLong();
     Node ret = nm->mkConst<Rational>(Rational(Integer(2).pow(k), Integer(1)));
     return RewriteResponse(REWRITE_DONE, ret);
diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index 96272f939..9e7202f1d 100644
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -85,6 +85,7 @@ void ArithCongruenceManager::finishInit(eq::EqualityEngine* ee,
   d_ee->addFunctionKind(kind::EXPONENTIAL);
   d_ee->addFunctionKind(kind::SINE);
   d_ee->addFunctionKind(kind::IAND);
+  d_ee->addFunctionKind(kind::POW2);
   // have proof equality engine only if proofs are enabled
   Assert(isProofEnabled() == (pfee != nullptr));
   d_pfee = pfee;
diff --git a/src/theory/arith/nl/ext_theory_callback.cpp b/src/theory/arith/nl/ext_theory_callback.cpp
index c778a89cc..02914f938 100644
--- a/src/theory/arith/nl/ext_theory_callback.cpp
+++ b/src/theory/arith/nl/ext_theory_callback.cpp
@@ -76,7 +76,8 @@ bool NlExtTheoryCallback::isExtfReduced(
   if (n != d_zero)
   {
     Kind k = n.getKind();
-    if (k != NONLINEAR_MULT && !isTranscendentalKind(k) && k != IAND)
+    if (k != NONLINEAR_MULT && !isTranscendentalKind(k) && k != IAND
+        && k != POW2)
     {
       id = ExtReducedId::ARITH_SR_LINEAR;
       return true;
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index 1bb558d1b..a8b056d45 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -59,13 +59,15 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing,
       d_tangentPlaneSlv(&d_extState),
       d_cadSlv(d_im, d_model, state.getUserContext(), pnm),
       d_icpSlv(d_im),
-      d_iandSlv(d_im, state, d_model)
+      d_iandSlv(d_im, state, d_model),
+      d_pow2Slv(d_im, state, d_model)
 {
   d_extTheory.addFunctionKind(kind::NONLINEAR_MULT);
   d_extTheory.addFunctionKind(kind::EXPONENTIAL);
   d_extTheory.addFunctionKind(kind::SINE);
   d_extTheory.addFunctionKind(kind::PI);
   d_extTheory.addFunctionKind(kind::IAND);
+  d_extTheory.addFunctionKind(kind::POW2);
   d_true = NodeManager::currentNM()->mkConst(true);
   d_zero = NodeManager::currentNM()->mkConst(Rational(0));
   d_one = NodeManager::currentNM()->mkConst(Rational(1));
@@ -568,6 +570,11 @@ void NonlinearExtension::runStrategy(Theory::Effort effort,
         break;
       case InferStep::IAND_FULL: d_iandSlv.checkFullRefine(); break;
       case InferStep::IAND_INITIAL: d_iandSlv.checkInitialRefine(); break;
+      case InferStep::POW2_INIT:
+        d_pow2Slv.initLastCall(assertions, false_asserts, xts);
+        break;
+      case InferStep::POW2_FULL: d_pow2Slv.checkFullRefine(); break;
+      case InferStep::POW2_INITIAL: d_pow2Slv.checkInitialRefine(); break;
       case InferStep::ICP:
         d_icpSlv.reset(assertions);
         d_icpSlv.check();
diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h
index 4e029be7c..aae19df6e 100644
--- a/src/theory/arith/nl/nonlinear_extension.h
+++ b/src/theory/arith/nl/nonlinear_extension.h
@@ -33,6 +33,7 @@
 #include "theory/arith/nl/iand_solver.h"
 #include "theory/arith/nl/icp/icp_solver.h"
 #include "theory/arith/nl/nl_model.h"
+#include "theory/arith/nl/pow2_solver.h"
 #include "theory/arith/nl/stats.h"
 #include "theory/arith/nl/strategy.h"
 #include "theory/arith/nl/transcendental/transcendental_solver.h"
@@ -277,6 +278,13 @@ class NonlinearExtension
    */
   IAndSolver d_iandSlv;
 
+  /** The pow2 solver
+   *
+   * This is the subsolver responsible for running the procedure for
+   * constraints involving powers of 2.
+   */
+  Pow2Solver d_pow2Slv;
+
   /** The strategy for the nonlinear extension. */
   Strategy d_strategy;
 
diff --git a/src/theory/arith/nl/pow2_solver.cpp b/src/theory/arith/nl/pow2_solver.cpp
index 41b9e6d72..d708e86e1 100644
--- a/src/theory/arith/nl/pow2_solver.cpp
+++ b/src/theory/arith/nl/pow2_solver.cpp
@@ -15,12 +15,16 @@
 
 #include "theory/arith/nl/pow2_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_state.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/nl_model.h"
 #include "theory/rewriter.h"
+#include "util/bitvector.h"
 
 using namespace cvc5::kind;
 
@@ -117,8 +121,8 @@ void Pow2Solver::checkFullRefine()
     {
       Trace("pow2-check") << "* " << i << ", value = " << valPow2xAbstract
                           << std::endl;
-      Trace("pow2-check") << "  actual (" << valXConcrete << ", "
-                          << ") = " << valPow2xConcrete << std::endl;
+      Trace("pow2-check") << "  actual " << valXConcrete << " = "
+                          << valPow2xConcrete << std::endl;
     }
     if (valPow2xAbstract == valPow2xConcrete)
     {
@@ -126,19 +130,19 @@ void Pow2Solver::checkFullRefine()
       continue;
     }
 
+    Integer x = valXConcrete.getConst<Rational>().getNumerator();
+    Integer pow2x = valPow2xAbstract.getConst<Rational>().getNumerator();
     // add monotinicity lemmas
     for (uint64_t j = i + 1; j < size; j++)
     {
       Node m = d_pow2s[j];
-      Node valPow2yConcrete = d_model.computeConcreteModelValue(m);
+      Node valPow2yAbstract = d_model.computeAbstractModelValue(m);
       Node valYConcrete = d_model.computeConcreteModelValue(m[0]);
 
-      Integer x = valXConcrete.getConst<Rational>().getNumerator();
       Integer y = valYConcrete.getConst<Rational>().getNumerator();
-      Integer pow2x = valPow2xConcrete.getConst<Rational>().getNumerator();
-      Integer pow2y = valPow2yConcrete.getConst<Rational>().getNumerator();
+      Integer pow2y = valPow2yAbstract.getConst<Rational>().getNumerator();
 
-      if (x <= y && pow2x > pow2y)
+      if (x < y && pow2x >= pow2y)
       {
         Node assumption = nm->mkNode(LEQ, n[0], m[0]);
         Node conclusion = nm->mkNode(LEQ, n, m);
@@ -148,6 +152,16 @@ void Pow2Solver::checkFullRefine()
         }
     }
 
+    // triviality lemmas: pow2(x) = 0 whenever x < 0
+    if (x < 0 && pow2x != 0)
+    {
+      Node assumption = nm->mkNode(LT, n[0], d_zero);
+      Node conclusion = nm->mkNode(EQUAL, n, d_zero);
+      Node lem = nm->mkNode(IMPLIES, assumption, conclusion);
+      d_im.addPendingLemma(
+          lem, InferenceId::ARITH_NL_POW2_TRIVIAL_CASE_REFINE, nullptr, true);
+    }
+
     // Place holder for additional lemma schemas
 
     // End of additional lemma schemas
@@ -161,6 +175,7 @@ void Pow2Solver::checkFullRefine()
         lem, InferenceId::ARITH_NL_POW2_VALUE_REFINE, nullptr, true);
   }
 }
+
 Node Pow2Solver::valueBasedLemma(Node i)
 {
   Assert(i.getKind() == POW2);
diff --git a/src/theory/arith/nl/strategy.cpp b/src/theory/arith/nl/strategy.cpp
index ffe925830..f20cf4221 100644
--- a/src/theory/arith/nl/strategy.cpp
+++ b/src/theory/arith/nl/strategy.cpp
@@ -37,6 +37,9 @@ std::ostream& operator<<(std::ostream& os, InferStep step)
     case InferStep::IAND_INIT: return os << "IAND_INIT";
     case InferStep::IAND_FULL: return os << "IAND_FULL";
     case InferStep::IAND_INITIAL: return os << "IAND_INITIAL";
+    case InferStep::POW2_INIT: return os << "POW2_INIT";
+    case InferStep::POW2_FULL: return os << "POW2_FULL";
+    case InferStep::POW2_INITIAL: return os << "POW2_INITIAL";
     case InferStep::ICP: return os << "ICP";
     case InferStep::NL_INIT: return os << "NL_INIT";
     case InferStep::NL_MONOMIAL_INFER_BOUNDS:
@@ -125,6 +128,8 @@ void Strategy::initializeStrategy()
   }
   one << InferStep::IAND_INIT;
   one << InferStep::IAND_INITIAL << InferStep::BREAK;
+  one << InferStep::POW2_INIT;
+  one << InferStep::POW2_INITIAL << InferStep::BREAK;
   if (options::nlExt() == options::NlExtMode::FULL
       || options::nlExt() == options::NlExtMode::LIGHT)
   {
@@ -164,6 +169,7 @@ void Strategy::initializeStrategy()
     one << InferStep::BREAK;
   }
   one << InferStep::IAND_FULL << InferStep::BREAK;
+  one << InferStep::POW2_FULL << InferStep::BREAK;
   if (options::nlCad())
   {
     one << InferStep::CAD_INIT;
diff --git a/src/theory/arith/nl/strategy.h b/src/theory/arith/nl/strategy.h
index ba0d3370e..e2fc6c1c6 100644
--- a/src/theory/arith/nl/strategy.h
+++ b/src/theory/arith/nl/strategy.h
@@ -44,7 +44,15 @@ enum class InferStep
   /** An initial IAND check */
   IAND_INITIAL,
 
+  /** Initialize the POW2 solver */
+  POW2_INIT,
+  /** A full POW2 check */
+  POW2_FULL,
+  /** An initial POW2 check */
+  POW2_INITIAL,
+
   /** An ICP check */
+
   ICP,
 
   /** Initialize the NL solver */
diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp
index 17b7dd83d..fe794ed72 100644
--- a/src/theory/arith/normal_form.cpp
+++ b/src/theory/arith/normal_form.cpp
@@ -78,6 +78,11 @@ bool Variable::isIAndMember(Node n)
          && Polynomial::isMember(n[1]);
 }
 
+bool Variable::isPow2Member(Node n)
+{
+  return n.getKind() == kind::POW2 && Polynomial::isMember(n[0]);
+}
+
 bool Variable::isDivMember(Node n){
   switch(n.getKind()){
   case kind::DIVISION:
diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h
index 2f2d56962..76a94f4c5 100644
--- a/src/theory/arith/normal_form.h
+++ b/src/theory/arith/normal_form.h
@@ -239,6 +239,7 @@ public:
      case kind::INTS_MODULUS_TOTAL:
      case kind::DIVISION_TOTAL: return isDivMember(n);
      case kind::IAND: return isIAndMember(n);
+     case kind::POW2: return isPow2Member(n);
      case kind::EXPONENTIAL:
      case kind::SINE:
      case kind::COSINE:
@@ -265,6 +266,7 @@ public:
 
   static bool isLeafMember(Node n);
   static bool isIAndMember(Node n);
+  static bool isPow2Member(Node n);
   static bool isDivMember(Node n);
   bool isDivLike() const{
     return isDivMember(getNode());
diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp
index 778c842a6..2cbba6b33 100644
--- a/src/theory/inference_id.cpp
+++ b/src/theory/inference_id.cpp
@@ -79,6 +79,10 @@ const char* toString(InferenceId i)
       return "ARITH_NL_POW2_INIT_REFINE";
     case InferenceId::ARITH_NL_POW2_VALUE_REFINE:
       return "ARITH_NL_POW2_VALUE_REFINE";
+    case InferenceId::ARITH_NL_POW2_MONOTONE_REFINE:
+      return "ARITH_NL_POW2_MONOTONE_REFINE";
+    case InferenceId::ARITH_NL_POW2_TRIVIAL_CASE_REFINE:
+      return "ARITH_NL_POW2_TRIVIAL_CASE_REFINE";
     case InferenceId::ARITH_NL_CAD_CONFLICT: return "ARITH_NL_CAD_CONFLICT";
     case InferenceId::ARITH_NL_CAD_EXCLUDED_INTERVAL:
       return "ARITH_NL_CAD_EXCLUDED_INTERVAL";
diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h
index 2216d8fed..f8bc35e08 100644
--- a/src/theory/inference_id.h
+++ b/src/theory/inference_id.h
@@ -133,6 +133,8 @@ enum class InferenceId
   ARITH_NL_POW2_VALUE_REFINE,
   // monotonicity refinements (Pow2Solver::checkFullRefine)
   ARITH_NL_POW2_MONOTONE_REFINE,
+  // trivial refinements (Pow2Solver::checkFullRefine)
+  ARITH_NL_POW2_TRIVIAL_CASE_REFINE,
   //-------------------- nonlinear cad solver
   // conflict / infeasible subset obtained from cad
   ARITH_NL_CAD_CONFLICT,
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 24eee5998..d2d6f0855 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -733,6 +733,10 @@ set(regress_0_tests
   regress0/nl/nta/sin-sym.smt2
   regress0/nl/nta/sqrt-simple.smt2
   regress0/nl/nta/tan-rewrite.smt2
+  regress0/nl/pow2-native-0.smt2
+  regress0/nl/pow2-native-1.smt2
+  regress0/nl/pow2-native-2.smt2
+  regress0/nl/pow2-native-3.smt2
   regress0/nl/real-as-int.smt2
   regress0/nl/real-div-ufnra.smt2
   regress0/nl/sin-cos-346-b-chunk-0169.smt2
diff --git a/test/regress/regress0/nl/pow2-native-0.smt2 b/test/regress/regress0/nl/pow2-native-0.smt2
new file mode 100644
index 000000000..f88ac4151
--- /dev/null
+++ b/test/regress/regress0/nl/pow2-native-0.smt2
@@ -0,0 +1,6 @@
+; EXPECT: unsat
+(set-logic QF_NIA)
+(declare-fun x () Int)
+(assert (< x 0))
+(assert (distinct (pow2 x) 0))
+(check-sat)
diff --git a/test/regress/regress0/nl/pow2-native-1.smt2 b/test/regress/regress0/nl/pow2-native-1.smt2
new file mode 100644
index 000000000..1e24ae572
--- /dev/null
+++ b/test/regress/regress0/nl/pow2-native-1.smt2
@@ -0,0 +1,9 @@
+; EXPECT: sat
+(set-logic QF_NIA)
+(set-info :status sat)
+(declare-fun x () Int)
+
+(assert (and (<= 0 x) (< x 16)))
+(assert (> (pow2 x) 0))
+
+(check-sat)
diff --git a/test/regress/regress0/nl/pow2-native-2.smt2 b/test/regress/regress0/nl/pow2-native-2.smt2
new file mode 100644
index 000000000..ba0621dbc
--- /dev/null
+++ b/test/regress/regress0/nl/pow2-native-2.smt2
@@ -0,0 +1,9 @@
+; EXPECT: unsat
+(set-logic QF_NIA)
+(set-info :status unsat)
+(declare-fun x () Int)
+
+(assert (and (<= 0 x) (< x 16)))
+(assert (< (pow2 x) x))
+
+(check-sat)
diff --git a/test/regress/regress0/nl/pow2-native-3.smt2 b/test/regress/regress0/nl/pow2-native-3.smt2
new file mode 100644
index 000000000..45975a474
--- /dev/null
+++ b/test/regress/regress0/nl/pow2-native-3.smt2
@@ -0,0 +1,12 @@
+; EXPECT: unsat
+(set-logic QF_NIA)
+(set-info :status unsat)
+(declare-fun x () Int)
+(declare-fun y () Int)
+
+(assert (<= 0 x))
+(assert (<= 0 y))
+(assert (< x y))
+(assert (> (pow2 x) (pow2 y)))
+
+(check-sat)