Reorder circuit propagator class.

1 files changed, 189 insertions, 174 deletions

diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h
index bd6da8742..adb1eb42f 100644
--- a/src/theory/booleans/circuit_propagator.h
+++ b/src/theory/booleans/circuit_propagator.h
@@ -23,33 +23,32 @@
 #include <unordered_map>
 #include <vector>
 
-#include "theory/theory.h"
-#include "context/context.h"
-#include "util/hash.h"
-#include "expr/node.h"
-#include "context/cdhashset.h"
 #include "context/cdhashmap.h"
+#include "context/cdhashset.h"
 #include "context/cdo.h"
+#include "context/context.h"
+#include "expr/node.h"
+#include "theory/theory.h"
+#include "util/hash.h"
 
 namespace CVC4 {
 namespace theory {
 namespace booleans {
 
-
 /**
  * The main purpose of the CircuitPropagator class is to maintain the
  * state of the circuit for subsequent calls to propagate(), so that
  * the same fact is not output twice, so that the same edge in the
  * circuit isn't propagated twice, etc.
  */
-class CircuitPropagator {
-
-public:
-
+class CircuitPropagator
+{
+ public:
   /**
    * Value of a particular node
    */
-  enum AssignmentStatus {
+  enum AssignmentStatus
+  {
     /** Node is currently unassigned */
     UNASSIGNED = 0,
     /** Node is assigned to true */
@@ -58,119 +57,85 @@ public:
     ASSIGNED_TO_FALSE,
   };
 
-  /** Invert a set value */
-  static inline AssignmentStatus neg(AssignmentStatus value) {
-    Assert(value != UNASSIGNED);
-    if (value == ASSIGNED_TO_TRUE) return ASSIGNED_TO_FALSE;
-    else return ASSIGNED_TO_TRUE;
-  }
-
-  typedef std::unordered_map<Node, std::vector<Node>, NodeHashFunction> BackEdgesMap;
-
-private:
-
-  context::Context d_context;
-
-  /** The propagation queue */
-  std::vector<TNode> d_propagationQueue;
-
-  /** A context-notify object that clears out stale data. */
-  template <class T>
-  class DataClearer : context::ContextNotifyObj {
-    T& d_data;
-  protected:
-   void contextNotifyPop() override
-   {
-     Trace("circuit-prop") << "CircuitPropagator::DataClearer: clearing data "
-                           << "(size was " << d_data.size() << ")" << std::endl;
-     d_data.clear();
-    }
-  public:
-    DataClearer(context::Context* context, T& data) :
-      context::ContextNotifyObj(context),
-      d_data(data) {
-    }
-  };/* class DataClearer<T> */
+  typedef std::unordered_map<Node, std::vector<Node>, NodeHashFunction>
+      BackEdgesMap;
 
   /**
-   * We have a propagation queue "clearer" object for when the user
-   * context pops.  Normally the propagation queue should be empty,
-   * but this keeps us safe in case there's still some rubbish around
-   * on the queue.
+   * Construct a new CircuitPropagator.
    */
-  DataClearer< std::vector<TNode> > d_propagationQueueClearer;
+  CircuitPropagator(std::vector<Node>& outLearnedLiterals,
+                    bool enableForward = true,
+                    bool enableBackward = true)
+      : d_context(),
+        d_propagationQueue(),
+        d_propagationQueueClearer(&d_context, d_propagationQueue),
+        d_conflict(&d_context, false),
+        d_learnedLiterals(outLearnedLiterals),
+        d_learnedLiteralClearer(&d_context, outLearnedLiterals),
+        d_backEdges(),
+        d_backEdgesClearer(&d_context, d_backEdges),
+        d_seen(&d_context),
+        d_state(&d_context),
+        d_forwardPropagation(enableForward),
+        d_backwardPropagation(enableBackward),
+        d_needsFinish(false)
+  {
+  }
 
-  /** Are we in conflict? */
-  context::CDO<bool> d_conflict;
+  /** Get Node assignment in circuit.  Assert-fails if Node is unassigned. */
+  bool getAssignment(TNode n) const
+  {
+    AssignmentMap::iterator i = d_state.find(n);
+    Assert(i != d_state.end() && (*i).second != UNASSIGNED);
+    return (*i).second == ASSIGNED_TO_TRUE;
+  }
 
-  /** Map of substitutions */
-  std::vector<Node>& d_learnedLiterals;
+  // Use custom context to ensure propagator is reset after use
+  void initialize() { d_context.push(); }
 
-  /**
-   * Similar data clearer for learned literals.
-   */
-  DataClearer< std::vector<Node> > d_learnedLiteralClearer;
+  void setNeedsFinish(bool value) { d_needsFinish = value; }
 
-  /**
-   * Back edges from nodes to where they are used.
-   */
-  BackEdgesMap d_backEdges;
+  bool getNeedsFinish() { return d_needsFinish; }
 
-  /**
-   * Similar data clearer for back edges.
-   */
-  DataClearer<BackEdgesMap> d_backEdgesClearer;
+  void finish() { d_context.pop(); }
 
-  /** Nodes that have been attached already (computed forward edges for) */
-  // All the nodes we've visited so far
-  context::CDHashSet<Node, NodeHashFunction> d_seen;
+  /** Assert for propagation */
+  void assertTrue(TNode assertion);
 
   /**
-   * Assignment status of each node.
+   * Propagate through the asserted circuit propagator. New information
+   * discovered by the propagator are put in the substitutions vector used in
+   * construction.
+   *
+   * @return true iff conflict found
    */
-  typedef context::CDHashMap<TNode, AssignmentStatus, TNodeHashFunction> AssignmentMap;
-  AssignmentMap d_state;
+  bool propagate() CVC4_WARN_UNUSED_RESULT;
 
   /**
-   * Assign Node in circuit with the value and add it to the queue; note conflicts.
+   * Get the back edges of this circuit.
    */
-  void assignAndEnqueue(TNode n, bool value) {
-
-    Trace("circuit-prop") << "CircuitPropagator::assign(" << n << ", " << (value ? "true" : "false") << ")" << std::endl;
+  const BackEdgesMap& getBackEdges() const { return d_backEdges; }
 
-    if (n.getKind() == kind::CONST_BOOLEAN) {
-      // Assigning a constant to the opposite value is dumb
-      if (value != n.getConst<bool>()) {
-        d_conflict = true;
-        return;
-      }
-    }
-
-    // Get the current assignment
-    AssignmentStatus state = d_state[n];
-
-    if(state != UNASSIGNED) {
-      // If the node is already assigned we might have a conflict
-      if(value != (state == ASSIGNED_TO_TRUE)) {
-        d_conflict = true;
-      }
-    } else {
-      // If unassigned, mark it as assigned
-      d_state[n] = value ? ASSIGNED_TO_TRUE : ASSIGNED_TO_FALSE;
-      // Add for further propagation
-      d_propagationQueue.push_back(n);
-    }
+  /** Invert a set value */
+  static inline AssignmentStatus neg(AssignmentStatus value)
+  {
+    Assert(value != UNASSIGNED);
+    if (value == ASSIGNED_TO_TRUE)
+      return ASSIGNED_TO_FALSE;
+    else
+      return ASSIGNED_TO_TRUE;
   }
 
-public:
   /** True iff Node is assigned in circuit (either true or false). */
-  bool isAssigned(TNode n) const {
+  bool isAssigned(TNode n) const
+  {
     AssignmentMap::const_iterator i = d_state.find(n);
     return i != d_state.end() && ((*i).second != UNASSIGNED);
   }
 
   /** True iff Node is assigned to the value. */
-  bool isAssignedTo(TNode n, bool value) const {
+  bool isAssignedTo(TNode n, bool value) const
+  {
     AssignmentMap::const_iterator i = d_state.find(n);
     if (i == d_state.end()) return false;
     if (value && ((*i).second == ASSIGNED_TO_TRUE)) return true;
@@ -178,41 +143,103 @@ public:
     return false;
   }
 
-  /** Get Node assignment in circuit.  Assert-fails if Node is unassigned. */
-  bool getAssignment(TNode n) const {
-    AssignmentMap::iterator i = d_state.find(n);
-    Assert(i != d_state.end() && (*i).second != UNASSIGNED);
-    return (*i).second == ASSIGNED_TO_TRUE;
-  }
+ private:
+  /** A context-notify object that clears out stale data. */
+  template <class T>
+  class DataClearer : context::ContextNotifyObj
+  {
+   public:
+    DataClearer(context::Context* context, T& data)
+        : context::ContextNotifyObj(context), d_data(data)
+    {
+    }
+
+   protected:
+    void contextNotifyPop() override
+    {
+      Trace("circuit-prop")
+          << "CircuitPropagator::DataClearer: clearing data "
+          << "(size was " << d_data.size() << ")" << std::endl;
+      d_data.clear();
+    }
+
+   private:
+    T& d_data;
+  }; /* class DataClearer<T> */
 
-private:
   /** Predicate for use in STL functions. */
-  class IsAssigned : public std::unary_function<TNode, bool> {
+  class IsAssigned : public std::unary_function<TNode, bool>
+  {
     CircuitPropagator& d_circuit;
-  public:
-    IsAssigned(CircuitPropagator& circuit) :
-      d_circuit(circuit) {
-    }
 
-    bool operator()(TNode in) const {
-      return d_circuit.isAssigned(in);
-    }
-  };/* class IsAssigned */
+   public:
+    IsAssigned(CircuitPropagator& circuit) : d_circuit(circuit) {}
+
+    bool operator()(TNode in) const { return d_circuit.isAssigned(in); }
+  }; /* class IsAssigned */
 
   /** Predicate for use in STL functions. */
-  class IsAssignedTo : public std::unary_function<TNode, bool> {
+  class IsAssignedTo : public std::unary_function<TNode, bool>
+  {
     CircuitPropagator& d_circuit;
     bool d_value;
-  public:
-    IsAssignedTo(CircuitPropagator& circuit, bool value) :
-      d_circuit(circuit),
-      d_value(value) {
+
+   public:
+    IsAssignedTo(CircuitPropagator& circuit, bool value)
+        : d_circuit(circuit), d_value(value)
+    {
     }
 
-    bool operator()(TNode in) const {
+    bool operator()(TNode in) const
+    {
       return d_circuit.isAssignedTo(in, d_value);
     }
-  };/* class IsAssignedTo */
+  }; /* class IsAssignedTo */
+
+  /**
+   * Assignment status of each node.
+   */
+  typedef context::CDHashMap<TNode, AssignmentStatus, TNodeHashFunction>
+      AssignmentMap;
+
+  /**
+   * Assign Node in circuit with the value and add it to the queue; note
+   * conflicts.
+   */
+  void assignAndEnqueue(TNode n, bool value)
+  {
+    Trace("circuit-prop") << "CircuitPropagator::assign(" << n << ", "
+                          << (value ? "true" : "false") << ")" << std::endl;
+
+    if (n.getKind() == kind::CONST_BOOLEAN)
+    {
+      // Assigning a constant to the opposite value is dumb
+      if (value != n.getConst<bool>())
+      {
+        d_conflict = true;
+        return;
+      }
+    }
+
+    // Get the current assignment
+    AssignmentStatus state = d_state[n];
+
+    if (state != UNASSIGNED)
+    {
+      // If the node is already assigned we might have a conflict
+      if (value != (state == ASSIGNED_TO_TRUE))
+      {
+        d_conflict = true;
+      }
+    }
+    else
+    {
+      // If unassigned, mark it as assigned
+      d_state[n] = value ? ASSIGNED_TO_TRUE : ASSIGNED_TO_FALSE;
+      // Add for further propagation
+      d_propagationQueue.push_back(n);
+    }
+  }
 
   /**
    * Compute the map from nodes to the nodes that use it.
@@ -231,71 +258,59 @@ private:
    */
   void propagateBackward(TNode parent, bool assignment);
 
-  /** Whether to perform forward propagation */
-  const bool d_forwardPropagation;
-
-  /** Whether to perform backward propagation */
-  const bool d_backwardPropagation;
+  context::Context d_context;
 
-  /* Does the current state require a call to finish()? */
-  bool d_needsFinish;
+  /** The propagation queue */
+  std::vector<TNode> d_propagationQueue;
 
-public:
   /**
-   * Construct a new CircuitPropagator.
+   * We have a propagation queue "clearer" object for when the user
+   * context pops.  Normally the propagation queue should be empty,
+   * but this keeps us safe in case there's still some rubbish around
+   * on the queue.
    */
- CircuitPropagator(std::vector<Node>& outLearnedLiterals,
-                   bool enableForward = true,
-                   bool enableBackward = true)
-     : d_context(),
-       d_propagationQueue(),
-       d_propagationQueueClearer(&d_context, d_propagationQueue),
-       d_conflict(&d_context, false),
-       d_learnedLiterals(outLearnedLiterals),
-       d_learnedLiteralClearer(&d_context, outLearnedLiterals),
-       d_backEdges(),
-       d_backEdgesClearer(&d_context, d_backEdges),
-       d_seen(&d_context),
-       d_state(&d_context),
-       d_forwardPropagation(enableForward),
-       d_backwardPropagation(enableBackward),
-       d_needsFinish(false)
- {
- }
-
-  // Use custom context to ensure propagator is reset after use
-  void initialize()
-  { d_context.push(); }
-
-  void setNeedsFinish(bool value) { d_needsFinish = value; }
+  DataClearer<std::vector<TNode> > d_propagationQueueClearer;
 
-  bool getNeedsFinish() { return d_needsFinish; }
+  /** Are we in conflict? */
+  context::CDO<bool> d_conflict;
 
-  void finish()
-  { d_context.pop(); }
+  /** Map of substitutions */
+  std::vector<Node>& d_learnedLiterals;
 
-  /** Assert for propagation */
-  void assertTrue(TNode assertion);
+  /**
+   * Similar data clearer for learned literals.
+   */
+  DataClearer<std::vector<Node> > d_learnedLiteralClearer;
 
   /**
-   * Propagate through the asserted circuit propagator. New information discovered by the propagator
-   * are put in the substitutions vector used in construction.
-   *
-   * @return true iff conflict found
+   * Back edges from nodes to where they are used.
    */
-  bool propagate() CVC4_WARN_UNUSED_RESULT;
+  BackEdgesMap d_backEdges;
 
   /**
-   * Get the back edges of this circuit.
+   * Similar data clearer for back edges.
    */
-  const BackEdgesMap& getBackEdges() const {
-    return d_backEdges;
-  }
+  DataClearer<BackEdgesMap> d_backEdgesClearer;
+
+  /** Nodes that have been attached already (computed forward edges for) */
+  // All the nodes we've visited so far
+  context::CDHashSet<Node, NodeHashFunction> d_seen;
+
+  AssignmentMap d_state;
+
+  /** Whether to perform forward propagation */
+  const bool d_forwardPropagation;
+
+  /** Whether to perform backward propagation */
+  const bool d_backwardPropagation;
+
+  /* Does the current state require a call to finish()? */
+  bool d_needsFinish;
 
-};/* class CircuitPropagator */
+}; /* class CircuitPropagator */
 
-}/* CVC4::theory::booleans namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+}  // namespace booleans
+}  // namespace theory
+}  // namespace CVC4
 
 #endif /* __CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H */