src/theory/booleans/circuit_propagator.h

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