pow2: adding a kind, inference rules, and some implementations in the pow2 solver (#6736)

This PR is the sequel of #6676 .
It adds the `POW2` kind, inference rules that will be used in the `pow2` solver, an implementation of one function of the solver, as well as stubs for the others. The next PR will include more implementations.

6 files changed, 101 insertions, 0 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index bec3a8345..2419e1e41 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -441,6 +441,7 @@ libcvc5_add_sources(
   theory/arith/nl/nonlinear_extension.h
   theory/arith/nl/poly_conversion.cpp
   theory/arith/nl/poly_conversion.h
+  theory/arith/nl/pow2_solver.cpp
   theory/arith/nl/pow2_solver.h
   theory/arith/nl/stats.cpp
   theory/arith/nl/stats.h
diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h
index 2ec190360..2c5d2873e 100644
--- a/src/api/cpp/cvc5_kind.h
+++ b/src/api/cpp/cvc5_kind.h
@@ -412,6 +412,22 @@ enum CVC5_EXPORT Kind : int32_t
    *   - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
    */
   IAND,
+  /**
+   * Operator for raising 2 to a non-negative integer  power
+   *
+   * Create with:
+   *   - `Solver::mkOp(Kind kind) const`
+   *
+
+   * Parameters:
+   *   - 1: Op of kind IAND
+   *   - 2: Integer term
+   *
+   * Create with:
+   *   - `Solver::mkTerm(const Op& op, const Term& child) const`
+   *   - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
+   */
+  POW2,
 #if 0
   /* Synonym for MULT.  */
   NONLINEAR_MULT,
diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index 396befb35..0c93db90f 100644
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -26,6 +26,7 @@ operator INTS_MODULUS_TOTAL 2 "integer modulus with interpreted division by 0 (i
 operator ABS 1 "absolute value"
 parameterized DIVISIBLE DIVISIBLE_OP 1 "divisibility-by-k predicate; first parameter is a DIVISIBLE_OP, second is integer term"
 operator POW 2 "arithmetic power"
+operator POW2 1 "arithmetic power of 2"
 
 operator EXPONENTIAL 1 "exponential"
 operator SINE 1 "sine"
@@ -148,6 +149,7 @@ typerule ARCTANGENT "SimpleTypeRule<RReal, AReal>"
 typerule ARCCOSECANT "SimpleTypeRule<RReal, AReal>"
 typerule ARCSECANT "SimpleTypeRule<RReal, AReal>"
 typerule ARCCOTANGENT "SimpleTypeRule<RReal, AReal>"
+typerule POW2 "SimpleTypeRule<RInteger, AInteger>"
 
 typerule SQRT "SimpleTypeRule<RReal, AReal>"
 
diff --git a/src/theory/arith/nl/pow2_solver.cpp b/src/theory/arith/nl/pow2_solver.cpp
new file mode 100644
index 000000000..534895c7f
--- /dev/null
+++ b/src/theory/arith/nl/pow2_solver.cpp
@@ -0,0 +1,73 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Makai Mann, Gereon Kremer
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * Implementation of pow2 solver.
+ */
+
+#include "theory/arith/nl/pow2_solver.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"
+
+using namespace cvc5::kind;
+
+namespace cvc5 {
+namespace theory {
+namespace arith {
+namespace nl {
+
+Pow2Solver::Pow2Solver(InferenceManager& im, ArithState& state, NlModel& model)
+    : d_im(im), d_model(model), d_initRefine(state.getUserContext())
+{
+  NodeManager* nm = NodeManager::currentNM();
+  d_false = nm->mkConst(false);
+  d_true = nm->mkConst(true);
+  d_zero = nm->mkConst(Rational(0));
+  d_one = nm->mkConst(Rational(1));
+  d_two = nm->mkConst(Rational(2));
+}
+
+Pow2Solver::~Pow2Solver() {}
+
+void Pow2Solver::initLastCall(const std::vector<Node>& assertions,
+                              const std::vector<Node>& false_asserts,
+                              const std::vector<Node>& xts)
+{
+  d_pow2s.clear();
+  Trace("pow2-mv") << "POW2 terms : " << std::endl;
+  for (const Node& a : xts)
+  {
+    Kind ak = a.getKind();
+    if (ak != POW2)
+    {
+      // don't care about other terms
+      continue;
+    }
+    d_pow2s.push_back(a);
+  }
+  Trace("pow2") << "We have " << d_pow2s.size() << " pow2 terms." << std::endl;
+}
+
+void Pow2Solver::checkInitialRefine() {}
+
+void Pow2Solver::checkFullRefine() {}
+
+Node Pow2Solver::valueBasedLemma(Node i) { return Node(); }
+
+}  // namespace nl
+}  // namespace arith
+}  // namespace theory
+}  // namespace cvc5
diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp
index fe4ed4c22..778c842a6 100644
--- a/src/theory/inference_id.cpp
+++ b/src/theory/inference_id.cpp
@@ -75,6 +75,10 @@ const char* toString(InferenceId i)
       return "ARITH_NL_IAND_SUM_REFINE";
     case InferenceId::ARITH_NL_IAND_BITWISE_REFINE:
       return "ARITH_NL_IAND_BITWISE_REFINE";
+    case InferenceId::ARITH_NL_POW2_INIT_REFINE:
+      return "ARITH_NL_POW2_INIT_REFINE";
+    case InferenceId::ARITH_NL_POW2_VALUE_REFINE:
+      return "ARITH_NL_POW2_VALUE_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 169992f41..6a87776d6 100644
--- a/src/theory/inference_id.h
+++ b/src/theory/inference_id.h
@@ -126,6 +126,11 @@ enum class InferenceId
   ARITH_NL_IAND_SUM_REFINE,
   // bitwise refinements (IAndSolver::checkFullRefine)
   ARITH_NL_IAND_BITWISE_REFINE,
+  //-------------------- nonlinear pow2 solver
+  // initial refinements (Pow2Solver::checkInitialRefine)
+  ARITH_NL_POW2_INIT_REFINE,
+  // value refinements (Pow2Solver::checkFullRefine)
+  ARITH_NL_POW2_VALUE_REFINE,
   //-------------------- nonlinear cad solver
   // conflict / infeasible subset obtained from cad
   ARITH_NL_CAD_CONFLICT,