src/theory/booleans/circuit_propagator.h

   1 /*********************                                                        */
   2 /*! \file circuit_propagator.h
   3  ** \verbatim
   4  ** Original author: mdeters
   5  ** Major contributors: none
   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
  32 namespace CVC4 {
  33 namespace theory {
  34 namespace booleans {
  35
  36
  37 /**
  38  * The main purpose of the CircuitPropagator class is to maintain the
  39  * state of the circuit for subsequent calls to propagate(), so that
  40  * the same fact is not output twice, so that the same edge in the
  41  * circuit isn't propagated twice, etc.
  42  */
  43 class CircuitPropagator {
  44
  45 public:
  46
  47   /**
  48    * Value of a particular node
  49    */
  50   enum AssignmentStatus {
  51     /** Node is currently unassigned */
  52     UNASSIGNED = 0,
  53     /** Node is assigned to true */
  54     ASSIGNED_TO_TRUE,
  55     /** Node is assigned to false */
  56     ASSIGNED_TO_FALSE,
  57   };
  58
  59   /** Invert a set value */
  60   static inline AssignmentStatus neg(AssignmentStatus value) {
  61     Assert(value != UNASSIGNED);
  62     if (value == ASSIGNED_TO_TRUE) return ASSIGNED_TO_FALSE;
  63     else return ASSIGNED_TO_TRUE;
  64   }
  65
  66 private:
  67
  68   /** Back edges from nodes to where they are used */
  69   typedef std::hash_map<TNode, std::vector<TNode>, TNodeHashFunction> BackEdgesMap;
  70   BackEdgesMap d_backEdges;
  71
  72   /** The propagation queue */
  73   std::vector<TNode> d_propagationQueue;
  74
  75   /** Are we in conflict */
  76   bool d_conflict;
  77
  78   /** Map of substitutions */
  79   std::vector<Node>& d_learnedLiterals;
  80
  81   /** Nodes that have been attached already (computed forward edges for) */
  82   // All the nodes we've visited so far
  83   std::hash_set<TNode, TNodeHashFunction> d_seen;
  84
  85   /**
  86    * Assignment status of each node.
  87    */
  88   typedef std::hash_map<TNode, AssignmentStatus, TNodeHashFunction> AssignmentMap;
  89   AssignmentMap d_state;
  90
  91   /**
  92    * Assign Node in circuit with the value and add it to the queue; note conflicts.
  93    */
  94   void assignAndEnqueue(TNode n, bool value) {
  95
  96     Debug("circuit-prop") << "CircuitPropagator::assign(" << n << ", " << (value ? "true" : "false") << ")" << std::endl;
  97
  98     if (n.getKind() == kind::CONST_BOOLEAN) {
  99       // Assigning a constant to the opposite value is dumb
 100       if (value != n.getConst<bool>()) {
 101         d_conflict = true;
 102         return;
 103       }
 104     }
 105
 106     // Get the current assignement
 107     AssignmentStatus state = d_state[n];
 108
 109     if(state != UNASSIGNED) {
 110       // If the node is already assigned we might have a conflict
 111       if(value != (state == ASSIGNED_TO_TRUE)) {
 112         d_conflict = true;
 113       }
 114     } else {
 115       // If unassigned, mark it as assigned
 116       d_state[n] = value ? ASSIGNED_TO_TRUE : ASSIGNED_TO_FALSE;
 117       // Add for further propagation
 118       d_propagationQueue.push_back(n);
 119     }
 120   }
 121
 122   /** True iff Node is assigned in circuit (either true or false). */
 123   bool isAssigned(TNode n) const {
 124     AssignmentMap::const_iterator i = d_state.find(n);
 125     return i != d_state.end() && ((*i).second != UNASSIGNED);
 126   }
 127
 128   /** True iff Node is assigned to the value. */
 129   bool isAssignedTo(TNode n, bool value) const {
 130     AssignmentMap::const_iterator i = d_state.find(n);
 131     if (i == d_state.end()) return false;
 132     if (value && ((*i).second == ASSIGNED_TO_TRUE)) return true;
 133     if (!value && ((*i).second == ASSIGNED_TO_FALSE)) return true;
 134     return false;
 135   }
 136
 137   /** Get Node assignment in circuit.  Assert-fails if Node is unassigned. */
 138   bool getAssignment(TNode n) const {
 139     Assert(d_state.find(n) != d_state.end() && d_state.find(n)->second != UNASSIGNED);
 140     return d_state.find(n)->second == ASSIGNED_TO_TRUE;
 141   }
 142
 143   /** Predicate for use in STL functions. */
 144   class IsAssigned : public std::unary_function<TNode, bool> {
 145     CircuitPropagator& d_circuit;
 146   public:
 147     IsAssigned(CircuitPropagator& circuit) :
 148       d_circuit(circuit) {
 149     }
 150
 151     bool operator()(TNode in) const {
 152       return d_circuit.isAssigned(in);
 153     }
 154   };/* class IsAssigned */
 155
 156   /** Predicate for use in STL functions. */
 157   class IsAssignedTo : public std::unary_function<TNode, bool> {
 158     CircuitPropagator& d_circuit;
 159     bool d_value;
 160   public:
 161     IsAssignedTo(CircuitPropagator& circuit, bool value) :
 162       d_circuit(circuit),
 163       d_value(value) {
 164     }
 165
 166     bool operator()(TNode in) const {
 167       return d_circuit.isAssignedTo(in, d_value);
 168     }
 169   };/* class IsAssignedTo */
 170
 171   /**
 172    * Compute the map from nodes to the nodes that use it.
 173    */
 174   void computeBackEdges(TNode node);
 175
 176   /**
 177    * Propagate new information forward in circuit to
 178    * the parents of "in".
 179    */
 180   void propagateForward(TNode child, bool assignment);
 181
 182   /**
 183    * Propagate new information backward in circuit to
 184    * the children of "in".
 185    */
 186   void propagateBackward(TNode parent, bool assignment);
 187
 188   /** Whether to perform forward propagation */
 189   bool d_forwardPropagation;
 190   /** Whether to perform backward propagation */
 191   bool d_backwardPropagation;
 192   /** Whether to perform expensive propagations */
 193   bool d_expensivePropagation;
 194
 195 public:
 196   /**
 197    * Construct a new CircuitPropagator with the given atoms and backEdges.
 198    */
 199   CircuitPropagator(std::vector<Node>& outLearnedLiterals, bool enableForward = true, bool enableBackward = true, bool enableExpensive = true) :
 200     d_conflict(false),
 201     d_learnedLiterals(outLearnedLiterals),
 202     d_forwardPropagation(enableForward),
 203     d_backwardPropagation(enableBackward),
 204     d_expensivePropagation(enableExpensive)
 205   {
 206   }
 207
 208   /** Assert for propagation */
 209   void assert(TNode assertion);
 210
 211   /**
 212    * Propagate through the asserted circuit propagator. New information discovered by the propagator
 213    * are put in the subsitutions vector used in construction.
 214    *
 215    * @return true iff conflict found
 216    */
 217   bool propagate() CVC4_WARN_UNUSED_RESULT;
 218
 219 };/* class CircuitPropagator */
 220
 221 }/* CVC4::theory::booleans namespace */
 222 }/* CVC4::theory namespace */
 223 }/* CVC4 namespace */
 224
 225 #endif /* __CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H */