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.
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;
/**
* 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
}
}
-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);
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
#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"
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;
}
}
#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"
}
}
}
- 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);
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());
* 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
*/
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
--- /dev/null
+; 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)
--- /dev/null
+; COMMAND-LINE: -q
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+(assert (forall ((t Real)) (= 0 (/ t (cos 1.0)))))
+(check-sat)
--- /dev/null
+; 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)
projects / cvc5.git / commitdiff