diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-04 22:26:40 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-04 22:26:40 +0000 |
commit | 3609fb41d7744b3a7d74e44f7bedc4d4c522c938 (patch) | |
tree | 011a3fa796fdb98bb3b9a1b425d12c678535f294 /src/theory/booleans/circuit_propagator.h | |
parent | 468c5bc5d8b63ec6818813270225e09383dd79ff (diff) |
Added preprocessing pass that propagates unconstrained values - solves all of
the unconstrained examples in QF_AUFBV/brummayerbiere3 - should also help
generally on at least BV and maybe others.
Off by default for now - results are mixed and it's hard to evaluate with so
many existing assertion failures and segfaults - will re-evaluate once those
are fixed
Diffstat (limited to 'src/theory/booleans/circuit_propagator.h')
-rw-r--r-- | src/theory/booleans/circuit_propagator.h | 16 |
1 files changed, 11 insertions, 5 deletions
diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h index f5e4f4630..60e48dba2 100644 --- a/src/theory/booleans/circuit_propagator.h +++ b/src/theory/booleans/circuit_propagator.h @@ -68,10 +68,6 @@ public: private: - /** Back edges from nodes to where they are used */ - typedef std::hash_map<Node, std::vector<Node>, NodeHashFunction> BackEdgesMap; - BackEdgesMap d_backEdges; - /** The propagation queue */ std::vector<TNode> d_propagationQueue; @@ -111,6 +107,15 @@ private: */ DataClearer< std::vector<Node> > d_learnedLiteralClearer; + /** Back edges from nodes to where they are used */ + typedef std::hash_map<Node, std::vector<Node>, NodeHashFunction> BackEdgesMap; + BackEdgesMap d_backEdges; + + /** + * Similar data clearer for back edges. + */ + DataClearer<BackEdgesMap> d_backEdgesClearer; + /** Nodes that have been attached already (computed forward edges for) */ // All the nodes we've visited so far context::CDHashSet<TNode, TNodeHashFunction> d_seen; @@ -231,12 +236,13 @@ public: */ CircuitPropagator(context::Context* context, std::vector<Node>& outLearnedLiterals, bool enableForward = true, bool enableBackward = true) : - d_backEdges(), d_propagationQueue(), d_propagationQueueClearer(context, d_propagationQueue), d_conflict(context, false), d_learnedLiterals(outLearnedLiterals), d_learnedLiteralClearer(context, outLearnedLiterals), + d_backEdges(), + d_backEdgesClearer(context, d_backEdges), d_seen(context), d_state(context), d_forwardPropagation(enableForward), |