diff options
Diffstat (limited to 'src/theory/valuation.h')
| -rw-r--r-- | src/theory/valuation.h | 19 |
1 files changed, 19 insertions, 0 deletions
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 |