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