diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-19 11:44:35 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-19 11:44:35 -0600 |
| commit | 3654512dd8b341c5725e550d438b23508493b991 (patch) | |
| tree | 367684e5521e35a452ef669a4e58bb1b5005509c /src/theory/theory_engine.cpp | |
| parent | b0130a1e032c201fab3c4b19f25871428b761967 (diff) | |
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.
Diffstat (limited to 'src/theory/theory_engine.cpp')
| -rw-r--r-- | src/theory/theory_engine.cpp | 15 |
1 files changed, 13 insertions, 2 deletions
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()) |