diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-15 03:24:51 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-15 03:24:51 +0000 |
commit | 43839eed3814cb4175869cd1fbbb4e9a5ece59dc (patch) | |
tree | 7e21053b228b6d4a1d8c6b9381f5e0a6c1be3b1b /src/theory/booleans | |
parent | 331c0f5861060f4b6f3f14cf17bd2a15059bb54a (diff) |
Fix for incompleteness bug with decision engine: repeated simplification
could introduce additional assertions that were not beign processed by the
decision engine. Now these assertions are merged in with pre-ITE-removal
assertions, ensuring the decision engine sees them.
Diffstat (limited to 'src/theory/booleans')
-rw-r--r-- | src/theory/booleans/circuit_propagator.h | 24 |
1 files changed, 17 insertions, 7 deletions
diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h index 60e48dba2..796bc9e21 100644 --- a/src/theory/booleans/circuit_propagator.h +++ b/src/theory/booleans/circuit_propagator.h @@ -68,6 +68,8 @@ public: private: + context::Context d_context; + /** The propagation queue */ std::vector<TNode> d_propagationQueue; @@ -234,21 +236,29 @@ public: /** * Construct a new CircuitPropagator. */ - CircuitPropagator(context::Context* context, std::vector<Node>& outLearnedLiterals, + CircuitPropagator(std::vector<Node>& outLearnedLiterals, bool enableForward = true, bool enableBackward = true) : + d_context(), d_propagationQueue(), - d_propagationQueueClearer(context, d_propagationQueue), - d_conflict(context, false), + d_propagationQueueClearer(&d_context, d_propagationQueue), + d_conflict(&d_context, false), d_learnedLiterals(outLearnedLiterals), - d_learnedLiteralClearer(context, outLearnedLiterals), + d_learnedLiteralClearer(&d_context, outLearnedLiterals), d_backEdges(), - d_backEdgesClearer(context, d_backEdges), - d_seen(context), - d_state(context), + d_backEdgesClearer(&d_context, d_backEdges), + d_seen(&d_context), + d_state(&d_context), d_forwardPropagation(enableForward), d_backwardPropagation(enableBackward) { } + // Use custom context to ensure propagator is reset after use + void initialize() + { d_context.push(); } + + void finish() + { d_context.pop(); } + /** Assert for propagation */ void assert(TNode assertion); |