summaryrefslogtreecommitdiff
path: root/src/prop
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop')
-rw-r--r--src/prop/prop_engine.cpp22
-rw-r--r--src/prop/prop_engine.h4
-rw-r--r--src/prop/skolem_def_manager.cpp173
-rw-r--r--src/prop/skolem_def_manager.h91
-rw-r--r--src/prop/theory_proxy.cpp33
-rw-r--r--src/prop/theory_proxy.h12
6 files changed, 317 insertions, 18 deletions
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 71b27d8ec..3f53433ae 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -174,17 +174,15 @@ theory::TrustNode PropEngine::removeItes(
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);
}
@@ -192,7 +190,7 @@ void PropEngine::assertSkolemDefinition(TNode node, TNode skolem)
{
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);
}
@@ -284,13 +282,13 @@ void PropEngine::assertLemmasInternal(
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]);
}
}
}
@@ -465,14 +463,14 @@ Node PropEngine::getPreprocessedTerm(TNode n,
// 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())
@@ -481,7 +479,7 @@ Node PropEngine::getPreprocessedTerm(TNode n,
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
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index d0810324a..fe5d94122 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -220,6 +220,10 @@ class PropEngine
* 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,
diff --git a/src/prop/skolem_def_manager.cpp b/src/prop/skolem_def_manager.cpp
new file mode 100644
index 000000000..c2a6a8462
--- /dev/null
+++ b/src/prop/skolem_def_manager.cpp
@@ -0,0 +1,173 @@
+/********************* */
+/*! \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
diff --git a/src/prop/skolem_def_manager.h b/src/prop/skolem_def_manager.h
new file mode 100644
index 000000000..9bb118356
--- /dev/null
+++ b/src/prop/skolem_def_manager.h
@@ -0,0 +1,91 @@
+/********************* */
+/*! \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 */
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 5ee472b93..66023cd88 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -42,7 +42,8 @@ TheoryProxy::TheoryProxy(PropEngine* propEngine,
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))
{
}
@@ -52,6 +53,29 @@ TheoryProxy::~TheoryProxy() {
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)));
}
@@ -194,16 +218,15 @@ theory::TrustNode TheoryProxy::removeItes(
}
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));
}
}
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index 83c64d726..01d98f1b9 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -29,6 +29,7 @@
#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"
@@ -62,6 +63,12 @@ class TheoryProxy : public Registrar
/** 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);
@@ -124,7 +131,7 @@ class TheoryProxy : public Registrar
* 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;
@@ -153,6 +160,9 @@ class TheoryProxy : public Registrar
/** The theory preprocessor */
theory::TheoryPreprocessor d_tpp;
+
+ /** The skolem definition manager */
+ std::unique_ptr<SkolemDefManager> d_skdm;
}; /* class TheoryProxy */
}/* CVC4::prop namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback