summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/decision/decision_engine.cpp2
-rw-r--r--src/decision/decision_engine.h2
-rw-r--r--src/decision/decision_strategy.h4
-rw-r--r--src/decision/justification_heuristic.cpp2
-rw-r--r--src/decision/justification_heuristic.h2
-rw-r--r--src/prop/prop_engine.cpp2
-rw-r--r--src/prop/prop_engine.h11
-rw-r--r--src/prop/skolem_def_manager.cpp19
-rw-r--r--src/prop/skolem_def_manager.h9
-rw-r--r--src/prop/theory_proxy.cpp6
-rw-r--r--src/prop/theory_proxy.h11
11 files changed, 53 insertions, 17 deletions
diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index 12e148500..d55d2077f 100644
--- a/src/decision/decision_engine.cpp
+++ b/src/decision/decision_engine.cpp
@@ -24,6 +24,7 @@
using namespace std;
namespace cvc5 {
+namespace decision {
DecisionEngine::DecisionEngine(context::Context* sc,
context::UserContext* uc,
@@ -100,4 +101,5 @@ void DecisionEngine::addSkolemDefinition(TNode lem, TNode skolem)
}
}
+}
} // namespace cvc5
diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index 0a1d63d99..c10fe2bb9 100644
--- a/src/decision/decision_engine.h
+++ b/src/decision/decision_engine.h
@@ -31,6 +31,7 @@ using namespace cvc5::prop;
using namespace cvc5::decision;
namespace cvc5 {
+namespace decision {
class DecisionEngine {
@@ -159,6 +160,7 @@ class DecisionEngine {
std::unique_ptr<ITEDecisionStrategy> d_enabledITEStrategy;
};/* DecisionEngine class */
+}
} // namespace cvc5
#endif /* CVC5__DECISION__DECISION_ENGINE_H */
diff --git a/src/decision/decision_strategy.h b/src/decision/decision_strategy.h
index 9f3b4be91..0376b00cc 100644
--- a/src/decision/decision_strategy.h
+++ b/src/decision/decision_strategy.h
@@ -26,13 +26,13 @@
namespace cvc5 {
-class DecisionEngine;
-
namespace context {
class Context;
} // namespace context
namespace decision {
+
+class DecisionEngine;
class DecisionStrategy {
protected:
diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index 42e4cb7b0..ecc0ae68c 100644
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -32,7 +32,7 @@
namespace cvc5 {
namespace decision {
-JustificationHeuristic::JustificationHeuristic(cvc5::DecisionEngine* de,
+JustificationHeuristic::JustificationHeuristic(DecisionEngine* de,
context::UserContext* uc,
context::Context* c)
: ITEDecisionStrategy(de, c),
diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h
index a7c82646d..45f297bb9 100644
--- a/src/decision/justification_heuristic.h
+++ b/src/decision/justification_heuristic.h
@@ -117,7 +117,7 @@ class JustificationHeuristic : public ITEDecisionStrategy {
};
public:
- JustificationHeuristic(cvc5::DecisionEngine* de,
+ JustificationHeuristic(DecisionEngine* de,
context::UserContext* uc,
context::Context* c);
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 646da84b2..c4d929d35 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -73,6 +73,7 @@ PropEngine::PropEngine(TheoryEngine* te,
: d_inCheckSat(false),
d_theoryEngine(te),
d_context(satContext),
+ d_skdm(new SkolemDefManager(satContext, userContext)),
d_theoryProxy(nullptr),
d_satSolver(nullptr),
d_pnm(pnm),
@@ -95,6 +96,7 @@ PropEngine::PropEngine(TheoryEngine* te,
d_theoryProxy = new TheoryProxy(this,
d_theoryEngine,
d_decisionEngine.get(),
+ d_skdm.get(),
satContext,
userContext,
pnm);
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index cae02eba2..a0496a525 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -22,6 +22,7 @@
#include "context/cdlist.h"
#include "expr/node.h"
+#include "prop/skolem_def_manager.h"
#include "theory/output_channel.h"
#include "theory/trust_node.h"
#include "util/result.h"
@@ -29,11 +30,14 @@
namespace cvc5 {
class ResourceManager;
-class DecisionEngine;
class OutputManager;
class ProofNodeManager;
class TheoryEngine;
+namespace decision {
+class DecisionEngine;
+}
+
namespace prop {
class CnfStream;
@@ -331,11 +335,14 @@ class PropEngine
TheoryEngine* d_theoryEngine;
/** The decision engine we will be using */
- std::unique_ptr<DecisionEngine> d_decisionEngine;
+ std::unique_ptr<decision::DecisionEngine> d_decisionEngine;
/** The context */
context::Context* d_context;
+ /** The skolem definition manager */
+ std::unique_ptr<SkolemDefManager> d_skdm;
+
/** SAT solver's proxy back to theories; kept around for dtor cleanup */
TheoryProxy* d_theoryProxy;
diff --git a/src/prop/skolem_def_manager.cpp b/src/prop/skolem_def_manager.cpp
index 9b4011557..873a748ae 100644
--- a/src/prop/skolem_def_manager.cpp
+++ b/src/prop/skolem_def_manager.cpp
@@ -44,12 +44,13 @@ void SkolemDefManager::notifySkolemDefinition(TNode skolem, Node 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;
+ Assert(it != d_skDefs.end()) << "No skolem def for " << skolem;
return it->second;
}
void SkolemDefManager::notifyAsserted(TNode literal,
- std::vector<TNode>& activatedSkolems)
+ std::vector<TNode>& activatedSkolems,
+ bool useDefs)
{
std::unordered_set<Node, NodeHashFunction> skolems;
getSkolems(literal, skolems);
@@ -61,8 +62,18 @@ void SkolemDefManager::notifyAsserted(TNode literal,
continue;
}
d_skActive.insert(k);
- // add to the activated list
- activatedSkolems.push_back(k);
+ if (useDefs)
+ {
+ // add its definition to the activated list
+ NodeNodeMap::const_iterator it = d_skDefs.find(k);
+ Assert(it != d_skDefs.end());
+ activatedSkolems.push_back(it->second);
+ }
+ else
+ {
+ // add to the activated list
+ activatedSkolems.push_back(k);
+ }
}
}
diff --git a/src/prop/skolem_def_manager.h b/src/prop/skolem_def_manager.h
index 9ddde3fb2..475f40c85 100644
--- a/src/prop/skolem_def_manager.h
+++ b/src/prop/skolem_def_manager.h
@@ -64,8 +64,15 @@ class SkolemDefManager
* 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.
+ *
+ * @param literal The literal that became asserted
+ * @param activatedSkolems The list to add skolems to
+ * @param useDefs If this flag is true, we add the skolem definition for
+ * skolems to activatedSkolems instead of the skolem itself.
*/
- void notifyAsserted(TNode literal, std::vector<TNode>& activatedSkolems);
+ void notifyAsserted(TNode literal,
+ std::vector<TNode>& activatedSkolems,
+ bool useDefs = false);
/**
* Get the set of skolems maintained by this class that occur in node n,
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 98a76ae1a..43f91f732 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -24,6 +24,7 @@
#include "proof/cnf_proof.h"
#include "prop/cnf_stream.h"
#include "prop/prop_engine.h"
+#include "prop/skolem_def_manager.h"
#include "smt/smt_statistics_registry.h"
#include "theory/rewriter.h"
#include "theory/theory_engine.h"
@@ -34,7 +35,8 @@ namespace prop {
TheoryProxy::TheoryProxy(PropEngine* propEngine,
TheoryEngine* theoryEngine,
- DecisionEngine* decisionEngine,
+ decision::DecisionEngine* decisionEngine,
+ SkolemDefManager* skdm,
context::Context* context,
context::UserContext* userContext,
ProofNodeManager* pnm)
@@ -44,7 +46,7 @@ TheoryProxy::TheoryProxy(PropEngine* propEngine,
d_theoryEngine(theoryEngine),
d_queue(context),
d_tpp(*theoryEngine, userContext, pnm),
- d_skdm(new SkolemDefManager(context, userContext))
+ d_skdm(skdm)
{
}
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index 5ba9ea50f..bc834d205 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -28,7 +28,6 @@
#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"
@@ -36,13 +35,16 @@
namespace cvc5 {
+namespace decision {
class DecisionEngine;
+}
class TheoryEngine;
namespace prop {
class PropEngine;
class CnfStream;
+class SkolemDefManager;
/**
* The proxy class that allows the SatSolver to communicate with the theories
@@ -52,7 +54,8 @@ class TheoryProxy : public Registrar
public:
TheoryProxy(PropEngine* propEngine,
TheoryEngine* theoryEngine,
- DecisionEngine* decisionEngine,
+ decision::DecisionEngine* decisionEngine,
+ SkolemDefManager* skdm,
context::Context* context,
context::UserContext* userContext,
ProofNodeManager* pnm);
@@ -140,7 +143,7 @@ class TheoryProxy : public Registrar
CnfStream* d_cnfStream;
/** The decision engine we are using. */
- DecisionEngine* d_decisionEngine;
+ decision::DecisionEngine* d_decisionEngine;
/** The theory engine we are using. */
TheoryEngine* d_theoryEngine;
@@ -158,7 +161,7 @@ class TheoryProxy : public Registrar
theory::TheoryPreprocessor d_tpp;
/** The skolem definition manager */
- std::unique_ptr<SkolemDefManager> d_skdm;
+ SkolemDefManager* d_skdm;
}; /* class TheoryProxy */
} // namespace prop
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback