diff options
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()) |