From 43839eed3814cb4175869cd1fbbb4e9a5ece59dc Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Fri, 15 Jun 2012 03:24:51 +0000 Subject: 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. --- src/theory/booleans/circuit_propagator.h | 24 +++++++++++++++++------- 1 file changed, 17 insertions(+), 7 deletions(-) (limited to 'src/theory') 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 d_propagationQueue; @@ -234,21 +236,29 @@ public: /** * Construct a new CircuitPropagator. */ - CircuitPropagator(context::Context* context, std::vector& outLearnedLiterals, + CircuitPropagator(std::vector& 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); -- cgit v1.2.3