summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/arith/theory_arith.cpp10
-rw-r--r--src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp3
-rw-r--r--src/theory/theory_engine.cpp15
-rw-r--r--src/theory/theory_engine.h5
-rw-r--r--src/theory/theory_preprocessor.cpp49
-rw-r--r--test/regress/CMakeLists.txt3
-rw-r--r--test/regress/regress1/quantifiers/issue5469-aext.smt210
-rw-r--r--test/regress/regress1/quantifiers/issue5470-aext.smt26
-rw-r--r--test/regress/regress1/quantifiers/issue5471-aext.smt210
9 files changed, 77 insertions, 34 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index c77e64221..b5c0d1bd0 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -154,10 +154,15 @@ void TheoryArith::ppStaticLearn(TNode n, NodeBuilder<>& learned) {
d_internal->ppStaticLearn(n, learned);
}
-bool TheoryArith::preCheck(Effort level) { return d_internal->preCheck(level); }
+bool TheoryArith::preCheck(Effort level)
+{
+ Trace("arith-check") << "TheoryArith::preCheck " << level << std::endl;
+ return d_internal->preCheck(level);
+}
void TheoryArith::postCheck(Effort level)
{
+ Trace("arith-check") << "TheoryArith::postCheck " << level << std::endl;
// check with the non-linear solver at last call
if (level == Theory::EFFORT_LAST_CALL)
{
@@ -191,6 +196,9 @@ void TheoryArith::postCheck(Effort level)
bool TheoryArith::preNotifyFact(
TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
{
+ Trace("arith-check") << "TheoryArith::preNotifyFact: " << fact
+ << ", isPrereg=" << isPrereg
+ << ", isInternal=" << isInternal << std::endl;
d_internal->preNotifyFact(atom, pol, fact);
// We do not assert to the equality engine of arithmetic in the standard way,
// hence we return "true" to indicate we are finished with this fact.
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 3bf3cc425..561817aa8 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -603,7 +603,8 @@ void InstStrategyCegqi::registerCounterexampleLemma(Node q, Node lem)
ce_vars.push_back(tutil->getInstantiationConstant(q, i));
}
CegInstantiator* cinst = getInstantiator(q);
- LemmaStatus status = d_quantEngine->getOutputChannel().lemma(lem);
+ LemmaStatus status =
+ d_quantEngine->getOutputChannel().lemma(lem, LemmaProperty::PREPROCESS);
Node ppLem = status.getRewrittenLemma();
Trace("cegqi-debug") << "Counterexample lemma (post-preprocess): " << ppLem
<< std::endl;
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 3a155b9ad..d54538049 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -312,6 +312,8 @@ void TheoryEngine::preRegister(TNode preprocessed) {
Debug("theory") << "TheoryEngine::preRegister: " << preprocessed
<< std::endl;
Assert(!expr::hasFreeVar(preprocessed));
+ // should not have witness
+ Assert(!expr::hasSubtermKind(kind::WITNESS, preprocessed));
// Pre-register the terms in the atom
theory::TheoryIdSet theories = NodeVisitor<PreRegisterVisitor>::run(
@@ -1172,8 +1174,15 @@ Node TheoryEngine::ensureLiteral(TNode n) {
Debug("ensureLiteral") << "rewriting: " << n << std::endl;
Node rewritten = Rewriter::rewrite(n);
Debug("ensureLiteral") << " got: " << rewritten << std::endl;
- TrustNode tp = preprocess(rewritten);
- Node preprocessed = tp.isNull() ? rewritten : tp.getNode();
+ std::vector<TrustNode> newLemmas;
+ std::vector<Node> newSkolems;
+ TrustNode tpn = d_tpp.preprocess(n, newLemmas, newSkolems, true);
+ // send lemmas corresponding to the skolems introduced by preprocessing n
+ for (const TrustNode& tnl : newLemmas)
+ {
+ lemma(tnl, LemmaProperty::NONE);
+ }
+ Node preprocessed = tpn.isNull() ? rewritten : tpn.getNode();
Debug("ensureLiteral") << "preprocessed: " << preprocessed << std::endl;
d_propEngine->ensureLiteral(preprocessed);
return preprocessed;
@@ -1417,6 +1426,8 @@ theory::LemmaStatus TheoryEngine::lemma(theory::TrustNode tlemma,
Node node = tlemma.getNode();
Node lemma = tlemma.getProven();
+ Assert(!expr::hasFreeVar(lemma));
+
// when proofs are enabled, we ensure the trust node has a generator by
// adding a trust step to the lazy proof maintained by this class
if (isProofEnabled())
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 088e413bb..ee3611a53 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -663,7 +663,9 @@ class TheoryEngine {
Node getModelValue(TNode var);
/**
- * Takes a literal and returns an equivalent literal that is guaranteed to be a SAT literal
+ * Takes a literal and returns an equivalent literal that is guaranteed to be
+ * a SAT literal. This rewrites and preprocesses n, which notice may involve
+ * sending lemmas if preprocessing n involves introducing new skolems.
*/
Node ensureLiteral(TNode n);
@@ -746,7 +748,6 @@ private:
* This function is called from the smt engine's checkModel routine.
*/
void checkTheoryAssertionsWithModel(bool hardFailure);
-
private:
IntStat d_arithSubstitutionsAdded;
};/* class TheoryEngine */
diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp
index 42ac074ce..9ebf12577 100644
--- a/src/theory/theory_preprocessor.cpp
+++ b/src/theory/theory_preprocessor.cpp
@@ -89,9 +89,9 @@ TrustNode TheoryPreprocessor::preprocess(TNode node,
{
// In this method, all rewriting steps of node are stored in d_tpg.
- Trace("tpp-proof-debug") << "TheoryPreprocessor::preprocess: start " << node
- << ", doTheoryPreprocess=" << doTheoryPreprocess
- << std::endl;
+ Trace("tpp-debug") << "TheoryPreprocessor::preprocess: start " << node
+ << ", doTheoryPreprocess=" << doTheoryPreprocess
+ << std::endl;
// Run theory preprocessing, maybe
Node ppNode = node;
if (doTheoryPreprocess)
@@ -121,23 +121,21 @@ TrustNode TheoryPreprocessor::preprocess(TNode node,
// in d_tpg, which maintains the fact that d_tpg can prove the rewrite.
Node retNode = rewriteWithProof(rtfNode);
- if (Trace.isOn("tpp-proof-debug"))
+ if (Trace.isOn("tpp-debug"))
{
if (node != ppNode)
{
- Trace("tpp-proof-debug")
- << "after preprocessing : " << ppNode << std::endl;
+ Trace("tpp-debug") << "after preprocessing : " << ppNode << std::endl;
}
if (rtfNode != ppNode)
{
- Trace("tpp-proof-debug") << "after rtf : " << rtfNode << std::endl;
+ Trace("tpp-debug") << "after rtf : " << rtfNode << std::endl;
}
if (retNode != rtfNode)
{
- Trace("tpp-proof-debug") << "after rewriting : " << retNode << std::endl;
+ Trace("tpp-debug") << "after rewriting : " << retNode << std::endl;
}
- Trace("tpp-proof-debug")
- << "TheoryPreprocessor::preprocess: finish" << std::endl;
+ Trace("tpp-debug") << "TheoryPreprocessor::preprocess: finish" << std::endl;
}
if (node == retNode)
{
@@ -177,7 +175,7 @@ TrustNode TheoryPreprocessor::preprocess(TNode node,
// we wil use the sequence generator
tret = d_tspg->mkTrustRewriteSequence(cterms);
}
- tret.debugCheckClosed("tpp-proof-debug", "TheoryPreprocessor::lemma_ret");
+ tret.debugCheckClosed("tpp-debug", "TheoryPreprocessor::lemma_ret");
}
else
{
@@ -185,14 +183,14 @@ TrustNode TheoryPreprocessor::preprocess(TNode node,
}
// now, rewrite the lemmas
- Trace("tpp-proof-debug") << "TheoryPreprocessor::preprocess: process lemmas"
- << std::endl;
+ Trace("tpp-debug") << "TheoryPreprocessor::preprocess: process lemmas"
+ << std::endl;
for (size_t i = 0, lsize = newLemmas.size(); i < lsize; ++i)
{
// get the trust node to process
TrustNode trn = newLemmas[i];
trn.debugCheckClosed(
- "tpp-proof-debug", "TheoryPreprocessor::lemma_new_initial", false);
+ "tpp-debug", "TheoryPreprocessor::lemma_new_initial", false);
Assert(trn.getKind() == TrustNodeKind::LEMMA);
Node assertion = trn.getNode();
// rewrite, which is independent of d_tpg, since additional lemmas
@@ -217,11 +215,9 @@ TrustNode TheoryPreprocessor::preprocess(TNode node,
newLemmas[i] = TrustNode::mkTrustLemma(rewritten, d_lp.get());
}
Assert(!isProofEnabled() || newLemmas[i].getGenerator() != nullptr);
- newLemmas[i].debugCheckClosed("tpp-proof-debug",
- "TheoryPreprocessor::lemma_new");
+ newLemmas[i].debugCheckClosed("tpp-debug", "TheoryPreprocessor::lemma_new");
}
- Trace("tpp-proof-debug") << "Preprocessed: " << node << " " << retNode
- << std::endl;
+ Trace("tpp-debug") << "Preprocessed: " << node << " " << retNode << std::endl;
return tret;
}
@@ -390,9 +386,8 @@ Node TheoryPreprocessor::rewriteWithProof(Node term)
// may rewrite the same term more than once, thus check hasRewriteStep
if (termr != term)
{
- Trace("tpp-proof-debug")
- << "TheoryPreprocessor: addRewriteStep (rewriting) " << term << " -> "
- << termr << std::endl;
+ Trace("tpp-debug") << "TheoryPreprocessor: addRewriteStep (rewriting) "
+ << term << " -> " << termr << std::endl;
// always use term context hash 0 (default)
d_tpg->addRewriteStep(term, termr, PfRule::REWRITE, {}, {term});
}
@@ -420,10 +415,9 @@ Node TheoryPreprocessor::preprocessWithProof(Node term)
{
if (trn.getGenerator() != nullptr)
{
- Trace("tpp-proof-debug")
- << "TheoryPreprocessor: addRewriteStep (generator) " << term << " -> "
- << termr << std::endl;
- trn.debugCheckClosed("tpp-proof-debug",
+ Trace("tpp-debug") << "TheoryPreprocessor: addRewriteStep (generator) "
+ << term << " -> " << termr << std::endl;
+ trn.debugCheckClosed("tpp-debug",
"TheoryPreprocessor::preprocessWithProof");
// always use term context hash 0 (default)
d_tpg->addRewriteStep(
@@ -431,9 +425,8 @@ Node TheoryPreprocessor::preprocessWithProof(Node term)
}
else
{
- Trace("tpp-proof-debug")
- << "TheoryPreprocessor: addRewriteStep (trusted) " << term << " -> "
- << termr << std::endl;
+ Trace("tpp-debug") << "TheoryPreprocessor: addRewriteStep (trusted) "
+ << term << " -> " << termr << std::endl;
// small step trust
d_tpg->addRewriteStep(
term, termr, PfRule::THEORY_PREPROCESS, {}, {term.eqNode(termr)});
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index b12876a5c..9935adf59 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1609,6 +1609,9 @@ set(regress_1_tests
regress1/quantifiers/issue4620-erq-witness-unsound.smt2
regress1/quantifiers/issue4685-wrewrite.smt2
regress1/quantifiers/issue5019-cegqi-i.smt2
+ regress1/quantifiers/issue5469-aext.smt2
+ regress1/quantifiers/issue5470-aext.smt2
+ regress1/quantifiers/issue5471-aext.smt2
regress1/quantifiers/issue993.smt2
regress1/quantifiers/javafe.ast.StmtVec.009.smt2
regress1/quantifiers/lia-witness-div-pp.smt2
diff --git a/test/regress/regress1/quantifiers/issue5469-aext.smt2 b/test/regress/regress1/quantifiers/issue5469-aext.smt2
new file mode 100644
index 000000000..d66afb91a
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue5469-aext.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --sygus-inst --strings-exp --no-check-models
+; EXPECT: sat
+(set-logic NIA)
+(set-option :sygus-inst true)
+(set-option :strings-exp true)
+(set-info :status sat)
+(declare-fun d () Int)
+(assert (forall ((g Int)) (or (> 1 g) (> g (div 1 d)))))
+(assert (not (= d 0)))
+(check-sat)
diff --git a/test/regress/regress1/quantifiers/issue5470-aext.smt2 b/test/regress/regress1/quantifiers/issue5470-aext.smt2
new file mode 100644
index 000000000..500ef6d4c
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue5470-aext.smt2
@@ -0,0 +1,6 @@
+(set-logic NIA)
+(set-option :strings-exp true)
+(set-info :status sat)
+(declare-fun b () Int)
+(assert (exists ((c Int)) (< 0 c (div 0 b))))
+(check-sat)
diff --git a/test/regress/regress1/quantifiers/issue5471-aext.smt2 b/test/regress/regress1/quantifiers/issue5471-aext.smt2
new file mode 100644
index 000000000..c420359fc
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue5471-aext.smt2
@@ -0,0 +1,10 @@
+(set-logic NRA)
+(set-option :sygus-inst true)
+(set-option :strings-exp true)
+(set-info :status unsat)
+(declare-fun a () Real)
+(declare-fun b () Real)
+(declare-fun c () Real)
+(assert (forall ((d Real)) (= (> d 0) (<= (+ d (/ a c)) 0))))
+(assert (<= (* b b) 0))
+(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback