src/theory/booleans/circuit_propagator.h

   1 /*********************                                                        */
   2 /*! \file circuit_propagator.h
   3  ** \verbatim
   4  ** Original author: mdeters
   5  ** Major contributors: dejan
   6  ** Minor contributors (to current version): barrett
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009-2012  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief A non-clausal circuit propagator for Boolean simplification
  13  **
  14  ** A non-clausal circuit propagator for Boolean simplification.
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #ifndef __CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H
  20 #define __CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H
  21
  22 #include <vector>
  23 #include <functional>
  24
  25 #include "theory/theory.h"
  26 #include "context/context.h"
  27 #include "util/hash.h"
  28 #include "expr/node.h"
  29 #include "context/cdhashset.h"
  30 #include "context/cdhashmap.h"
  31 #include "context/cdo.h"
  32
  33 namespace CVC4 {
  34 namespace theory {
  35 namespace booleans {
  36
  37
  38 /**
  39  * The main purpose of the CircuitPropagator class is to maintain the
  40  * state of the circuit for subsequent calls to propagate(), so that
  41  * the same fact is not output twice, so that the same edge in the
  42  * circuit isn't propagated twice, etc.
  43  */
  44 class CircuitPropagator {
  45
  46 public:
  47
  48   /**
  49    * Value of a particular node
  50    */
  51   enum AssignmentStatus {
  52     /** Node is currently unassigned */
  53     UNASSIGNED = 0,
  54     /** Node is assigned to true */
  55     ASSIGNED_TO_TRUE,
  56     /** Node is assigned to false */
  57     ASSIGNED_TO_FALSE,
  58   };
  59
  60   /** Invert a set value */
  61   static inline AssignmentStatus neg(AssignmentStatus value) {
  62     Assert(value != UNASSIGNED);
  63     if (value == ASSIGNED_TO_TRUE) return ASSIGNED_TO_FALSE;
  64     else return ASSIGNED_TO_TRUE;
  65   }
  66
  67   typedef std::hash_map<Node, std::vector<Node>, NodeHashFunction> BackEdgesMap;
  68
  69 private:
  70
  71   context::Context d_context;
  72
  73   /** The propagation queue */
  74   std::vector<TNode> d_propagationQueue;
  75
  76   /** A context-notify object that clears out stale data. */
  77   template <class T>
  78   class DataClearer : context::ContextNotifyObj {
  79     T& d_data;
  80   protected:
  81     void contextNotifyPop() {
  82       Trace("circuit-prop") << "CircuitPropagator::DataClearer: clearing data "
  83                             << "(size was " << d_data.size() << ")" << std::endl;
  84       d_data.clear();
  85     }
  86   public:
  87     DataClearer(context::Context* context, T& data) :
  88       context::ContextNotifyObj(context),
  89       d_data(data) {
  90     }
  91   };/* class DataClearer<T> */
  92
  93   /**
  94    * We have a propagation queue "clearer" object for when the user
  95    * context pops.  Normally the propagation queue should be empty,
  96    * but this keeps us safe in case there's still some rubbish around
  97    * on the queue.
  98    */
  99   DataClearer< std::vector<TNode> > d_propagationQueueClearer;
 100
 101   /** Are we in conflict? */
 102   context::CDO<bool> d_conflict;
 103
 104   /** Map of substitutions */
 105   std::vector<Node>& d_learnedLiterals;
 106
 107   /**
 108    * Similar data clearer for learned literals.
 109    */
 110   DataClearer< std::vector<Node> > d_learnedLiteralClearer;
 111
 112   /**
 113    * Back edges from nodes to where they are used.
 114    */
 115   BackEdgesMap d_backEdges;
 116
 117   /**
 118    * Similar data clearer for back edges.
 119    */
 120   DataClearer<BackEdgesMap> d_backEdgesClearer;
 121
 122   /** Nodes that have been attached already (computed forward edges for) */
 123   // All the nodes we've visited so far
 124   context::CDHashSet<Node, NodeHashFunction> d_seen;
 125
 126   /**
 127    * Assignment status of each node.
 128    */
 129   typedef context::CDHashMap<TNode, AssignmentStatus, TNodeHashFunction> AssignmentMap;
 130   AssignmentMap d_state;
 131
 132   /**
 133    * Assign Node in circuit with the value and add it to the queue; note conflicts.
 134    */
 135   void assignAndEnqueue(TNode n, bool value) {
 136
 137     Trace("circuit-prop") << "CircuitPropagator::assign(" << n << ", " << (value ? "true" : "false") << ")" << std::endl;
 138
 139     if (n.getKind() == kind::CONST_BOOLEAN) {
 140       // Assigning a constant to the opposite value is dumb
 141       if (value != n.getConst<bool>()) {
 142         d_conflict = true;
 143         return;
 144       }
 145     }
 146
 147     // Get the current assignement
 148     AssignmentStatus state = d_state[n];
 149
 150     if(state != UNASSIGNED) {
 151       // If the node is already assigned we might have a conflict
 152       if(value != (state == ASSIGNED_TO_TRUE)) {
 153         d_conflict = true;
 154       }
 155     } else {
 156       // If unassigned, mark it as assigned
 157       d_state[n] = value ? ASSIGNED_TO_TRUE : ASSIGNED_TO_FALSE;
 158       // Add for further propagation
 159       d_propagationQueue.push_back(n);
 160     }
 161   }
 162
 163 public:
 164   /** True iff Node is assigned in circuit (either true or false). */
 165   bool isAssigned(TNode n) const {
 166     AssignmentMap::const_iterator i = d_state.find(n);
 167     return i != d_state.end() && ((*i).second != UNASSIGNED);
 168   }
 169
 170   /** True iff Node is assigned to the value. */
 171   bool isAssignedTo(TNode n, bool value) const {
 172     AssignmentMap::const_iterator i = d_state.find(n);
 173     if (i == d_state.end()) return false;
 174     if (value && ((*i).second == ASSIGNED_TO_TRUE)) return true;
 175     if (!value && ((*i).second == ASSIGNED_TO_FALSE)) return true;
 176     return false;
 177   }
 178
 179   /** Get Node assignment in circuit.  Assert-fails if Node is unassigned. */
 180   bool getAssignment(TNode n) const {
 181     AssignmentMap::iterator i = d_state.find(n);
 182     Assert(i != d_state.end() && (*i).second != UNASSIGNED);
 183     return (*i).second == ASSIGNED_TO_TRUE;
 184   }
 185
 186 private:
 187   /** Predicate for use in STL functions. */
 188   class IsAssigned : public std::unary_function<TNode, bool> {
 189     CircuitPropagator& d_circuit;
 190   public:
 191     IsAssigned(CircuitPropagator& circuit) :
 192       d_circuit(circuit) {
 193     }
 194
 195     bool operator()(TNode in) const {
 196       return d_circuit.isAssigned(in);
 197     }
 198   };/* class IsAssigned */
 199
 200   /** Predicate for use in STL functions. */
 201   class IsAssignedTo : public std::unary_function<TNode, bool> {
 202     CircuitPropagator& d_circuit;
 203     bool d_value;
 204   public:
 205     IsAssignedTo(CircuitPropagator& circuit, bool value) :
 206       d_circuit(circuit),
 207       d_value(value) {
 208     }
 209
 210     bool operator()(TNode in) const {
 211       return d_circuit.isAssignedTo(in, d_value);
 212     }
 213   };/* class IsAssignedTo */
 214
 215   /**
 216    * Compute the map from nodes to the nodes that use it.
 217    */
 218   void computeBackEdges(TNode node);
 219
 220   /**
 221    * Propagate new information forward in circuit to
 222    * the parents of "in".
 223    */
 224   void propagateForward(TNode child, bool assignment);
 225
 226   /**
 227    * Propagate new information backward in circuit to
 228    * the children of "in".
 229    */
 230   void propagateBackward(TNode parent, bool assignment);
 231
 232   /** Whether to perform forward propagation */
 233   const bool d_forwardPropagation;
 234
 235   /** Whether to perform backward propagation */
 236   const bool d_backwardPropagation;
 237
 238 public:
 239   /**
 240    * Construct a new CircuitPropagator.
 241    */
 242   CircuitPropagator(std::vector<Node>& outLearnedLiterals,
 243                     bool enableForward = true, bool enableBackward = true) :
 244     d_context(),
 245     d_propagationQueue(),
 246     d_propagationQueueClearer(&d_context, d_propagationQueue),
 247     d_conflict(&d_context, false),
 248     d_learnedLiterals(outLearnedLiterals),
 249     d_learnedLiteralClearer(&d_context, outLearnedLiterals),
 250     d_backEdges(),
 251     d_backEdgesClearer(&d_context, d_backEdges),
 252     d_seen(&d_context),
 253     d_state(&d_context),
 254     d_forwardPropagation(enableForward),
 255     d_backwardPropagation(enableBackward) {
 256   }
 257
 258   // Use custom context to ensure propagator is reset after use
 259   void initialize()
 260   { d_context.push(); }
 261
 262   void finish()
 263   { d_context.pop(); }
 264
 265   /** Assert for propagation */
 266   void assertTrue(TNode assertion);
 267
 268   /**
 269    * Propagate through the asserted circuit propagator. New information discovered by the propagator
 270    * are put in the substitutions vector used in construction.
 271    *
 272    * @return true iff conflict found
 273    */
 274   bool propagate() CVC4_WARN_UNUSED_RESULT;
 275
 276   /**
 277    * Get the back edges of this circuit.
 278    */
 279   const BackEdgesMap& getBackEdges() const {
 280     return d_backEdges;
 281   }
 282
 283 };/* class CircuitPropagator */
 284
 285 }/* CVC4::theory::booleans namespace */
 286 }/* CVC4::theory namespace */
 287 }/* CVC4 namespace */
 288
 289 #endif /* __CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H */