diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arith/arith_rewriter.cpp | 6 | ||||
-rw-r--r-- | src/theory/arith/congruence_manager.cpp | 1 | ||||
-rw-r--r-- | src/theory/arith/nl/ext_theory_callback.cpp | 3 | ||||
-rw-r--r-- | src/theory/arith/nl/nonlinear_extension.cpp | 9 | ||||
-rw-r--r-- | src/theory/arith/nl/nonlinear_extension.h | 8 | ||||
-rw-r--r-- | src/theory/arith/nl/pow2_solver.cpp | 29 | ||||
-rw-r--r-- | src/theory/arith/nl/strategy.cpp | 6 | ||||
-rw-r--r-- | src/theory/arith/nl/strategy.h | 8 | ||||
-rw-r--r-- | src/theory/arith/normal_form.cpp | 5 | ||||
-rw-r--r-- | src/theory/arith/normal_form.h | 2 | ||||
-rw-r--r-- | src/theory/inference_id.cpp | 4 | ||||
-rw-r--r-- | src/theory/inference_id.h | 2 |
12 files changed, 74 insertions, 9 deletions
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, |