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/prop | |
| 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/prop')
| -rw-r--r-- | src/prop/prop_engine.cpp | 17 | ||||
| -rw-r--r-- | src/prop/prop_engine.h | 6 |
2 files changed, 17 insertions, 6 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. |