diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-01-24 11:42:08 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-01-24 11:42:08 -0600 |
| commit | 1d49bcb407777cf177620dac4d8e4df82f5e1122 (patch) | |
| tree | 00ea9256957d8547519b7164d10344d7313e56c8 /src/theory/valuation.h | |
| parent | 109e7e43efdeb557ff17880da83da438db35eb3e (diff) | |
Add interface for getting preprocessed term (#5798)
Several places, e.g. in quantifiers, requiring knowing what the theory-preprocessed form of a node is.
This is required for an improvement to our E-matching algorithm, which requires knowing what the preprocessed form of ground subterms of triggers are.
Note that I'm not 100% happy with adding a new interface to Valuation, but at the moment I don't see a better way of doing this. On the positive side, this interface will make a few other things (e.g. the return value of OutputChannel::lemma) obsolete.
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 |