src/theory/booleans/circuit_propagator.h

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