From 5e7107f378f917731acbd017c854829f25ac8bdf Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 25 Feb 2022 12:45:43 -0600 Subject: [PATCH] Simplify and fix how purified terms are managed in the trancendental solver (#8167) Simplification is leftover from the sine symmetry heuristic, now the mapping from terms to what purifies them is injective. Also makes the mapping context-dependent. It also ensures that we keep model values for purification arguments. Fixes #8160. --- .../nl/transcendental/exponential_solver.h | 2 +- .../arith/nl/transcendental/sine_solver.cpp | 10 +---- .../transcendental/transcendental_solver.cpp | 41 +++++++++++++------ .../transcendental/transcendental_state.cpp | 32 ++++++++++----- .../nl/transcendental/transcendental_state.h | 33 ++++++++++----- test/regress/CMakeLists.txt | 1 + .../nl/nta/issue8160-model-purify.smt2 | 9 ++++ 7 files changed, 86 insertions(+), 42 deletions(-) create mode 100644 test/regress/regress0/nl/nta/issue8160-model-purify.smt2 diff --git a/src/theory/arith/nl/transcendental/exponential_solver.h b/src/theory/arith/nl/transcendental/exponential_solver.h index 05bbb141a..e13fb2a71 100644 --- a/src/theory/arith/nl/transcendental/exponential_solver.h +++ b/src/theory/arith/nl/transcendental/exponential_solver.h @@ -27,7 +27,7 @@ namespace arith { namespace nl { namespace transcendental { -struct TranscendentalState; +class TranscendentalState; /** Transcendental solver class * diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp index 3299a0586..21bbd4feb 100644 --- a/src/theory/arith/nl/transcendental/sine_solver.cpp +++ b/src/theory/arith/nl/transcendental/sine_solver.cpp @@ -111,15 +111,7 @@ void SineSolver::checkInitialRefine() if (d_tf_initial_refine.find(t) == d_tf_initial_refine.end()) { d_tf_initial_refine[t] = true; - Node symn = nm->mkNode(Kind::SINE, - nm->mkNode(Kind::MULT, d_data->d_neg_one, t[0])); - symn = rewrite(symn); - // Can assume it is its own master since phase is split over 0, - // hence -pi <= t[0] <= pi implies -pi <= -t[0] <= pi. - d_data->d_trMaster[symn] = symn; - d_data->d_trSlaves[symn].insert(symn); - Assert(d_data->d_trSlaves.find(t) != d_data->d_trSlaves.end()); - + Assert(d_data->isPurified(t)); { // sine bounds: -1 <= sin(t) <= 1 Node lem = nm->mkNode(Kind::AND, diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp index c394512d1..7db06008f 100644 --- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp @@ -67,16 +67,18 @@ void TranscendentalSolver::initLastCall(const std::vector& xts) for (const Node& a : needsMaster) { // should not have processed this already - Assert(d_tstate.d_trMaster.find(a) == d_tstate.d_trMaster.end()); + Assert(d_tstate.d_trPurify.find(a) == d_tstate.d_trPurify.end()); Kind k = a.getKind(); Assert(k == Kind::SINE || k == Kind::EXPONENTIAL); Node y = sm->mkSkolemFunction( SkolemFunId::TRANSCENDENTAL_PURIFY_ARG, nm->realType(), a); Node new_a = nm->mkNode(k, y); - d_tstate.d_trSlaves[new_a].insert(new_a); - d_tstate.d_trSlaves[new_a].insert(a); - d_tstate.d_trMaster[a] = new_a; - d_tstate.d_trMaster[new_a] = new_a; + Assert(d_tstate.d_trPurify.find(new_a) == d_tstate.d_trPurify.end()); + Assert(d_tstate.d_trPurifies.find(new_a) == d_tstate.d_trPurifies.end()); + d_tstate.d_trPurify[a] = new_a; + d_tstate.d_trPurify[new_a] = new_a; + d_tstate.d_trPurifies[new_a] = a; + d_tstate.d_trPurifyVars.insert(y); switch (k) { case Kind::SINE: d_sineSlv.doPhaseShift(a, new_a, y); break; @@ -90,7 +92,7 @@ bool TranscendentalSolver::preprocessAssertionsCheckModel( std::vector& assertions) { Subs subs; - for (const auto& sub : d_tstate.d_trMaster) + for (const auto& sub : d_tstate.d_trPurify) { subs.add(sub.first, sub.second); } @@ -141,10 +143,16 @@ bool TranscendentalSolver::preprocessAssertionsCheckModel( // for each function in the congruence classe for (const Node& ctf : d_tstate.d_funcCongClass[tf]) { - // each term in congruence classes should be master terms - Assert(d_tstate.d_trSlaves.find(ctf) != d_tstate.d_trSlaves.end()); - // we set the bounds for each slave of tf - for (const Node& stf : d_tstate.d_trSlaves[ctf]) + std::vector mset{ctf}; + // if this purifies another term, we set a bound on the term it + // purifies as well + context::CDHashMap::const_iterator itp = + d_tstate.d_trPurifies.find(ctf); + if (itp != d_tstate.d_trPurifies.end() && itp->second != ctf) + { + mset.push_back(itp->second); + } + for (const Node& stf : mset) { Trace("nl-ext-cm") << "...bound for " << stf << " : [" << bounds.first << ", " @@ -266,8 +274,8 @@ bool TranscendentalSolver::checkTfTangentPlanesFun(Node tf, unsigned d) { NodeManager* nm = NodeManager::currentNM(); Kind k = tf.getKind(); - // this should only be run on master applications - Assert(d_tstate.d_trSlaves.find(tf) != d_tstate.d_trSlaves.end()); + // this should only be run on purified applications + Assert(d_tstate.isPurified(tf)); // Figure 3 : c Node c = d_tstate.d_model.computeAbstractModelValue(tf[0]); @@ -477,6 +485,15 @@ void TranscendentalSolver::postProcessModel(std::map& arithModel, // skip integer variables if (am.first.getType().isInteger()) { + Trace("nl-ext") << "...keep model value for integer " << am.first + << std::endl; + continue; + } + // cannot erase values for purification arguments + if (d_tstate.d_trPurifyVars.find(am.first) != d_tstate.d_trPurifyVars.end()) + { + Trace("nl-ext") << "...keep model value for purification variable " + << am.first << std::endl; continue; } Node r = d_astate.getRepresentative(am.first); diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp index 3f003823c..45d2b81bb 100644 --- a/src/theory/arith/nl/transcendental/transcendental_state.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp @@ -33,7 +33,12 @@ namespace transcendental { TranscendentalState::TranscendentalState(Env& env, InferenceManager& im, NlModel& model) - : EnvObj(env), d_im(im), d_model(model) + : EnvObj(env), + d_im(im), + d_model(model), + d_trPurify(userContext()), + d_trPurifies(userContext()), + d_trPurifyVars(userContext()) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); @@ -61,7 +66,7 @@ CDProof* TranscendentalState::getProof() } void TranscendentalState::init(const std::vector& xts, - std::vector& needsMaster) + std::vector& needsPurify) { d_funcCongClass.clear(); d_funcMap.clear(); @@ -70,6 +75,7 @@ void TranscendentalState::init(const std::vector& xts, bool needPi = false; // for computing congruence std::map argTrie; + NodeMap::const_iterator itp; for (std::size_t i = 0, xsize = xts.size(); i < xsize; ++i) { // Ignore if it is not a transcendental @@ -80,11 +86,11 @@ void TranscendentalState::init(const std::vector& xts, Node a = xts[i]; Kind ak = a.getKind(); bool consider = true; - // if we've already computed master for a - if (d_trMaster.find(a) != d_trMaster.end()) + // if we've already assigned a purified term + itp = d_trPurify.find(a); + if (itp != d_trPurify.end()) { - // a master has at least one slave - consider = (d_trSlaves.find(a) != d_trSlaves.end()); + consider = itp->second == a; } else { @@ -106,13 +112,14 @@ void TranscendentalState::init(const std::vector& xts, } if (!consider) { - // wait to assign a master below - needsMaster.push_back(a); + // must assign a purified term + needsPurify.push_back(a); } else { - d_trMaster[a] = a; - d_trSlaves[a].insert(a); + // assume own purified + d_trPurify[a] = a; + d_trPurifies[a] = a; } } if (ak == Kind::EXPONENTIAL || ak == Kind::SINE) @@ -448,6 +455,11 @@ void TranscendentalState::doSecantLemmas(const std::pair& bounds, } } +bool TranscendentalState::isPurified(TNode n) const +{ + return d_trPurifies.find(n) != d_trPurifies.end(); +} + } // namespace transcendental } // namespace nl } // namespace arith diff --git a/src/theory/arith/nl/transcendental/transcendental_state.h b/src/theory/arith/nl/transcendental/transcendental_state.h index ede8079a4..292656e4e 100644 --- a/src/theory/arith/nl/transcendental/transcendental_state.h +++ b/src/theory/arith/nl/transcendental/transcendental_state.h @@ -16,6 +16,8 @@ #ifndef CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_STATE_H #define CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_STATE_H +#include "context/cdhashmap.h" +#include "context/cdhashset.h" #include "expr/node.h" #include "proof/proof_set.h" #include "smt/env.h" @@ -60,8 +62,12 @@ inline std::ostream& operator<<(std::ostream& os, Convexity c) { * This includes common lookups and caches as well as generic utilities for * secant plane lemmas and taylor approximations. */ -struct TranscendentalState : protected EnvObj +class TranscendentalState : protected EnvObj { + using NodeMap = context::CDHashMap; + using NodeSet = context::CDHashSet; + + public: TranscendentalState(Env& env, InferenceManager& im, NlModel& model); /** @@ -80,10 +86,10 @@ struct TranscendentalState : protected EnvObj * * This call may add lemmas to lems based on registering term * information (for example to ensure congruence of terms). - * It puts terms that need to be treated further as a master term on their own - * (for example purification of sine terms) into needsMaster. + * It puts terms that need to be treated further as a purified term on their + * own (for example purification of sine terms) into needsPurify. */ - void init(const std::vector& xts, std::vector& needsMaster); + void init(const std::vector& xts, std::vector& needsPurify); /** * Checks for terms that are congruent but disequal to a. @@ -157,6 +163,10 @@ struct TranscendentalState : protected EnvObj Convexity convexity, unsigned d, unsigned actual_d); + /** + * Is term t purified? (See d_trPurify below). + */ + bool isPurified(TNode n) const; Node d_true; Node d_false; @@ -181,18 +191,21 @@ struct TranscendentalState : protected EnvObj /** * Some transcendental functions f(t) are "purified", e.g. we add * t = y ^ f(t) = f(y) where y is a fresh variable. Those that are not - * purified we call "master terms". + * purified we call "purified terms". * - * The maps below maintain a master/slave relationship over - * transcendental functions (SINE, EXPONENTIAL, PI), where above - * f(y) is the master of itself and of f(t). + * The maps below maps transcendental function applications (SINE, + * EXPONENTIAL, PI) to their purified version, where above + * f(y) is the purified version of itself and of f(t). * * This is used for ensuring that the argument y of SINE we process is on * the interval [-pi .. pi], and that exponentials are not applied to * arguments that contain transcendental functions. */ - std::map d_trMaster; - std::map> d_trSlaves; + NodeMap d_trPurify; + /** inverse mapping of above, which is injective */ + NodeMap d_trPurifies; + /** The set of purification variables we have introduced */ + NodeSet d_trPurifyVars; /** concavity region for transcendental functions * diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index e9c4e98a5..2ec4dc348 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -791,6 +791,7 @@ set(regress_0_tests regress0/nl/nta/exp1-ub.smt2 regress0/nl/nta/issue7938-tf-model.smt2 regress0/nl/nta/issue8147-unc-model.smt2 + regress0/nl/nta/issue8160-model-purify.smt2 regress0/nl/nta/real-pi.smt2 regress0/nl/nta/sin-sym.smt2 regress0/nl/nta/sqrt-simple.smt2 diff --git a/test/regress/regress0/nl/nta/issue8160-model-purify.smt2 b/test/regress/regress0/nl/nta/issue8160-model-purify.smt2 new file mode 100644 index 000000000..0d260d5fd --- /dev/null +++ b/test/regress/regress0/nl/nta/issue8160-model-purify.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: -q +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) +(declare-fun b (Int Int) Int) +(declare-fun v () Real) +(declare-fun a () Real) +(assert (forall ((V Real)) (and (= 0 (b 0 0)) (forall ((V Real)) (= 0.0 (sin v))) (exists ((V Real)) (= 1.0 (* a a)))))) +(check-sat) -- 2.30.2