summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/prop/prop_engine.cpp51
-rw-r--r--src/prop/prop_engine.h17
-rw-r--r--src/prop/theory_proxy.cpp14
-rw-r--r--src/prop/theory_proxy.h11
-rw-r--r--src/smt/term_formula_removal.cpp23
-rw-r--r--src/smt/term_formula_removal.h8
-rw-r--r--src/theory/combination_care_graph.cpp2
-rw-r--r--src/theory/combination_engine.cpp1
-rw-r--r--src/theory/combination_engine.h3
-rw-r--r--src/theory/engine_output_channel.cpp28
-rw-r--r--src/theory/engine_output_channel.h9
-rw-r--r--src/theory/fp/theory_fp.cpp3
-rw-r--r--src/theory/output_channel.cpp16
-rw-r--r--src/theory/output_channel.h35
-rw-r--r--src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp15
-rw-r--r--src/theory/theory_engine.cpp35
-rw-r--r--src/theory/theory_engine.h24
-rw-r--r--src/theory/theory_test_utils.h14
-rw-r--r--src/theory/valuation.cpp12
-rw-r--r--src/theory/valuation.h7
-rw-r--r--test/unit/theory/theory_engine_white.h5
-rw-r--r--test/unit/theory/theory_white.h9
22 files changed, 164 insertions, 178 deletions
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index fb43ebe73..28159c229 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -36,6 +36,7 @@
#include "prop/theory_proxy.h"
#include "smt/smt_statistics_registry.h"
#include "theory/output_channel.h"
+#include "theory/rewriter.h"
#include "theory/theory_engine.h"
#include "util/resource_manager.h"
#include "util/result.h"
@@ -206,7 +207,7 @@ void PropEngine::assertFormula(TNode node) {
}
}
-Node PropEngine::assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p)
+void PropEngine::assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p)
{
bool removable = isLemmaPropertyRemovable(p);
@@ -261,20 +262,6 @@ Node PropEngine::assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p)
}
d_decisionEngine->addAssertions(assertions, ppLemmasF, ppSkolems);
}
-
- // make the return lemma, which the theory engine will use
- Node retLemma = tplemma.getProven();
- if (!ppLemmas.empty())
- {
- std::vector<Node> lemmas{retLemma};
- for (const theory::TrustNode& tnl : ppLemmas)
- {
- lemmas.push_back(tnl.getProven());
- }
- // the returned lemma is the conjunction of all additional lemmas.
- retLemma = NodeManager::currentNM()->mkNode(kind::AND, lemmas);
- }
- return retLemma;
}
void PropEngine::assertLemmaInternal(theory::TrustNode trn, bool removable)
@@ -441,6 +428,7 @@ Node PropEngine::ensureLiteral(TNode n)
Node PropEngine::getPreprocessedTerm(TNode n)
{
+ Node rewritten = theory::Rewriter::rewrite(n);
// must preprocess
std::vector<theory::TrustNode> newLemmas;
std::vector<Node> newSkolems;
@@ -453,6 +441,39 @@ Node PropEngine::getPreprocessedTerm(TNode n)
return tpn.isNull() ? Node(n) : tpn.getNode();
}
+Node PropEngine::getPreprocessedTerm(TNode n,
+ std::vector<Node>& skAsserts,
+ std::vector<Node>& sks)
+{
+ // get the preprocessed form of the term
+ Node pn = getPreprocessedTerm(n);
+ // initialize the set of skolems and assertions to process
+ std::vector<theory::TrustNode> toProcessAsserts;
+ std::vector<Node> toProcess;
+ d_theoryProxy->getSkolems(pn, toProcessAsserts, toProcess);
+ size_t index = 0;
+ // until fixed point is reached
+ while (index < toProcess.size())
+ {
+ theory::TrustNode ka = toProcessAsserts[index];
+ Node k = toProcess[index];
+ index++;
+ if (std::find(sks.begin(), sks.end(), k) != sks.end())
+ {
+ // already added the skolem to the list
+ continue;
+ }
+ // must preprocess lemmas as well
+ Node kap = getPreprocessedTerm(ka.getProven());
+ skAsserts.push_back(kap);
+ sks.push_back(k);
+ // get the skolems in the preprocessed form of the lemma ka
+ d_theoryProxy->getSkolems(kap, toProcessAsserts, toProcess);
+ }
+ // return the preprocessed term
+ return pn;
+}
+
void PropEngine::push()
{
Assert(!d_inCheckSat) << "Sat solver in solve()!";
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 493dbfe01..f7561d945 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -145,9 +145,8 @@ class PropEngine
*
* @param trn the trust node storing the formula to assert
* @param p the properties of the lemma
- * @return the (preprocessed) lemma
*/
- Node assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p);
+ void assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p);
/**
* If ever n is decided upon, it must be in the given phase. This
@@ -209,6 +208,20 @@ class PropEngine
* if preprocessing n involves introducing new skolems.
*/
Node getPreprocessedTerm(TNode n);
+ /**
+ * Same as above, but also compute the skolems in n and in the lemmas
+ * corresponding to their definition.
+ *
+ * Note this will include skolems that occur in the definition lemma
+ * for all skolems in sks. This is run until a fixed point is reached.
+ * For example, if k1 has definition (ite A (= k1 k2) (= k1 x)) where k2 is
+ * another skolem introduced by term formula removal, then calling this
+ * method on (P k1) will include both k1 and k2 in sks, and their definitions
+ * in skAsserts.
+ */
+ Node getPreprocessedTerm(TNode n,
+ std::vector<Node>& skAsserts,
+ std::vector<Node>& sks);
/**
* Push the context level.
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index c604c47f7..a6d570bc2 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -194,6 +194,20 @@ theory::TrustNode TheoryProxy::removeItes(
return rtf.run(node, newLemmas, newSkolems, true);
}
+void TheoryProxy::getSkolems(TNode node,
+ std::vector<theory::TrustNode>& skAsserts,
+ std::vector<Node>& sks)
+{
+ RemoveTermFormulas& rtf = d_tpp.getRemoveTermFormulas();
+ std::unordered_set<Node, NodeHashFunction> skolems;
+ rtf.getSkolems(node, skolems);
+ for (const Node& k : skolems)
+ {
+ sks.push_back(k);
+ skAsserts.push_back(rtf.getLemmaForSkolem(k));
+ }
+}
+
void TheoryProxy::preRegister(Node n) { d_theoryEngine->preRegister(n); }
}/* CVC4::prop namespace */
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index 57115d660..ac79cf967 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -118,6 +118,17 @@ class TheoryProxy : public Registrar
theory::TrustNode removeItes(TNode node,
std::vector<theory::TrustNode>& newLemmas,
std::vector<Node>& newSkolems);
+ /**
+ * Get the skolems within node and their corresponding definitions, store
+ * them in sks and skAsserts respectively. Note that this method does not
+ * necessary include all of the skolems in skAsserts. In other words, it
+ * collects from node only. To compute all skolems that node depends on
+ * requires calling this method again on each lemma in skAsserts until a
+ * fixed point is reached.
+ */
+ void getSkolems(TNode node,
+ std::vector<theory::TrustNode>& skAsserts,
+ std::vector<Node>& sks);
/** Preregister term */
void preRegister(Node n) override;
diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp
index f77ae7b49..9a856fc14 100644
--- a/src/smt/term_formula_removal.cpp
+++ b/src/smt/term_formula_removal.cpp
@@ -517,21 +517,9 @@ Node RemoveTermFormulas::getSkolemForNode(Node k) const
return Node::null();
}
-bool RemoveTermFormulas::getSkolems(
+void RemoveTermFormulas::getSkolems(
TNode n, std::unordered_set<Node, NodeHashFunction>& skolems) const
{
- // if n was unchanged by term formula removal, just return immediately
- std::pair<Node, uint32_t> initial(n, d_rtfc.initialValue());
- TermFormulaCache::const_iterator itc = d_tfCache.find(initial);
- if (itc != d_tfCache.end())
- {
- if (itc->second == n)
- {
- return false;
- }
- }
- // otherwise, traverse it
- bool ret = false;
std::unordered_set<TNode, TNodeHashFunction> visited;
std::unordered_set<TNode, TNodeHashFunction>::iterator it;
std::vector<TNode> visit;
@@ -549,16 +537,15 @@ bool RemoveTermFormulas::getSkolems(
{
if (d_lemmaCache.find(cur) != d_lemmaCache.end())
{
- // technically could already be in skolems if skolems was non-empty,
- // regardless set return value to true.
skolems.insert(cur);
- ret = true;
}
}
- visit.insert(visit.end(), cur.begin(), cur.end());
+ else
+ {
+ visit.insert(visit.end(), cur.begin(), cur.end());
+ }
}
} while (!visit.empty());
- return ret;
}
Node RemoveTermFormulas::getAxiomFor(Node n)
diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h
index ac2644182..0c026a5fe 100644
--- a/src/smt/term_formula_removal.h
+++ b/src/smt/term_formula_removal.h
@@ -130,12 +130,10 @@ class RemoveTermFormulas {
* Get the set of skolems introduced by this class that occur in node n,
* add them to skolems.
*
- * This method uses an optimization that returns false immediately if n
- * was unchanged by term formula removal, based on the initial context.
- *
- * Return true if any nodes were added to skolems.
+ * @param n The node to traverse
+ * @param skolems The set where the skolems are added
*/
- bool getSkolems(TNode n,
+ void getSkolems(TNode n,
std::unordered_set<Node, NodeHashFunction>& skolems) const;
/**
diff --git a/src/theory/combination_care_graph.cpp b/src/theory/combination_care_graph.cpp
index 45a709d19..402eeeb26 100644
--- a/src/theory/combination_care_graph.cpp
+++ b/src/theory/combination_care_graph.cpp
@@ -85,7 +85,7 @@ void CombinationCareGraph::combineTheories()
// This is supposed to force preference to follow what the theory models
// already have but it doesn't seem to make a big difference - need to
// explore more -Clark
- Node e = d_te.ensureLiteral(equality);
+ Node e = d_valuation.ensureLiteral(equality);
propEngine->requirePhase(e, true);
}
}
diff --git a/src/theory/combination_engine.cpp b/src/theory/combination_engine.cpp
index 71eac49a0..21450df04 100644
--- a/src/theory/combination_engine.cpp
+++ b/src/theory/combination_engine.cpp
@@ -28,6 +28,7 @@ CombinationEngine::CombinationEngine(TheoryEngine& te,
const std::vector<Theory*>& paraTheories,
ProofNodeManager* pnm)
: d_te(te),
+ d_valuation(&te),
d_pnm(pnm),
d_logicInfo(te.getLogicInfo()),
d_paraTheories(paraTheories),
diff --git a/src/theory/combination_engine.h b/src/theory/combination_engine.h
index 765a49d68..5bc9d7bdd 100644
--- a/src/theory/combination_engine.h
+++ b/src/theory/combination_engine.h
@@ -24,6 +24,7 @@
#include "theory/ee_manager.h"
#include "theory/model_manager.h"
#include "theory/shared_solver.h"
+#include "theory/valuation.h"
namespace CVC4 {
@@ -104,6 +105,8 @@ class CombinationEngine
void sendLemma(TrustNode trn, TheoryId atomsTo);
/** Reference to the theory engine */
TheoryEngine& d_te;
+ /** Valuation for the engine */
+ Valuation d_valuation;
/** The proof node manager */
ProofNodeManager* d_pnm;
/** Logic info of theory engine (cached) */
diff --git a/src/theory/engine_output_channel.cpp b/src/theory/engine_output_channel.cpp
index 0aa56a381..1105b918b 100644
--- a/src/theory/engine_output_channel.cpp
+++ b/src/theory/engine_output_channel.cpp
@@ -67,7 +67,7 @@ void EngineOutputChannel::safePoint(ResourceManager::Resource r)
}
}
-theory::LemmaStatus EngineOutputChannel::lemma(TNode lemma, LemmaProperty p)
+void EngineOutputChannel::lemma(TNode lemma, LemmaProperty p)
{
Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma("
<< lemma << ")"
@@ -76,15 +76,13 @@ theory::LemmaStatus EngineOutputChannel::lemma(TNode lemma, LemmaProperty p)
d_engine->d_outputChannelUsed = true;
TrustNode tlem = TrustNode::mkTrustLemma(lemma);
- theory::LemmaStatus result = d_engine->lemma(
- tlem,
- p,
- isLemmaPropertySendAtoms(p) ? d_theory : theory::THEORY_LAST,
- d_theory);
- return result;
+ d_engine->lemma(tlem,
+ p,
+ isLemmaPropertySendAtoms(p) ? d_theory : theory::THEORY_LAST,
+ d_theory);
}
-theory::LemmaStatus EngineOutputChannel::splitLemma(TNode lemma, bool removable)
+void EngineOutputChannel::splitLemma(TNode lemma, bool removable)
{
Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma("
<< lemma << ")" << std::endl;
@@ -95,8 +93,7 @@ theory::LemmaStatus EngineOutputChannel::splitLemma(TNode lemma, bool removable)
<< std::endl;
TrustNode tlem = TrustNode::mkTrustLemma(lemma);
LemmaProperty p = removable ? LemmaProperty::REMOVABLE : LemmaProperty::NONE;
- theory::LemmaStatus result = d_engine->lemma(tlem, p, d_theory);
- return result;
+ d_engine->lemma(tlem, p, d_theory);
}
bool EngineOutputChannel::propagate(TNode literal)
@@ -172,7 +169,7 @@ void EngineOutputChannel::trustedConflict(TrustNode pconf)
d_engine->conflict(pconf, d_theory);
}
-LemmaStatus EngineOutputChannel::trustedLemma(TrustNode plem, LemmaProperty p)
+void EngineOutputChannel::trustedLemma(TrustNode plem, LemmaProperty p)
{
Trace("theory::lemma") << "EngineOutputChannel<" << d_theory
<< ">::trustedLemma(" << plem << ")" << std::endl;
@@ -184,11 +181,10 @@ LemmaStatus EngineOutputChannel::trustedLemma(TrustNode plem, LemmaProperty p)
++d_statistics.lemmas;
d_engine->d_outputChannelUsed = true;
// now, call the normal interface for lemma
- return d_engine->lemma(
- plem,
- p,
- isLemmaPropertySendAtoms(p) ? d_theory : theory::THEORY_LAST,
- d_theory);
+ d_engine->lemma(plem,
+ p,
+ isLemmaPropertySendAtoms(p) ? d_theory : theory::THEORY_LAST,
+ d_theory);
}
} // namespace theory
diff --git a/src/theory/engine_output_channel.h b/src/theory/engine_output_channel.h
index 7a59dbf2a..c53feabc5 100644
--- a/src/theory/engine_output_channel.h
+++ b/src/theory/engine_output_channel.h
@@ -48,10 +48,9 @@ class EngineOutputChannel : public theory::OutputChannel
void conflict(TNode conflictNode) override;
bool propagate(TNode literal) override;
- theory::LemmaStatus lemma(TNode lemma,
- LemmaProperty p = LemmaProperty::NONE) override;
+ void lemma(TNode lemma, LemmaProperty p = LemmaProperty::NONE) override;
- theory::LemmaStatus splitLemma(TNode lemma, bool removable = false) override;
+ void splitLemma(TNode lemma, bool removable = false) override;
void demandRestart() override;
@@ -76,8 +75,8 @@ class EngineOutputChannel : public theory::OutputChannel
* by the generator pfg. Apart from pfg, the interface for this method is
* the same as calling OutputChannel::lemma on lem.
*/
- LemmaStatus trustedLemma(TrustNode plem,
- LemmaProperty p = LemmaProperty::NONE) override;
+ void trustedLemma(TrustNode plem,
+ LemmaProperty p = LemmaProperty::NONE) override;
protected:
/**
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 0a8c4ee0e..a71a2d0eb 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -918,9 +918,6 @@ void TheoryFp::handleLemma(Node node) {
Trace("fp") << "TheoryFp::handleLemma(): asserting " << node << std::endl;
// Preprocess has to be true because it contains embedded ITEs
d_out->lemma(node, LemmaProperty::PREPROCESS);
- // Ignore the LemmaStatus structure for now...
-
- return;
}
bool TheoryFp::propagateLit(TNode node)
diff --git a/src/theory/output_channel.cpp b/src/theory/output_channel.cpp
index 91f30514c..e63b78486 100644
--- a/src/theory/output_channel.cpp
+++ b/src/theory/output_channel.cpp
@@ -84,19 +84,7 @@ std::ostream& operator<<(std::ostream& out, LemmaProperty p)
return out;
}
-LemmaStatus::LemmaStatus(TNode rewrittenLemma, unsigned level)
- : d_rewrittenLemma(rewrittenLemma), d_level(level)
-{
-}
-
-TNode LemmaStatus::getRewrittenLemma() const { return d_rewrittenLemma; }
-
-unsigned LemmaStatus::getLevel() const { return d_level; }
-
-LemmaStatus OutputChannel::split(TNode n)
-{
- return splitLemma(n.orNode(n.notNode()));
-}
+void OutputChannel::split(TNode n) { splitLemma(n.orNode(n.notNode())); }
void OutputChannel::trustedConflict(TrustNode pconf)
{
@@ -104,7 +92,7 @@ void OutputChannel::trustedConflict(TrustNode pconf)
<< std::endl;
}
-LemmaStatus OutputChannel::trustedLemma(TrustNode lem, LemmaProperty p)
+void OutputChannel::trustedLemma(TrustNode lem, LemmaProperty p)
{
Unreachable() << "OutputChannel::trustedLemma: no implementation"
<< std::endl;
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index 197e42a99..c3d4b6a42 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -73,29 +73,6 @@ std::ostream& operator<<(std::ostream& out, LemmaProperty p);
class Theory;
/**
- * A LemmaStatus, returned from OutputChannel::lemma(), provides information
- * about the lemma added. In particular, it contains the T-rewritten lemma
- * for inspection and the user-level at which the lemma will reside.
- */
-class LemmaStatus {
- public:
- LemmaStatus(TNode rewrittenLemma, unsigned level);
-
- /** Get the T-rewritten form of the lemma. */
- TNode getRewrittenLemma() const;
- /**
- * Get the user-level at which the lemma resides. After this user level
- * is popped, the lemma is un-asserted from the SAT layer. This level
- * will be 0 if the lemma didn't reach the SAT layer at all.
- */
- unsigned getLevel() const;
-
- private:
- Node d_rewrittenLemma;
- unsigned d_level;
-}; /* class LemmaStatus */
-
-/**
* Generic "theory output channel" interface.
*
* All methods can throw unrecoverable CVC4::Exception's unless otherwise
@@ -150,10 +127,8 @@ class OutputChannel {
*
* @param n - a theory lemma valid at decision level 0
* @param p The properties of the lemma
- * @return the "status" of the lemma, including user level at which
- * the lemma resides; the lemma will be removed when this user level pops
*/
- virtual LemmaStatus lemma(TNode n, LemmaProperty p = LemmaProperty::NONE) = 0;
+ virtual void lemma(TNode n, LemmaProperty p = LemmaProperty::NONE) = 0;
/**
* Request a split on a new theory atom. This is equivalent to
@@ -161,9 +136,9 @@ class OutputChannel {
*
* @param n - a theory atom; must be of Boolean type
*/
- LemmaStatus split(TNode n);
+ void split(TNode n);
- virtual LemmaStatus splitLemma(TNode n, bool removable = false) = 0;
+ virtual void splitLemma(TNode n, bool removable = false) = 0;
/**
* If a decision is made on n, it must be in the phase specified.
@@ -227,8 +202,8 @@ class OutputChannel {
* by the generator pfg. Apart from pfg, the interface for this method is
* the same as OutputChannel.
*/
- virtual LemmaStatus trustedLemma(TrustNode lem,
- LemmaProperty p = LemmaProperty::NONE);
+ virtual void trustedLemma(TrustNode lem,
+ LemmaProperty p = LemmaProperty::NONE);
//---------------------------- end new proof
}; /* class OutputChannel */
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 118e7023c..8a8678749 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -373,13 +373,20 @@ void InstStrategyCegqi::registerCounterexampleLemma(Node q, Node lem)
{
ce_vars.push_back(tutil->getInstantiationConstant(q, i));
}
- CegInstantiator* cinst = getInstantiator(q);
- LemmaStatus status =
- d_quantEngine->getOutputChannel().lemma(lem, LemmaProperty::PREPROCESS);
- Node ppLem = status.getRewrittenLemma();
+ // send the lemma
+ d_quantEngine->getOutputChannel().lemma(lem, LemmaProperty::PREPROCESS);
+ // get the preprocessed form of the lemma we just sent
+ std::vector<Node> skolems;
+ std::vector<Node> skAsserts;
+ Node ppLem = d_quantEngine->getValuation().getPreprocessedTerm(
+ lem, skAsserts, skolems);
+ std::vector<Node> lemp{ppLem};
+ lemp.insert(lemp.end(), skAsserts.begin(), skAsserts.end());
+ ppLem = NodeManager::currentNM()->mkAnd(lemp);
Trace("cegqi-debug") << "Counterexample lemma (post-preprocess): " << ppLem
<< std::endl;
std::vector<Node> auxLems;
+ CegInstantiator* cinst = getInstantiator(q);
cinst->registerCounterexampleLemma(ppLem, ce_vars, auxLems);
for (unsigned i = 0, size = auxLems.size(); i < size; i++)
{
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 18d9bb572..3492f97a9 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1161,19 +1161,6 @@ Node TheoryEngine::getModelValue(TNode var) {
return theoryOf(Theory::theoryOf(var.getType()))->getModelValue(var);
}
-
-Node TheoryEngine::ensureLiteral(TNode n) {
- Trace("ensureLiteral") << "ensureLiteral rewriting: " << n << std::endl;
- Node rewritten = Rewriter::rewrite(n);
- return d_propEngine->ensureLiteral(rewritten);
-}
-
-Node TheoryEngine::getPreprocessedTerm(TNode n)
-{
- Node rewritten = Rewriter::rewrite(n);
- return d_propEngine->getPreprocessedTerm(rewritten);
-}
-
void TheoryEngine::printSynthSolution( std::ostream& out ) {
if( d_quantEngine ){
d_quantEngine->printSynthSolution( out );
@@ -1340,10 +1327,10 @@ void TheoryEngine::ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::The
}
}
-theory::LemmaStatus TheoryEngine::lemma(theory::TrustNode tlemma,
- theory::LemmaProperty p,
- theory::TheoryId atomsTo,
- theory::TheoryId from)
+void TheoryEngine::lemma(theory::TrustNode tlemma,
+ theory::LemmaProperty p,
+ theory::TheoryId atomsTo,
+ theory::TheoryId from)
{
// For resource-limiting (also does a time check).
// spendResource();
@@ -1393,20 +1380,24 @@ theory::LemmaStatus TheoryEngine::lemma(theory::TrustNode tlemma,
printer.toStreamCmdCheckSat(out, n);
}
- Node retLemma = d_propEngine->assertLemma(tlemma, p);
+ // assert the lemma
+ d_propEngine->assertLemma(tlemma, p);
// If specified, we must add this lemma to the set of those that need to be
- // justified, where note we pass all auxiliary lemmas in lemmas, since these
- // by extension must be justified as well.
+ // justified, where note we pass all auxiliary lemmas in skAsserts as well,
+ // since these by extension must be justified as well.
if (d_relManager != nullptr && isLemmaPropertyNeedsJustify(p))
{
+ std::vector<Node> skAsserts;
+ std::vector<Node> sks;
+ Node retLemma =
+ d_propEngine->getPreprocessedTerm(tlemma.getProven(), skAsserts, sks);
d_relManager->notifyPreprocessedAssertion(retLemma);
+ d_relManager->notifyPreprocessedAssertions(skAsserts);
}
// Mark that we added some lemmas
d_lemmasAdded = true;
-
- return theory::LemmaStatus(retLemma, d_userContext->getLevel());
}
void TheoryEngine::conflict(theory::TrustNode tconflict, TheoryId theoryId)
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 747c1ccc9..46498e71a 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -274,13 +274,11 @@ class TheoryEngine {
* @param p the properties of the lemma.
* @param atomsTo the theory that atoms of the lemma should be sent to
* @param from the theory that sent the lemma
- * @return a lemma status, containing the lemma and context information
- * about when it was sent.
*/
- theory::LemmaStatus lemma(theory::TrustNode node,
- theory::LemmaProperty p,
- theory::TheoryId atomsTo = theory::THEORY_LAST,
- theory::TheoryId from = theory::THEORY_LAST);
+ void lemma(theory::TrustNode node,
+ theory::LemmaProperty p,
+ theory::TheoryId atomsTo = theory::THEORY_LAST,
+ theory::TheoryId from = theory::THEORY_LAST);
/** Enusre that the given atoms are send to the given theory */
void ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::TheoryId theory);
@@ -648,20 +646,6 @@ class TheoryEngine {
* has (or null if none);
*/
Node getModelValue(TNode var);
-
- /**
- * 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
- * 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 solution for synthesis conjectures found by ce_guided_instantiation module
*/
diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h
index 003e439ae..f37e4c942 100644
--- a/src/theory/theory_test_utils.h
+++ b/src/theory/theory_test_utils.h
@@ -77,26 +77,18 @@ public:
return true;
}
- LemmaStatus lemma(TNode n, LemmaProperty p) override
- {
- push(LEMMA, n);
- return LemmaStatus(Node::null(), 0);
- }
+ void lemma(TNode n, LemmaProperty p) override { push(LEMMA, n); }
- LemmaStatus trustedLemma(TrustNode n, LemmaProperty p) override
+ void trustedLemma(TrustNode n, LemmaProperty p) override
{
push(LEMMA, n.getNode());
- return LemmaStatus(Node::null(), 0);
}
void requirePhase(TNode, bool) override {}
void setIncomplete() override {}
void handleUserAttribute(const char* attr, theory::Theory* t) override {}
- LemmaStatus splitLemma(TNode n, bool removable = false) override {
- push(LEMMA, n);
- return LemmaStatus(Node::null(), 0);
- }
+ void splitLemma(TNode n, bool removable = false) override { push(LEMMA, n); }
void clear() { d_callHistory.clear(); }
diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp
index b8ee5d41c..6fae8421d 100644
--- a/src/theory/valuation.cpp
+++ b/src/theory/valuation.cpp
@@ -156,13 +156,21 @@ void Valuation::setIrrelevantKind(Kind k)
Node Valuation::ensureLiteral(TNode n) {
Assert(d_engine != nullptr);
- return d_engine->ensureLiteral(n);
+ return d_engine->getPropEngine()->ensureLiteral(n);
}
Node Valuation::getPreprocessedTerm(TNode n)
{
Assert(d_engine != nullptr);
- return d_engine->getPreprocessedTerm(n);
+ return d_engine->getPropEngine()->getPreprocessedTerm(n);
+}
+
+Node Valuation::getPreprocessedTerm(TNode n,
+ std::vector<Node>& skAsserts,
+ std::vector<Node>& sks)
+{
+ Assert(d_engine != nullptr);
+ return d_engine->getPropEngine()->getPreprocessedTerm(n, skAsserts, sks);
}
bool Valuation::isDecision(Node lit) const {
diff --git a/src/theory/valuation.h b/src/theory/valuation.h
index 065556872..9759309fa 100644
--- a/src/theory/valuation.h
+++ b/src/theory/valuation.h
@@ -159,6 +159,13 @@ public:
* @return The preprocessed form of n
*/
Node getPreprocessedTerm(TNode n);
+ /**
+ * Same as above, but also tracks the skolems and their corresponding
+ * definitions in sks and skAsserts respectively.
+ */
+ Node getPreprocessedTerm(TNode n,
+ std::vector<Node>& skAsserts,
+ std::vector<Node>& sks);
/**
* Returns whether the given lit (which must be a SAT literal) is a decision
diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index 97da7eb8b..04bc79b3a 100644
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -56,8 +56,7 @@ using namespace std;
class FakeOutputChannel : public OutputChannel {
void conflict(TNode n) override { Unimplemented(); }
bool propagate(TNode n) override { Unimplemented(); }
- LemmaStatus lemma(TNode n,
- LemmaProperty p = LemmaProperty::NONE) override
+ void lemma(TNode n, LemmaProperty p = LemmaProperty::NONE) override
{
Unimplemented();
}
@@ -66,7 +65,7 @@ class FakeOutputChannel : public OutputChannel {
void handleUserAttribute(const char* attr, Theory* t) override {
Unimplemented();
}
- LemmaStatus splitLemma(TNode n, bool removable) override { Unimplemented(); }
+ void splitLemma(TNode n, bool removable) override { Unimplemented(); }
}; /* class FakeOutputChannel */
template<TheoryId theory>
diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h
index 9f23dbad6..4b6c1a064 100644
--- a/test/unit/theory/theory_white.h
+++ b/test/unit/theory/theory_white.h
@@ -54,17 +54,12 @@ class TestOutputChannel : public OutputChannel {
return true;
}
- LemmaStatus lemma(TNode n,
- LemmaProperty p = LemmaProperty::NONE) override
+ void lemma(TNode n, LemmaProperty p = LemmaProperty::NONE) override
{
push(LEMMA, n);
- return LemmaStatus(Node::null(), 0);
}
- LemmaStatus splitLemma(TNode n, bool removable) override {
- push(LEMMA, n);
- return LemmaStatus(Node::null(), 0);
- }
+ void splitLemma(TNode n, bool removable) override { push(LEMMA, n); }
void requirePhase(TNode, bool) override { Unreachable(); }
void setIncomplete() override { Unreachable(); }
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback