From eefd31d2fe256bdee9a5c33105eced1a358bb378 Mon Sep 17 00:00:00 2001 From: yoni206 Date: Fri, 25 Jun 2021 19:42:43 -0700 Subject: [PATCH] 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. --- src/api/cpp/cvc5.cpp | 2 ++ src/parser/smt2/smt2.cpp | 2 ++ src/printer/smt2/smt2_printer.cpp | 6 ++--- src/theory/arith/arith_rewriter.cpp | 6 +++++ src/theory/arith/congruence_manager.cpp | 1 + src/theory/arith/nl/ext_theory_callback.cpp | 3 ++- src/theory/arith/nl/nonlinear_extension.cpp | 9 ++++++- src/theory/arith/nl/nonlinear_extension.h | 8 ++++++ src/theory/arith/nl/pow2_solver.cpp | 29 ++++++++++++++++----- src/theory/arith/nl/strategy.cpp | 6 +++++ src/theory/arith/nl/strategy.h | 8 ++++++ src/theory/arith/normal_form.cpp | 5 ++++ src/theory/arith/normal_form.h | 2 ++ src/theory/inference_id.cpp | 4 +++ src/theory/inference_id.h | 2 ++ test/regress/CMakeLists.txt | 4 +++ test/regress/regress0/nl/pow2-native-0.smt2 | 6 +++++ test/regress/regress0/nl/pow2-native-1.smt2 | 9 +++++++ test/regress/regress0/nl/pow2-native-2.smt2 | 9 +++++++ test/regress/regress0/nl/pow2-native-3.smt2 | 12 +++++++++ 20 files changed, 121 insertions(+), 12 deletions(-) create mode 100644 test/regress/regress0/nl/pow2-native-0.smt2 create mode 100644 test/regress/regress0/nl/pow2-native-1.smt2 create mode 100644 test/regress/regress0/nl/pow2-native-2.smt2 create mode 100644 test/regress/regress0/nl/pow2-native-3.smt2 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 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::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().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().getNumerator(); + if (i < 0) + { + return RewriteResponse( + REWRITE_DONE, + nm->mkConst(Rational(Integer(0), Integer(1)))); + } unsigned long k = i.getUnsignedLong(); Node ret = nm->mkConst(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().getNumerator(); + Integer pow2x = valPow2xAbstract.getConst().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().getNumerator(); Integer y = valYConcrete.getConst().getNumerator(); - Integer pow2x = valPow2xConcrete.getConst().getNumerator(); - Integer pow2y = valPow2yConcrete.getConst().getNumerator(); + Integer pow2y = valPow2yAbstract.getConst().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) -- 2.30.2