This creates a central utility for managing "skolem definitions", e.g. mapping between skolems and the lemmas that define their behavior.
This utility is taken from the satRlv branch. It will also be used for the new implementation of the justification decision heuristic.
Note that this PR takes some helper functions out of term formula removal (e.g. hasSkolems) Prior to this PR, these helper functions were incorrect since term formula removal does not account for all introduced skolems. For instance, Theory::ppRewrite may introduce skolems directly. This PR consolidates these cases into the new class, which is called from PropEngine when lemmas and assertions are added. At the moment, the only use of this method is for CEGQI, which needs to do its own tracking of skolems in certain literals.
It also makes some minor reorganization to prop engine.
prop/sat_solver_factory.h
prop/sat_solver_types.cpp
prop/sat_solver_types.h
+ prop/skolem_def_manager.cpp
+ prop/skolem_def_manager.h
prop/theory_proxy.cpp
prop/theory_proxy.h
smt/abduction_solver.cpp
void PropEngine::notifyPreprocessedAssertions(
const std::vector<Node>& assertions)
{
- // notify the theory engine of preprocessed assertions
- d_theoryEngine->notifyPreprocessedAssertions(assertions);
- for (const Node& assertion : assertions)
- {
- d_decisionEngine->addAssertion(assertion);
- }
+ // notify the theory proxy of preprocessed assertions
+ d_theoryProxy->notifyPreprocessedAssertions(assertions);
}
void PropEngine::assertFormula(TNode node) {
Assert(!d_inCheckSat) << "Sat solver in solve()!";
Debug("prop") << "assertFormula(" << node << ")" << std::endl;
+ // NOTE: we do not notify the theory proxy here, since we've already
+ // notified the theory proxy during notifyPreprocessedAssertions
assertInternal(node, false, false, true);
}
{
Assert(!d_inCheckSat) << "Sat solver in solve()!";
Debug("prop") << "assertFormula(" << node << ")" << std::endl;
- d_decisionEngine->addSkolemDefinition(node, skolem);
+ d_theoryProxy->notifyAssertion(node, skolem);
assertInternal(node, false, false, true);
}
if (!trn.isNull())
{
// notify the theory proxy of the lemma
- d_decisionEngine->addAssertion(trn.getProven());
+ d_theoryProxy->notifyAssertion(trn.getProven());
}
Assert(ppSkolems.size() == ppLemmas.size());
for (size_t i = 0, lsize = ppLemmas.size(); i < lsize; ++i)
{
Node lem = ppLemmas[i].getProven();
- d_decisionEngine->addSkolemDefinition(lem, ppSkolems[i]);
+ d_theoryProxy->notifyAssertion(ppLemmas[i].getProven(), ppSkolems[i]);
}
}
}
// 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> 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 ka = toProcessAsserts[index];
Node k = toProcess[index];
index++;
if (std::find(sks.begin(), sks.end(), k) != sks.end())
continue;
}
// must preprocess lemmas as well
- Node kap = getPreprocessedTerm(ka.getProven());
+ Node kap = getPreprocessedTerm(ka);
skAsserts.push_back(kap);
sks.push_back(k);
// get the skolems in the preprocessed form of the lemma ka
* 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.
+ *
+ * Notice that this method is not frequently used. It is used for algorithms
+ * that explicitly care about knowing which skolems occur in the preprocessed
+ * form of a term, recursively.
*/
Node getPreprocessedTerm(TNode n,
std::vector<Node>& skAsserts,
--- /dev/null
+/********************* */
+/*! \file skolem_def_manager.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Skolem definition manager
+ **/
+
+#include "prop/skolem_def_manager.h"
+
+#include "expr/attribute.h"
+
+namespace CVC4 {
+namespace prop {
+
+SkolemDefManager::SkolemDefManager(context::Context* context,
+ context::UserContext* userContext)
+ : d_skDefs(userContext), d_skActive(context)
+{
+}
+
+SkolemDefManager::~SkolemDefManager() {}
+
+void SkolemDefManager::notifySkolemDefinition(TNode skolem, Node def)
+{
+ // Notice that skolem may have kind SKOLEM or BOOLEAN_TERM_VARIABLE
+ Trace("sk-defs") << "notifySkolemDefinition: " << def << " for " << skolem
+ << std::endl;
+ // in very rare cases, a skolem may be generated twice for terms that are
+ // equivalent up to purification
+ if (d_skDefs.find(skolem) == d_skDefs.end())
+ {
+ d_skDefs.insert(skolem, def);
+ }
+}
+
+TNode SkolemDefManager::getDefinitionForSkolem(TNode skolem) const
+{
+ NodeNodeMap::const_iterator it = d_skDefs.find(skolem);
+ AlwaysAssert(it != d_skDefs.end()) << "No skolem def for " << skolem;
+ return it->second;
+}
+
+void SkolemDefManager::notifyAsserted(TNode literal,
+ std::vector<TNode>& activatedSkolems)
+{
+ std::unordered_set<Node, NodeHashFunction> skolems;
+ getSkolems(literal, skolems);
+ for (const Node& k : skolems)
+ {
+ if (d_skActive.find(k) != d_skActive.end())
+ {
+ // already active
+ continue;
+ }
+ d_skActive.insert(k);
+ // add to the activated list
+ activatedSkolems.push_back(k);
+ }
+}
+
+struct HasSkolemTag
+{
+};
+struct HasSkolemComputedTag
+{
+};
+/** Attribute true for nodes with skolems in them */
+typedef expr::Attribute<HasSkolemTag, bool> HasSkolemAttr;
+/** Attribute true for nodes where we have computed the above attribute */
+typedef expr::Attribute<HasSkolemComputedTag, bool> HasSkolemComputedAttr;
+
+bool SkolemDefManager::hasSkolems(TNode n) const
+{
+ std::unordered_set<TNode, TNodeHashFunction> visited;
+ std::unordered_set<TNode, TNodeHashFunction>::iterator it;
+ std::vector<TNode> visit;
+ TNode cur;
+ visit.push_back(n);
+ do
+ {
+ cur = visit.back();
+ if (cur.getAttribute(HasSkolemComputedAttr()))
+ {
+ visit.pop_back();
+ // already computed
+ continue;
+ }
+ it = visited.find(cur);
+ if (it == visited.end())
+ {
+ visited.insert(cur);
+ if (cur.getNumChildren() == 0)
+ {
+ visit.pop_back();
+ bool hasSkolem = false;
+ if (cur.isVar())
+ {
+ hasSkolem = (d_skDefs.find(cur) != d_skDefs.end());
+ }
+ cur.setAttribute(HasSkolemAttr(), hasSkolem);
+ cur.setAttribute(HasSkolemComputedAttr(), true);
+ }
+ else
+ {
+ visit.insert(visit.end(), cur.begin(), cur.end());
+ }
+ }
+ else
+ {
+ visit.pop_back();
+ bool hasSkolem = false;
+ for (TNode i : cur)
+ {
+ Assert(i.getAttribute(HasSkolemComputedAttr()));
+ if (i.getAttribute(HasSkolemAttr()))
+ {
+ hasSkolem = true;
+ break;
+ }
+ }
+ cur.setAttribute(HasSkolemAttr(), hasSkolem);
+ cur.setAttribute(HasSkolemComputedAttr(), true);
+ }
+ } while (!visit.empty());
+ Assert(n.getAttribute(HasSkolemComputedAttr()));
+ return n.getAttribute(HasSkolemAttr());
+}
+
+void SkolemDefManager::getSkolems(
+ TNode n, std::unordered_set<Node, NodeHashFunction>& skolems) const
+{
+ std::unordered_set<TNode, TNodeHashFunction> visited;
+ std::unordered_set<TNode, TNodeHashFunction>::iterator it;
+ std::vector<TNode> visit;
+ TNode cur;
+ visit.push_back(n);
+ do
+ {
+ cur = visit.back();
+ visit.pop_back();
+ if (!hasSkolems(cur))
+ {
+ // does not have skolems, continue
+ continue;
+ }
+ it = visited.find(cur);
+ if (it == visited.end())
+ {
+ visited.insert(cur);
+ if (cur.isVar())
+ {
+ if (d_skDefs.find(cur) != d_skDefs.end())
+ {
+ skolems.insert(cur);
+ }
+ }
+ else
+ {
+ visit.insert(visit.end(), cur.begin(), cur.end());
+ }
+ }
+ } while (!visit.empty());
+}
+
+} // namespace prop
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file skolem_def_manager.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Skolem definition manager
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__PROP__SKOLEM_DEF_MANAGER_H
+#define CVC4__PROP__SKOLEM_DEF_MANAGER_H
+
+#include <iosfwd>
+#include <unordered_set>
+#include <vector>
+
+#include "context/cdhashset.h"
+#include "context/cdinsert_hashmap.h"
+#include "context/context.h"
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace prop {
+
+/**
+ * This class manages the mapping between introduced skolems and the lemmas
+ * that define their behavior. It can be used to manage which lemmas are
+ * relevant in the current context, e.g. a lemma corresponding to a skolem
+ * definition for k is relevant when k appears in an asserted literal.
+ *
+ * It also has utilities for tracking (in a SAT-context-dependent manner) which
+ * skolems are "active", e.g. appear in any asserted literal.
+ */
+class SkolemDefManager
+{
+ using NodeNodeMap = context::CDInsertHashMap<Node, Node, NodeHashFunction>;
+ using NodeSet = context::CDHashSet<Node, NodeHashFunction>;
+
+ public:
+ SkolemDefManager(context::Context* context,
+ context::UserContext* userContext);
+
+ ~SkolemDefManager();
+
+ /**
+ * Notify skolem definition. This is called when a lemma def is added to the
+ * SAT solver that corresponds to the skolem definition for skolem k.
+ */
+ void notifySkolemDefinition(TNode k, Node def);
+ /**
+ * Get skolem definition for k, where k must be a skolem having a definition
+ * managed by this class.
+ */
+ TNode getDefinitionForSkolem(TNode k) const;
+ /**
+ * Notify that the given literal has been asserted. This method adds skolems
+ * that become "active" as a result of asserting this literal. A skolem
+ * is active in the SAT context if it appears in an asserted literal.
+ */
+ void notifyAsserted(TNode literal, std::vector<TNode>& activatedSkolems);
+
+ /**
+ * Get the set of skolems maintained by this class that occur in node n,
+ * add them to skolems.
+ *
+ * @param n The node to traverse
+ * @param skolems The set where the skolems are added
+ */
+ void getSkolems(TNode n,
+ std::unordered_set<Node, NodeHashFunction>& skolems) const;
+ /** Does n have skolems having definitions managed by this class? */
+ bool hasSkolems(TNode n) const;
+
+ private:
+ /** skolems to definitions (user-context dependent) */
+ NodeNodeMap d_skDefs;
+ /** set of active skolems (SAT-context dependent) */
+ NodeSet d_skActive;
+};
+
+} // namespace prop
+} // namespace CVC4
+
+#endif /* CVC4__PROP__SKOLEM_DEF_MANAGER_H */
d_decisionEngine(decisionEngine),
d_theoryEngine(theoryEngine),
d_queue(context),
- d_tpp(*theoryEngine, userContext, pnm)
+ d_tpp(*theoryEngine, userContext, pnm),
+ d_skdm(new SkolemDefManager(context, userContext))
{
}
void TheoryProxy::finishInit(CnfStream* cnfStream) { d_cnfStream = cnfStream; }
+void TheoryProxy::notifyPreprocessedAssertions(
+ const std::vector<Node>& assertions)
+{
+ d_theoryEngine->notifyPreprocessedAssertions(assertions);
+ for (const Node& assertion : assertions)
+ {
+ d_decisionEngine->addAssertion(assertion);
+ }
+}
+
+void TheoryProxy::notifyAssertion(Node lem, TNode skolem)
+{
+ if (skolem.isNull())
+ {
+ d_decisionEngine->addAssertion(lem);
+ }
+ else
+ {
+ d_skdm->notifySkolemDefinition(skolem, lem);
+ d_decisionEngine->addSkolemDefinition(lem, skolem);
+ }
+}
+
void TheoryProxy::variableNotify(SatVariable var) {
d_theoryEngine->preRegister(getNode(SatLiteral(var)));
}
}
void TheoryProxy::getSkolems(TNode node,
- std::vector<theory::TrustNode>& skAsserts,
+ std::vector<Node>& skAsserts,
std::vector<Node>& sks)
{
- RemoveTermFormulas& rtf = d_tpp.getRemoveTermFormulas();
std::unordered_set<Node, NodeHashFunction> skolems;
- rtf.getSkolems(node, skolems);
+ d_skdm->getSkolems(node, skolems);
for (const Node& k : skolems)
{
sks.push_back(k);
- skAsserts.push_back(rtf.getLemmaForSkolem(k));
+ skAsserts.push_back(d_skdm->getDefinitionForSkolem(k));
}
}
#include "expr/node.h"
#include "prop/registrar.h"
#include "prop/sat_solver_types.h"
+#include "prop/skolem_def_manager.h"
#include "theory/theory.h"
#include "theory/theory_preprocessor.h"
#include "theory/trust_node.h"
/** Finish initialize */
void finishInit(CnfStream* cnfStream);
+ /** Notify (preprocessed) assertions. */
+ void notifyPreprocessedAssertions(const std::vector<Node>& assertions);
+
+ /** Notify a lemma, possibly corresponding to a skolem definition */
+ void notifyAssertion(Node lem, TNode skolem = TNode::null());
+
void theoryCheck(theory::Theory::Effort effort);
void explainPropagation(SatLiteral l, SatClause& explanation);
* fixed point is reached.
*/
void getSkolems(TNode node,
- std::vector<theory::TrustNode>& skAsserts,
+ std::vector<Node>& skAsserts,
std::vector<Node>& sks);
/** Preregister term */
void preRegister(Node n) override;
/** The theory preprocessor */
theory::TheoryPreprocessor d_tpp;
+
+ /** The skolem definition manager */
+ std::unique_ptr<SkolemDefManager> d_skdm;
}; /* class TheoryProxy */
}/* CVC4::prop namespace */
ProofNodeManager* pnm)
: d_tfCache(u),
d_skolem_cache(u),
- d_lemmaCache(u),
d_pnm(pnm),
d_tpg(nullptr),
d_lp(nullptr)
newLem = theory::TrustNode::mkTrustLemma(newAssertion, d_lp.get());
- // store in the lemma cache, if it is not already there.
- if (d_lemmaCache.find(skolem) == d_lemmaCache.end())
- {
- d_lemmaCache.insert(skolem, newLem);
- }
-
Trace("rtf-proof-debug") << "Checking closed..." << std::endl;
newLem.debugCheckClosed("rtf-proof-debug",
"RemoveTermFormulas::run:new_assert");
return Node::null();
}
-struct HasSkolemTag
-{
-};
-struct HasSkolemComputedTag
-{
-};
-/** Attribute true for nodes with skolems in them */
-typedef expr::Attribute<HasSkolemTag, bool> HasSkolemAttr;
-/** Attribute true for nodes where we have computed the above attribute */
-typedef expr::Attribute<HasSkolemComputedTag, bool> HasSkolemComputedAttr;
-
-bool RemoveTermFormulas::hasSkolems(TNode n) const
-{
- std::unordered_set<TNode, TNodeHashFunction> visited;
- std::unordered_set<TNode, TNodeHashFunction>::iterator it;
- std::vector<TNode> visit;
- TNode cur;
- visit.push_back(n);
- do
- {
- cur = visit.back();
- if (cur.getAttribute(HasSkolemComputedAttr()))
- {
- visit.pop_back();
- // already computed
- continue;
- }
- it = visited.find(cur);
- if (it == visited.end())
- {
- visited.insert(cur);
- if (cur.getNumChildren() == 0)
- {
- visit.pop_back();
- bool hasSkolem = false;
- if (cur.isVar())
- {
- hasSkolem = (d_lemmaCache.find(cur) != d_lemmaCache.end());
- }
- cur.setAttribute(HasSkolemAttr(), hasSkolem);
- cur.setAttribute(HasSkolemComputedAttr(), true);
- }
- else
- {
- visit.insert(visit.end(), cur.begin(), cur.end());
- }
- }
- else
- {
- visit.pop_back();
- bool hasSkolem = false;
- for (TNode i : cur)
- {
- Assert(i.getAttribute(HasSkolemComputedAttr()));
- if (i.getAttribute(HasSkolemAttr()))
- {
- hasSkolem = true;
- break;
- }
- }
- cur.setAttribute(HasSkolemAttr(), hasSkolem);
- cur.setAttribute(HasSkolemComputedAttr(), true);
- }
- } while (!visit.empty());
- Assert(n.getAttribute(HasSkolemComputedAttr()));
- return n.getAttribute(HasSkolemAttr());
-}
-
-void RemoveTermFormulas::getSkolems(
- TNode n, std::unordered_set<Node, NodeHashFunction>& skolems) const
-{
- std::unordered_set<TNode, TNodeHashFunction> visited;
- std::unordered_set<TNode, TNodeHashFunction>::iterator it;
- std::vector<TNode> visit;
- TNode cur;
- visit.push_back(n);
- do
- {
- cur = visit.back();
- visit.pop_back();
- if (!hasSkolems(cur))
- {
- // does not have skolems, continue
- continue;
- }
- it = visited.find(cur);
- if (it == visited.end())
- {
- visited.insert(cur);
- if (cur.isVar())
- {
- if (d_lemmaCache.find(cur) != d_lemmaCache.end())
- {
- skolems.insert(cur);
- }
- }
- else
- {
- visit.insert(visit.end(), cur.begin(), cur.end());
- }
- }
- } while (!visit.empty());
-}
-
Node RemoveTermFormulas::getAxiomFor(Node n)
{
NodeManager* nm = NodeManager::currentNM();
return Node::null();
}
-theory::TrustNode RemoveTermFormulas::getLemmaForSkolem(TNode n) const
-{
- context::CDInsertHashMap<Node, theory::TrustNode, NodeHashFunction>::
- const_iterator it = d_lemmaCache.find(n);
- if (it == d_lemmaCache.end())
- {
- return theory::TrustNode::null();
- }
- return (*it).second;
-}
-
ProofGenerator* RemoveTermFormulas::getTConvProofGenerator()
{
return d_tpg.get();
*/
static Node getAxiomFor(Node n);
- /**
- * Get the set of skolems introduced by this class that occur in node n,
- * add them to skolems.
- *
- * @param n The node to traverse
- * @param skolems The set where the skolems are added
- */
- void getSkolems(TNode n,
- std::unordered_set<Node, NodeHashFunction>& skolems) const;
- /**
- * Does n have skolems introduced by this class?
- */
- bool hasSkolems(TNode n) const;
-
- /**
- * Get the lemma for the skolem, or the null node if k is not a skolem this
- * class introduced.
- */
- theory::TrustNode getLemmaForSkolem(TNode k) const;
-
private:
typedef context::CDInsertHashMap<
std::pair<Node, uint32_t>,
* d_tfCache[<ite( G, a, b ),0>] = d_tfCache[<ite( G, a, b ),1>] = k.
*/
context::CDInsertHashMap<Node, Node, NodeHashFunction> d_skolem_cache;
- /**
- * Mapping from skolems to their corresponding lemma.
- */
- context::CDInsertHashMap<Node, theory::TrustNode, NodeHashFunction>
- d_lemmaCache;
/** gets the skolem for node
*
projects / cvc5.git / commitdiff