diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/prop/prop_engine.cpp | 17 | ||||
-rw-r--r-- | src/prop/prop_engine.h | 6 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 5 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 10 | ||||
-rw-r--r-- | src/theory/valuation.cpp | 6 | ||||
-rw-r--r-- | src/theory/valuation.h | 19 |
6 files changed, 55 insertions, 8 deletions
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 384734100..2fa62d9f6 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -427,6 +427,16 @@ void PropEngine::getBooleanVariables(std::vector<TNode>& outputVariables) const Node PropEngine::ensureLiteral(TNode n) { // must preprocess + Node preprocessed = getPreprocessedTerm(n); + Trace("ensureLiteral") << "ensureLiteral preprocessed: " << preprocessed + << std::endl; + d_cnfStream->ensureLiteral(preprocessed); + return preprocessed; +} + +Node PropEngine::getPreprocessedTerm(TNode n) +{ + // must preprocess std::vector<theory::TrustNode> newLemmas; std::vector<Node> newSkolems; theory::TrustNode tpn = @@ -434,14 +444,9 @@ Node PropEngine::ensureLiteral(TNode n) // send lemmas corresponding to the skolems introduced by preprocessing n for (const theory::TrustNode& tnl : newLemmas) { - Trace("ensureLiteral") << " lemma: " << tnl.getNode() << std::endl; assertLemma(tnl, theory::LemmaProperty::NONE); } - Node preprocessed = tpn.isNull() ? Node(n) : tpn.getNode(); - Trace("ensureLiteral") << "ensureLiteral preprocessed: " << preprocessed - << std::endl; - d_cnfStream->ensureLiteral(preprocessed); - return preprocessed; + return tpn.isNull() ? Node(n) : tpn.getNode(); } void PropEngine::push() diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 453c1c2af..8086a427e 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -190,6 +190,12 @@ class PropEngine * via getSatValue(). */ Node ensureLiteral(TNode n); + /** + * This returns the theory-preprocessed form of term n. This rewrites and + * preprocesses n, which notice may involve adding clauses to the SAT solver + * if preprocessing n involves introducing new skolems. + */ + Node getPreprocessedTerm(TNode n); /** * Push the context level. diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 5206ed7ae..27ae0018e 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1174,6 +1174,11 @@ Node TheoryEngine::ensureLiteral(TNode n) { return d_propEngine->ensureLiteral(rewritten); } +Node TheoryEngine::getPreprocessedTerm(TNode n) +{ + Node rewritten = Rewriter::rewrite(n); + return d_propEngine->getPreprocessedTerm(rewritten); +} void TheoryEngine::printInstantiations( std::ostream& out ) { if( d_quantEngine ){ diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 41f8372a9..df57d9903 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -654,10 +654,16 @@ class TheoryEngine { /** * 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. + * adding clauses to the SAT solver if preprocessing n involves introducing + * new skolems. */ Node ensureLiteral(TNode n); - + /** + * This returns the theory-preprocessed form of term n. This rewrites and + * preprocesses n, which notice may involve adding clauses to the SAT solver + * if preprocessing n involves introducing new skolems. + */ + Node getPreprocessedTerm(TNode n); /** * Print all instantiations made by the quantifiers module. */ diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp index ad6ee9fdf..b8ee5d41c 100644 --- a/src/theory/valuation.cpp +++ b/src/theory/valuation.cpp @@ -159,6 +159,12 @@ Node Valuation::ensureLiteral(TNode n) { return d_engine->ensureLiteral(n); } +Node Valuation::getPreprocessedTerm(TNode n) +{ + Assert(d_engine != nullptr); + return d_engine->getPreprocessedTerm(n); +} + bool Valuation::isDecision(Node lit) const { Assert(d_engine != nullptr); return d_engine->getPropEngine()->isDecision(lit); diff --git a/src/theory/valuation.h b/src/theory/valuation.h index 01b33eb99..065556872 100644 --- a/src/theory/valuation.h +++ b/src/theory/valuation.h @@ -135,6 +135,9 @@ public: * that is definitionally equal to it. The result of this function * is a Node that can be queried via getSatValue(). * + * Note that this call may add lemmas to the SAT solver corresponding to the + * definition of subterms eliminated by preprocessing. + * * @return the actual node that's been "literalized," which may * differ from the input due to theory-rewriting and preprocessing, * as well as CNF conversion @@ -142,6 +145,22 @@ public: Node ensureLiteral(TNode n) CVC4_WARN_UNUSED_RESULT; /** + * This returns the theory-preprocessed form of term n. The theory + * preprocessed form of a term t is one returned by + * TheoryPreprocess::preprocess (see theory/theory_preprocess.h). In + * particular, the returned term has syntax sugar symbols eliminated + * (e.g. div, mod, partial datatype selectors), has term formulas (e.g. ITE + * terms eliminated) and has been rewritten. + * + * Note that this call may add lemmas to the SAT solver corresponding to the + * definition of subterms eliminated by preprocessing. + * + * @param n The node to preprocess + * @return The preprocessed form of n + */ + Node getPreprocessedTerm(TNode n); + + /** * Returns whether the given lit (which must be a SAT literal) is a decision * literal or not. Throws an exception if lit is not a SAT literal. "lit" may * be in either phase; that is, if "lit" is a SAT literal, this function returns |