diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-10-03 17:59:33 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-10-03 17:59:33 +0000 |
commit | f0547f8a6fe9cecefde8b1d0c3dc8fcf50219c6b (patch) | |
tree | a2afaaa295c8964408dd7c53127df61527e00d90 /src/prop/prop_engine.h | |
parent | b8a010d260c90efa5433a71dd317a03f051c2592 (diff) |
adding ::getBooleanVariables to the PropEngine
you can get the Boolean variables in the TheoryEngine now by using d_propEngine->getBooleanVariables
Diffstat (limited to 'src/prop/prop_engine.h')
-rw-r--r-- | src/prop/prop_engine.h | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 2d4e08db7..f3b1ccaf3 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -157,7 +157,7 @@ public: /** * Create a PropEngine with a particular decision and theory engine. */ - PropEngine(TheoryEngine*, DecisionEngine*, context::Context*); + PropEngine(TheoryEngine*, DecisionEngine*, context::Context* satContext, context::Context* userContext); /** * Destructor. @@ -260,6 +260,11 @@ public: bool hasValue(TNode node, bool& value) const; /** + * Returns the Boolean variables known to the SAT solver. + */ + void getBooleanVariables(std::vector<TNode>& outputVariables) const; + + /** * Ensure that the given node will have a designated SAT literal * that is definitionally equal to it. The result of this function * is that the Node can be queried via getSatValue(). |