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 private:
  68
  69   context::Context d_context;
  70
  71   /** The propagation queue */
  72   std::vector<TNode> d_propagationQueue;
  73
  74   /** A context-notify object that clears out stale data. */
  75   template <class T>
  76   class DataClearer : context::ContextNotifyObj {
  77     T& d_data;
  78   protected:
  79     void contextNotifyPop() {
  80       Trace("circuit-prop") << "CircuitPropagator::DataClearer: clearing data "
  81                             << "(size was " << d_data.size() << ")" << std::endl;
  82       d_data.clear();
  83     }
  84   public:
  85     DataClearer(context::Context* context, T& data) :
  86       context::ContextNotifyObj(context),
  87       d_data(data) {
  88     }
  89   };/* class DataClearer<T> */
  90
  91   /**
  92    * We have a propagation queue "clearer" object for when the user
  93    * context pops.  Normally the propagation queue should be empty,
  94    * but this keeps us safe in case there's still some rubbish around
  95    * on the queue.
  96    */
  97   DataClearer< std::vector<TNode> > d_propagationQueueClearer;
  98
  99   /** Are we in conflict */
 100   context::CDO<bool> d_conflict;
 101
 102   /** Map of substitutions */
 103   std::vector<Node>& d_learnedLiterals;
 104
 105   /**
 106    * Similar data clearer for learned literals.
 107    */
 108   DataClearer< std::vector<Node> > d_learnedLiteralClearer;
 109
 110   /** Back edges from nodes to where they are used */
 111   typedef std::hash_map<Node, std::vector<Node>, NodeHashFunction> BackEdgesMap;
 112   BackEdgesMap d_backEdges;
 113
 114   /**
 115    * Similar data clearer for back edges.
 116    */
 117   DataClearer<BackEdgesMap> d_backEdgesClearer;
 118
 119   /** Nodes that have been attached already (computed forward edges for) */
 120   // All the nodes we've visited so far
 121   context::CDHashSet<Node, NodeHashFunction> d_seen;
 122
 123   /**
 124    * Assignment status of each node.
 125    */
 126   typedef context::CDHashMap<TNode, AssignmentStatus, TNodeHashFunction> AssignmentMap;
 127   AssignmentMap d_state;
 128
 129   /**
 130    * Assign Node in circuit with the value and add it to the queue; note conflicts.
 131    */
 132   void assignAndEnqueue(TNode n, bool value) {
 133
 134     Trace("circuit-prop") << "CircuitPropagator::assign(" << n << ", " << (value ? "true" : "false") << ")" << std::endl;
 135
 136     if (n.getKind() == kind::CONST_BOOLEAN) {
 137       // Assigning a constant to the opposite value is dumb
 138       if (value != n.getConst<bool>()) {
 139         d_conflict = true;
 140         return;
 141       }
 142     }
 143
 144     // Get the current assignement
 145     AssignmentStatus state = d_state[n];
 146
 147     if(state != UNASSIGNED) {
 148       // If the node is already assigned we might have a conflict
 149       if(value != (state == ASSIGNED_TO_TRUE)) {
 150         d_conflict = true;
 151       }
 152     } else {
 153       // If unassigned, mark it as assigned
 154       d_state[n] = value ? ASSIGNED_TO_TRUE : ASSIGNED_TO_FALSE;
 155       // Add for further propagation
 156       d_propagationQueue.push_back(n);
 157     }
 158   }
 159
 160   /** True iff Node is assigned in circuit (either true or false). */
 161   bool isAssigned(TNode n) const {
 162     AssignmentMap::const_iterator i = d_state.find(n);
 163     return i != d_state.end() && ((*i).second != UNASSIGNED);
 164   }
 165
 166   /** True iff Node is assigned to the value. */
 167   bool isAssignedTo(TNode n, bool value) const {
 168     AssignmentMap::const_iterator i = d_state.find(n);
 169     if (i == d_state.end()) return false;
 170     if (value && ((*i).second == ASSIGNED_TO_TRUE)) return true;
 171     if (!value && ((*i).second == ASSIGNED_TO_FALSE)) return true;
 172     return false;
 173   }
 174
 175   /** Get Node assignment in circuit.  Assert-fails if Node is unassigned. */
 176   bool getAssignment(TNode n) const {
 177     AssignmentMap::iterator i = d_state.find(n);
 178     Assert(i != d_state.end() && (*i).second != UNASSIGNED);
 179     return (*i).second == ASSIGNED_TO_TRUE;
 180   }
 181
 182   /** Predicate for use in STL functions. */
 183   class IsAssigned : public std::unary_function<TNode, bool> {
 184     CircuitPropagator& d_circuit;
 185   public:
 186     IsAssigned(CircuitPropagator& circuit) :
 187       d_circuit(circuit) {
 188     }
 189
 190     bool operator()(TNode in) const {
 191       return d_circuit.isAssigned(in);
 192     }
 193   };/* class IsAssigned */
 194
 195   /** Predicate for use in STL functions. */
 196   class IsAssignedTo : public std::unary_function<TNode, bool> {
 197     CircuitPropagator& d_circuit;
 198     bool d_value;
 199   public:
 200     IsAssignedTo(CircuitPropagator& circuit, bool value) :
 201       d_circuit(circuit),
 202       d_value(value) {
 203     }
 204
 205     bool operator()(TNode in) const {
 206       return d_circuit.isAssignedTo(in, d_value);
 207     }
 208   };/* class IsAssignedTo */
 209
 210   /**
 211    * Compute the map from nodes to the nodes that use it.
 212    */
 213   void computeBackEdges(TNode node);
 214
 215   /**
 216    * Propagate new information forward in circuit to
 217    * the parents of "in".
 218    */
 219   void propagateForward(TNode child, bool assignment);
 220
 221   /**
 222    * Propagate new information backward in circuit to
 223    * the children of "in".
 224    */
 225   void propagateBackward(TNode parent, bool assignment);
 226
 227   /** Whether to perform forward propagation */
 228   const bool d_forwardPropagation;
 229
 230   /** Whether to perform backward propagation */
 231   const bool d_backwardPropagation;
 232
 233 public:
 234   /**
 235    * Construct a new CircuitPropagator.
 236    */
 237   CircuitPropagator(std::vector<Node>& outLearnedLiterals,
 238                     bool enableForward = true, bool enableBackward = true) :
 239     d_context(),
 240     d_propagationQueue(),
 241     d_propagationQueueClearer(&d_context, d_propagationQueue),
 242     d_conflict(&d_context, false),
 243     d_learnedLiterals(outLearnedLiterals),
 244     d_learnedLiteralClearer(&d_context, outLearnedLiterals),
 245     d_backEdges(),
 246     d_backEdgesClearer(&d_context, d_backEdges),
 247     d_seen(&d_context),
 248     d_state(&d_context),
 249     d_forwardPropagation(enableForward),
 250     d_backwardPropagation(enableBackward) {
 251   }
 252
 253   // Use custom context to ensure propagator is reset after use
 254   void initialize()
 255   { d_context.push(); }
 256
 257   void finish()
 258   { d_context.pop(); }
 259
 260   /** Assert for propagation */
 261   void assertTrue(TNode assertion);
 262
 263   /**
 264    * Propagate through the asserted circuit propagator. New information discovered by the propagator
 265    * are put in the substitutions vector used in construction.
 266    *
 267    * @return true iff conflict found
 268    */
 269   bool propagate() CVC4_WARN_UNUSED_RESULT;
 270
 271 };/* class CircuitPropagator */
 272
 273 }/* CVC4::theory::booleans namespace */
 274 }/* CVC4::theory namespace */
 275 }/* CVC4 namespace */
 276
 277 #endif /* __CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H */