pow2: more implementations (#6756)

This PR adds implementations of functions from the pow2 solver, rewriter and type checker.

5 files changed, 118 insertions, 3 deletions

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 4d632e043..b0453fad4 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -112,6 +112,7 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){
     case kind::MULT:
     case kind::NONLINEAR_MULT: return preRewriteMult(t);
     case kind::IAND: return RewriteResponse(REWRITE_DONE, t);
+    case kind::POW2: return RewriteResponse(REWRITE_DONE, t);
     case kind::EXPONENTIAL:
     case kind::SINE:
     case kind::COSINE:
@@ -175,6 +176,7 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){
     case kind::MULT:
     case kind::NONLINEAR_MULT: return postRewriteMult(t);
     case kind::IAND: return postRewriteIAnd(t);
+    case kind::POW2: return postRewritePow2(t);
     case kind::EXPONENTIAL:
     case kind::SINE:
     case kind::COSINE:
@@ -381,6 +383,23 @@ RewriteResponse ArithRewriter::postRewriteMult(TNode t){
   return RewriteResponse(REWRITE_DONE, res.getNode());
 }
 
+RewriteResponse ArithRewriter::postRewritePow2(TNode t)
+{
+  Assert(t.getKind() == kind::POW2);
+  NodeManager* nm = NodeManager::currentNM();
+  // if constant, we eliminate
+  if (t[0].isConst())
+  {
+    // pow2 is only supported for integers
+    Assert(t[0].getType().isInteger());
+    Integer i = t[0].getConst<Rational>().getNumerator();
+    unsigned long k = i.getUnsignedLong();
+    Node ret = nm->mkConst<Rational>(Rational(Integer(2).pow(k), Integer(1)));
+    return RewriteResponse(REWRITE_DONE, ret);
+  }
+  return RewriteResponse(REWRITE_DONE, t);
+}
+
 RewriteResponse ArithRewriter::postRewriteIAnd(TNode t)
 {
   Assert(t.getKind() == kind::IAND);
diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h
index 6a92ba1cc..813f2b1bb 100644
--- a/src/theory/arith/arith_rewriter.h
+++ b/src/theory/arith/arith_rewriter.h
@@ -64,6 +64,7 @@ class ArithRewriter : public TheoryRewriter
   static RewriteResponse postRewriteMult(TNode t);
 
   static RewriteResponse postRewriteIAnd(TNode t);
+  static RewriteResponse postRewritePow2(TNode t);
 
   static RewriteResponse preRewriteTranscendental(TNode t);
   static RewriteResponse postRewriteTranscendental(TNode t);
diff --git a/src/theory/arith/nl/pow2_solver.cpp b/src/theory/arith/nl/pow2_solver.cpp
index 534895c7f..9864fc709 100644
--- a/src/theory/arith/nl/pow2_solver.cpp
+++ b/src/theory/arith/nl/pow2_solver.cpp
@@ -61,11 +61,81 @@ void Pow2Solver::initLastCall(const std::vector<Node>& assertions,
   Trace("pow2") << "We have " << d_pow2s.size() << " pow2 terms." << std::endl;
 }
 
-void Pow2Solver::checkInitialRefine() {}
+void Pow2Solver::checkInitialRefine()
+{
+  Trace("pow2-check") << "Pow2Solver::checkInitialRefine" << std::endl;
+  NodeManager* nm = NodeManager::currentNM();
+  for (const Node& i : d_pow2s)
+  {
+    if (d_initRefine.find(i) != d_initRefine.end())
+    {
+      // already sent initial axioms for i in this user context
+      continue;
+    }
+    d_initRefine.insert(i);
+    // initial refinement lemmas
+    std::vector<Node> conj;
+    // x>=0 -> x < pow2(x)
+    Node xgeq0 = nm->mkNode(LEQ, d_zero, i[0]);
+    Node xltpow2x = nm->mkNode(LT, i[0], i);
+    conj.push_back(nm->mkNode(IMPLIES, xgeq0, xltpow2x));
+    Node lem = nm->mkAnd(conj);
+    Trace("pow2-lemma") << "Pow2Solver::Lemma: " << lem << " ; INIT_REFINE"
+                        << std::endl;
+    d_im.addPendingLemma(lem, InferenceId::ARITH_NL_POW2_INIT_REFINE);
+  }
+}
 
-void Pow2Solver::checkFullRefine() {}
+void Pow2Solver::checkFullRefine()
+{
+  Trace("pow2-check") << "Pow2Solver::checkFullRefine";
+  Trace("pow2-check") << "pow2 terms: " << std::endl;
+  for (const Node& i : d_pow2s)
+  {
+    Node valPow2x = d_model.computeAbstractModelValue(i);
+    Node valPow2xC = d_model.computeConcreteModelValue(i);
+    if (Trace.isOn("pow2-check"))
+    {
+      Node x = i[0];
+      Node valX = d_model.computeConcreteModelValue(x);
 
-Node Pow2Solver::valueBasedLemma(Node i) { return Node(); }
+      Trace("pow2-check") << "* " << i << ", value = " << valPow2x << std::endl;
+      Trace("pow2-check") << "  actual (" << valX << ", "
+                          << ") = " << valPow2xC << std::endl;
+    }
+    if (valPow2x == valPow2xC)
+    {
+      Trace("pow2-check") << "...already correct" << std::endl;
+      continue;
+    }
+
+    // Place holder for additional lemma schemas
+    //
+    // End of additional lemma schemas
+
+    // this is the most naive model-based schema based on model values
+    Node lem = valueBasedLemma(i);
+    Trace("pow2-lemma") << "Pow2Solver::Lemma: " << lem << " ; VALUE_REFINE"
+                        << std::endl;
+    // send the value lemma
+    d_im.addPendingLemma(
+        lem, InferenceId::ARITH_NL_POW2_VALUE_REFINE, nullptr, true);
+  }
+}
+Node Pow2Solver::valueBasedLemma(Node i)
+{
+  Assert(i.getKind() == POW2);
+  Node x = i[0];
+
+  Node valX = d_model.computeConcreteModelValue(x);
+
+  NodeManager* nm = NodeManager::currentNM();
+  Node valC = nm->mkNode(POW2, valX);
+  valC = Rewriter::rewrite(valC);
+
+  Node lem = nm->mkNode(IMPLIES, x.eqNode(valX), i.eqNode(valC));
+  return lem;
+}
 
 }  // namespace nl
 }  // namespace arith
