diff options
Diffstat (limited to 'src/theory')
-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 |
4 files changed, 38 insertions, 2 deletions
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 |