From: Andrew Reynolds Date: Tue, 1 Mar 2022 21:14:16 +0000 (-0600) Subject: Fix issue involving dropped purification lemmas for transcendental functions (#8198) X-Git-Tag: cvc5-1.0.0~352 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=64583f8e57492e8499f681dae333c93efaf7bb79;p=cvc5.git Fix issue involving dropped purification lemmas for transcendental functions (#8198) Fixes #4693. Fixes #8181 (which now times out). The issue was caused by purification lemmas being dropped, often in incremental mode. This meant that we were replacing sin(t) by sin(k) when checking models, but not having any information about sin(k). We now are more robust and send the purification lemmas for transcendental functions based on checking whether it is necessary to do so. --- diff --git a/src/theory/arith/nl/transcendental/exponential_solver.cpp b/src/theory/arith/nl/transcendental/exponential_solver.cpp index 918a81364..ccfc2f265 100644 --- a/src/theory/arith/nl/transcendental/exponential_solver.cpp +++ b/src/theory/arith/nl/transcendental/exponential_solver.cpp @@ -44,11 +44,11 @@ ExponentialSolver::ExponentialSolver(Env& env, TranscendentalState* tstate) ExponentialSolver::~ExponentialSolver() {} -void ExponentialSolver::doPurification(TNode a, TNode new_a, TNode y) +void ExponentialSolver::doPurification(TNode a, TNode new_a) { NodeManager* nm = NodeManager::currentNM(); // do both equalities to ensure that new_a becomes a preregistered term - Node lem = nm->mkNode(Kind::AND, a.eqNode(new_a), a[0].eqNode(y)); + Node lem = nm->mkNode(Kind::AND, a.eqNode(new_a), a[0].eqNode(new_a[0])); // note we must do preprocess on this lemma Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : purify : " << lem << std::endl; diff --git a/src/theory/arith/nl/transcendental/exponential_solver.h b/src/theory/arith/nl/transcendental/exponential_solver.h index e13fb2a71..196b109ed 100644 --- a/src/theory/arith/nl/transcendental/exponential_solver.h +++ b/src/theory/arith/nl/transcendental/exponential_solver.h @@ -49,9 +49,9 @@ class ExponentialSolver : protected EnvObj /** * Ensures that new_a is properly registered as a term where new_a is the - * purified version of a, y being the new skolem used for purification. + * purified version of a, new_a[0] being the new skolem used for purification. */ - void doPurification(TNode a, TNode new_a, TNode y); + void doPurification(TNode a, TNode new_a); /** * check initial refine diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp index 8ab363687..e765a1599 100644 --- a/src/theory/arith/nl/transcendental/sine_solver.cpp +++ b/src/theory/arith/nl/transcendental/sine_solver.cpp @@ -158,8 +158,9 @@ void SineSolver::doReductions() } } -void SineSolver::doPhaseShift(TNode a, TNode new_a, TNode y) +void SineSolver::doPhaseShift(TNode a, TNode new_a) { + TNode y = new_a[0]; NodeManager* nm = NodeManager::currentNM(); SkolemManager* sm = nm->getSkolemManager(); Assert(a.getKind() == Kind::SINE); diff --git a/src/theory/arith/nl/transcendental/sine_solver.h b/src/theory/arith/nl/transcendental/sine_solver.h index a0589d108..9a635b7d0 100644 --- a/src/theory/arith/nl/transcendental/sine_solver.h +++ b/src/theory/arith/nl/transcendental/sine_solver.h @@ -60,9 +60,9 @@ class SineSolver : protected EnvObj void doReductions(); /** * Introduces new_a as purified version of a which is also shifted to the main - * phase (from -pi to pi). y is the new skolem used for purification. + * phase (from -pi to pi). new_a[0] is the new skolem used for purification. */ - void doPhaseShift(TNode a, TNode new_a, TNode y); + void doPhaseShift(TNode a, TNode new_a); /** * check initial refine diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp index 262298772..94aaaf0a0 100644 --- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp @@ -20,7 +20,6 @@ #include "expr/node_algorithm.h" #include "expr/node_builder.h" -#include "expr/skolem_manager.h" #include "options/arith_options.h" #include "theory/arith/arith_msum.h" #include "theory/arith/arith_state.h" @@ -70,27 +69,25 @@ void TranscendentalSolver::initLastCall(const std::vector& xts) return; } - NodeManager* nm = NodeManager::currentNM(); - SkolemManager* sm = nm->getSkolemManager(); for (const Node& a : needsMaster) { - // should not have processed this already - 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); - 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); + Node new_a = d_tstate.getPurifiedForm(a); + // Check if the transcental function application is equal to its purified + // form, if so, we already processed the lemma. In rare cases, note that + // we may require sending a lemma here even if the purified form above had + // already been allocated, e.g. in the case that the purification lemma + // below was dropped. + if (d_astate.areEqual(a, new_a)) + { + // already processed + continue; + } switch (k) { - case Kind::SINE: d_sineSlv.doPhaseShift(a, new_a, y); break; - case Kind::EXPONENTIAL: d_expSlv.doPurification(a, new_a, y); break; + case Kind::SINE: d_sineSlv.doPhaseShift(a, new_a); break; + case Kind::EXPONENTIAL: d_expSlv.doPurification(a, new_a); break; default: AlwaysAssert(false) << "Unexpected Kind " << k; } } diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp index c33ed5ef1..9704957ac 100644 --- a/src/theory/arith/nl/transcendental/transcendental_state.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp @@ -15,6 +15,7 @@ #include "theory/arith/nl/transcendental/transcendental_state.h" +#include "expr/skolem_manager.h" #include "proof/proof.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/inference_manager.h" @@ -110,18 +111,18 @@ void TranscendentalState::init(const std::vector& xts, } } } - if (!consider) - { - // must assign a purified term - needsPurify.push_back(a); - } - else + if (consider) { // assume own purified d_trPurify[a] = a; d_trPurifies[a] = a; } } + if (!consider) + { + // must assign a purified term + needsPurify.push_back(a); + } if (ak == Kind::EXPONENTIAL || ak == Kind::SINE) { needPi = needPi || (ak == Kind::SINE); @@ -454,6 +455,27 @@ bool TranscendentalState::isPurified(TNode n) const return d_trPurifies.find(n) != d_trPurifies.end(); } +Node TranscendentalState::getPurifiedForm(TNode n) +{ + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); + NodeMap::const_iterator it = d_trPurify.find(n); + if (it != d_trPurify.end()) + { + return it->second; + } + Kind k = n.getKind(); + Assert(k == Kind::SINE || k == Kind::EXPONENTIAL); + Node y = sm->mkSkolemFunction( + SkolemFunId::TRANSCENDENTAL_PURIFY_ARG, nm->realType(), n); + Node new_n = nm->mkNode(k, y); + d_trPurify[n] = new_n; + d_trPurify[new_n] = new_n; + d_trPurifies[new_n] = n; + d_trPurifyVars.insert(y); + return new_n; +} + bool TranscendentalState::addModelBoundForPurifyTerm(TNode n, TNode l, TNode u) { Assert(d_funcCongClass.find(n) != d_funcCongClass.end()); diff --git a/src/theory/arith/nl/transcendental/transcendental_state.h b/src/theory/arith/nl/transcendental/transcendental_state.h index 31f7731af..3cb1790d4 100644 --- a/src/theory/arith/nl/transcendental/transcendental_state.h +++ b/src/theory/arith/nl/transcendental/transcendental_state.h @@ -167,6 +167,8 @@ class TranscendentalState : protected EnvObj * Is term t purified? (See d_trPurify below). */ bool isPurified(TNode n) const; + /** get the purified form of node n */ + Node getPurifiedForm(TNode n); /** * Add bound for n, and for what (if anything) it purifies */ diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 4171925fc..a773241b5 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -789,6 +789,9 @@ set(regress_0_tests regress0/nl/nta/exp-n0.5-ub.smt2 regress0/nl/nta/exp-neg2-unsat-unsound.smt2 regress0/nl/nta/exp1-ub.smt2 + regress0/nl/nta/issue4693-inc-purify.smt2 + regress0/nl/nta/issue4693-4-inc-purify-sat.smt2 + regress0/nl/nta/issue4693-5-inc-purify.smt2 regress0/nl/nta/issue7938-tf-model.smt2 regress0/nl/nta/issue8147-unc-model.smt2 regress0/nl/nta/issue8160-model-purify.smt2 diff --git a/test/regress/regress0/nl/nta/issue4693-4-inc-purify-sat.smt2 b/test/regress/regress0/nl/nta/issue4693-4-inc-purify-sat.smt2 new file mode 100644 index 000000000..1b3ad0ab7 --- /dev/null +++ b/test/regress/regress0/nl/nta/issue4693-4-inc-purify-sat.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: -i -q --no-debug-check-models +; EXPECT: sat +; EXPECT: sat +(set-logic ALL) +(declare-const v0 Bool) +(declare-const v7 Bool) +(declare-const v12 Bool) +(declare-const r11 Real) +(declare-const bv_17-0 (_ BitVec 17)) +(declare-const r14 Real) +(assert (xor (>= 98766.0 (cos r11) r14) v12 (= #x1e #x1e #x1e) v0 (= (concat (bvxor (_ bv860 10) (_ bv860 10) (_ bv860 10)) bv_17-0) (concat (bvxor (_ bv860 10) (_ bv860 10) (_ bv860 10)) bv_17-0) (concat (bvxor (_ bv860 10) (_ bv860 10) (_ bv860 10)) bv_17-0)) v7)) +(push 1) +(check-sat) +(pop 1) +(check-sat) diff --git a/test/regress/regress0/nl/nta/issue4693-5-inc-purify.smt2 b/test/regress/regress0/nl/nta/issue4693-5-inc-purify.smt2 new file mode 100644 index 000000000..730db4b23 --- /dev/null +++ b/test/regress/regress0/nl/nta/issue4693-5-inc-purify.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: -q +; EXPECT: unsat +(set-logic ALL) +(set-info :status unsat) +(assert (forall ((t Real)) (= 0 (/ t (cos 1.0))))) +(check-sat) diff --git a/test/regress/regress0/nl/nta/issue4693-inc-purify.smt2 b/test/regress/regress0/nl/nta/issue4693-inc-purify.smt2 new file mode 100644 index 000000000..b9e8e61bf --- /dev/null +++ b/test/regress/regress0/nl/nta/issue4693-inc-purify.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: -i -q +; EXPECT: unsat +; EXPECT: unsat +(set-logic QF_NRAT) +(declare-const r0 Real) +(assert (! (>= (sin 97111.0) r0 r0 r0 97111.0) :named IP_3)) +(push 1) +(check-sat) +(pop 1) +(check-sat)