From: Andrew Reynolds Date: Thu, 19 Nov 2020 17:44:35 +0000 (-0600) Subject: Fix issues related to eliminating extended arithmetic operators (#5475) X-Git-Tag: cvc5-1.0.0~2581 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3654512dd8b341c5725e550d438b23508493b991;p=cvc5.git Fix issues related to eliminating extended arithmetic operators (#5475) This fixes 2 issues related to eliminating arithmetic operators: (1) counterexample lemmas in CEGQI were not being preprocessed (2) ensureLiteral was not doing term formula removal. This corrects these two issues. Now ensureLiteral does full theory preprocessing on the term we are ensuring literal for, meaning this may trigger lemmas if the term contains extended arithmetic operators like div. Fixes #5469, fixes #5470, fixes #5471. This adds --sygus-inst to 2 of these benchmarks which moreover makes them solvable. This also improves our assertions and trace messages. --- 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::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 newLemmas; + std::vector 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)