This makes it so that TheoryEngine::lemma returns void not LemmaStatus.
Currently, there was only one use of LemmaStatus by theory solvers, which was CEGQI using it as a way of getting the preprocessed form of a lemma. This makes it so that there is an explicit method in Valuation for getting the preprocessed form of a term + its skolems and their definition assertions.
It also simplifies a few things, e.g. Valuation calls are forwarded to PropEngine instead of going through TheoryEngine. It fixes a few issues in TermFormulaRemoval related to getSkolems.
#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"
}
}
-Node PropEngine::assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p)
+void PropEngine::assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p)
{
bool removable = isLemmaPropertyRemovable(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)
Node PropEngine::getPreprocessedTerm(TNode n)
{
+ Node rewritten = theory::Rewriter::rewrite(n);
// must preprocess
std::vector<theory::TrustNode> newLemmas;
std::vector<Node> newSkolems;
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()!";
*
* @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
* 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.
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 */
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;
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;
{
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)
* 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;
/**
// 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);
}
}
const std::vector<Theory*>& paraTheories,
ProofNodeManager* pnm)
: d_te(te),
+ d_valuation(&te),
d_pnm(pnm),
d_logicInfo(te.getLogicInfo()),
d_paraTheories(paraTheories),
#include "theory/ee_manager.h"
#include "theory/model_manager.h"
#include "theory/shared_solver.h"
+#include "theory/valuation.h"
namespace CVC4 {
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) */
}
}
-theory::LemmaStatus EngineOutputChannel::lemma(TNode lemma, LemmaProperty p)
+void EngineOutputChannel::lemma(TNode lemma, LemmaProperty p)
{
Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma("
<< lemma << ")"
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;
<< 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)
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;
++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
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;
* 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:
/**
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)
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)
{
<< std::endl;
}
-LemmaStatus OutputChannel::trustedLemma(TrustNode lem, LemmaProperty p)
+void OutputChannel::trustedLemma(TrustNode lem, LemmaProperty p)
{
Unreachable() << "OutputChannel::trustedLemma: no implementation"
<< std::endl;
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.
*
*
* @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
*
* @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.
* 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 */
{
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++)
{
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 );
}
}
-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();
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)
* @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);
* 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
*/
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(); }
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 {
* @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
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();
}
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>
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(); }
projects / cvc5.git / commitdiff