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

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),