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) d_context()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. */ getAssignment(TNode n)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 initialize()92 void initialize() { d_context.push(); } 93 setNeedsFinish(bool value)94 void setNeedsFinish(bool value) { d_needsFinish = value; } 95 getNeedsFinish()96 bool getNeedsFinish() { return d_needsFinish; } 97 getLearnedLiterals()98 std::vector<Node>& getLearnedLiterals() { return d_learnedLiterals; } 99 finish()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 */ getBackEdges()117 const BackEdgesMap& getBackEdges() const { return d_backEdges; } 118 119 /** Invert a set value */ neg(AssignmentStatus 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). */ isAssigned(TNode n)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. */ isAssignedTo(TNode n,bool 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: DataClearer(context::Context * context,T & data)152 DataClearer(context::Context* context, T& data) 153 : context::ContextNotifyObj(context), d_data(data) 154 { 155 } 156 157 protected: contextNotifyPop()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: IsAssigned(CircuitPropagator & circuit)176 IsAssigned(CircuitPropagator& circuit) : d_circuit(circuit) {} 177 operator()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: IsAssignedTo(CircuitPropagator & circuit,bool value)188 IsAssignedTo(CircuitPropagator& circuit, bool value) 189 : d_circuit(circuit), d_value(value) 190 { 191 } 192 operator()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 */ assignAndEnqueue(TNode n,bool value)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 */ 317