diff --git a/src/theory/arith/theory_arith_type_rules.cpp b/src/theory/arith/theory_arith_type_rules.cpp
index 1ba501f90..c9309a3d4 100644
--- a/src/theory/arith/theory_arith_type_rules.cpp
+++ b/src/theory/arith/theory_arith_type_rules.cpp
@@ -133,6 +133,25 @@ TypeNode IAndTypeRule::computeType(NodeManager* nodeManager,
   return nodeManager->integerType();
 }
 
+TypeNode Pow2TypeRule::computeType(NodeManager* nodeManager,
+                                   TNode n,
+                                   bool check)
+{
+  if (n.getKind() != kind::POW2)
+  {
+    InternalError() << "POW2 typerule invoked for POW2 kind";
+  }
+  if (check)
+  {
+    TypeNode arg1 = n[0].getType(check);
+    if (!arg1.isInteger())
+    {
+      throw TypeCheckingExceptionPrivate(n, "expecting integer terms");
+    }
+  }
+  return nodeManager->integerType();
+}
+
 TypeNode IndexedRootPredicateTypeRule::computeType(NodeManager* nodeManager,
                                                    TNode n,
                                                    bool check)
diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h
index f7ef64e2d..7bb623ad2 100644
--- a/src/theory/arith/theory_arith_type_rules.h
+++ b/src/theory/arith/theory_arith_type_rules.h
@@ -55,6 +55,12 @@ class IAndTypeRule
   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
+class Pow2TypeRule
+{
+ public:
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
+};
+
 class IndexedRootPredicateTypeRule
 {
  public: