diff options
Diffstat (limited to 'src/theory/booleans/circuit_propagator.h')
-rw-r--r-- | src/theory/booleans/circuit_propagator.h | 207 |
1 files changed, 113 insertions, 94 deletions
diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h index f9efc20af..73a5be0f8 100644 --- a/src/theory/booleans/circuit_propagator.h +++ b/src/theory/booleans/circuit_propagator.h @@ -33,6 +33,7 @@ namespace CVC4 { namespace theory { namespace booleans { + /** * The main purpose of the CircuitPropagator class is to maintain the * state of the circuit for subsequent calls to propagate(), so that @@ -40,104 +41,103 @@ namespace booleans { * circuit isn't propagated twice, etc. */ class CircuitPropagator { - const std::vector<TNode>& d_atoms; - const std::hash_map<TNode, std::vector<TNode>, TNodeHashFunction>& d_backEdges; - class ConflictException : Exception { - public: - ConflictException() : Exception("A conflict was found in the CircuitPropagator") { - } - };/* class ConflictException */ +public: + + /** + * Value of a particular node + */ + enum AssignmentStatus { + /** Node is currently unassigned */ + UNASSIGNED = 0, + /** Node is assigned to true */ + ASSIGNED_TO_TRUE, + /** Node is assigned to false */ + ASSIGNED_TO_FALSE, + }; + + /** Invert a set value */ + static inline AssignmentStatus neg(AssignmentStatus value) { + Assert(value != UNASSIGNED); + if (value == ASSIGNED_TO_TRUE) return ASSIGNED_TO_FALSE; + else return ASSIGNED_TO_TRUE; + } + +private: + + /** Back edges from nodes to where they are used */ + typedef std::hash_map<TNode, std::vector<TNode>, TNodeHashFunction> BackEdgesMap; + BackEdgesMap d_backEdges; - enum { - ASSIGNMENT_MASK = 1, - IS_ASSIGNED_MASK = 2, - IS_PROPAGATED_FORWARD_MASK = 4, - IS_PROPAGATED_BACKWARD_MASK = 8 - };/* enum */ + /** The propagation queue */ + std::vector<TNode> d_propagationQueue; + + /** Are we in conflict */ + bool d_conflict; + + /** Map of substitutions */ + std::vector<Node>& d_learnedLiterals; + + /** Nodes that have been attached already (computed forward edges for) */ + // All the nodes we've visited so far + std::hash_set<TNode, TNodeHashFunction> d_seen; /** - * For each Node we care about, we have a 4-bit state: - * Bit 0 (ASSIGNMENT_MASK) is set to indicate the current assignment - * Bit 1 (IS_ASSIGNED_MASK) is set if a value is assigned - * Bit 2 (IS_PROPAGATED_FORWARD) is set to indicate it's been propagated forward - * Bit 2 (IS_PROPAGATED_BACKWARD) is set to indicate it's been propagated backward + * Assignment status of each node. */ - std::hash_map<TNode, unsigned, TNodeHashFunction> d_state; - - /** Assign Node in circuit with the value and add it to the changed vector; note conflicts. */ - void assign(TNode n, bool b, std::vector<TNode>& changed) { - if(n.getMetaKind() == kind::metakind::CONSTANT) { - bool c = n.getConst<bool>(); - if(c != b) { - Debug("circuit-prop") << "while assigning(" << b << "): " << n - << ", constant conflict" << std::endl; - throw ConflictException(); - } else { - Debug("circuit-prop") << "assigning(" << b << "): " << n - << ", nothing to do" << std::endl; + typedef std::hash_map<TNode, AssignmentStatus, TNodeHashFunction> AssignmentMap; + AssignmentMap d_state; + + /** + * Assign Node in circuit with the value and add it to the queue; note conflicts. + */ + void assignAndEnqueue(TNode n, bool value) { + + Debug("circuit-prop") << "CircuitPropagator::assign(" << n << ", " << (value ? "true" : "false") << ")" << std::endl; + + if (n.getKind() == kind::CONST_BOOLEAN) { + // Assigning a constant to the opposite value is dumb + if (value != n.getConst<bool>()) { + d_conflict = true; + return; } - return; } - unsigned& state = d_state[n]; - if((state & IS_ASSIGNED_MASK) != 0) {// if assigned already - if(((state & ASSIGNMENT_MASK) != 0) != b) {// conflict - Debug("circuit-prop") << "while assigning(" << b << "): " << n - << ", got conflicting assignment(" << assignment(n) << "): " - << n << std::endl; - throw ConflictException(); - } else { - Debug("circuit-prop") << "already assigned(" << b << "): " << n << std::endl; + + // Get the current assignement + AssignmentStatus state = d_state[n]; + + if(state != UNASSIGNED) { + // If the node is already assigned we might have a conflict + if(value != (state == ASSIGNED_TO_TRUE)) { + d_conflict = true; } - } else {// if unassigned - Debug("circuit-prop") << "assigning(" << b << "): " << n << std::endl; - state |= IS_ASSIGNED_MASK | (b ? ASSIGNMENT_MASK : 0); - changed.push_back(n); + } else { + // If unassigned, mark it as assigned + d_state[n] = value ? ASSIGNED_TO_TRUE : ASSIGNED_TO_FALSE; + // Add for further propagation + d_propagationQueue.push_back(n); } } - /** True iff Node is assigned in circuit (either true or false). */ - bool isAssigned(TNode n) { - return (d_state[n] & IS_ASSIGNED_MASK) != 0; - } + /** True iff Node is assigned in circuit (either true or false). */ bool isAssigned(TNode n) const { - std::hash_map<TNode, unsigned, TNodeHashFunction>::const_iterator i = d_state.find(n); - return i != d_state.end() && ((*i).second & IS_ASSIGNED_MASK) != 0; - } - /** True iff Node is assigned in circuit with the value given. */ - bool isAssignedTo(TNode n, bool b) { - unsigned state = d_state[n]; - return (state & IS_ASSIGNED_MASK) && - (state & ASSIGNMENT_MASK) == (b ? ASSIGNMENT_MASK : 0); + AssignmentMap::const_iterator i = d_state.find(n); + return i != d_state.end() && ((*i).second != UNASSIGNED); } - /** True iff Node is assigned in circuit (either true or false). */ - bool isAssignedTo(TNode n, bool b) const { - std::hash_map<TNode, unsigned, TNodeHashFunction>::const_iterator i = d_state.find(n); - return i != d_state.end() && - ((*i).second & IS_ASSIGNED_MASK) && - ((*i).second & ASSIGNMENT_MASK) == (b ? ASSIGNMENT_MASK : 0); + + /** True iff Node is assigned to the value. */ + bool isAssignedTo(TNode n, bool value) const { + AssignmentMap::const_iterator i = d_state.find(n); + if (i == d_state.end()) return false; + if (value && ((*i).second == ASSIGNED_TO_TRUE)) return true; + if (!value && ((*i).second == ASSIGNED_TO_FALSE)) return true; + return false; } + /** Get Node assignment in circuit. Assert-fails if Node is unassigned. */ - bool assignment(TNode n) { - unsigned state = d_state[n]; - Assert((state & IS_ASSIGNED_MASK) != 0); - return (state & ASSIGNMENT_MASK) != 0; - } - /** Has this node already been propagated forward? */ - bool isPropagatedForward(TNode n) { - return (d_state[n] & IS_PROPAGATED_FORWARD_MASK) != 0; - } - /** Has this node already been propagated backward? */ - bool isPropagatedBackward(TNode n) { - return (d_state[n] & IS_PROPAGATED_BACKWARD_MASK) != 0; - } - /** Mark this node as already having been propagated forward. */ - void setPropagatedForward(TNode n) { - d_state[n] |= IS_PROPAGATED_FORWARD_MASK; - } - /** Mark this node as already having been propagated backward. */ - void setPropagatedBackward(TNode n) { - d_state[n] |= IS_PROPAGATED_BACKWARD_MASK; + bool getAssignment(TNode n) const { + Assert(d_state.find(n) != d_state.end() && d_state.find(n)->second != UNASSIGNED); + return d_state.find(n)->second == ASSIGNED_TO_TRUE; } /** Predicate for use in STL functions. */ @@ -169,33 +169,52 @@ class CircuitPropagator { };/* class IsAssignedTo */ /** - * Propagate new information (in = polarity) forward in circuit to + * Compute the map from nodes to the nodes that use it. + */ + void computeBackEdges(TNode node); + + /** + * Propagate new information forward in circuit to * the parents of "in". */ - void propagateForward(TNode in, bool polarity, std::vector<TNode>& newFacts); + void propagateForward(TNode child, bool assignment); + /** - * Propagate new information (in = polarity) backward in circuit to + * Propagate new information backward in circuit to * the children of "in". */ - void propagateBackward(TNode in, bool polarity, std::vector<TNode>& newFacts); + void propagateBackward(TNode parent, bool assignment); + + /** Whether to perform forward propagation */ + bool d_forwardPropagation; + /** Whether to perform backward propagation */ + bool d_backwardPropagation; + /** Whether to perform expensive propagations */ + bool d_expensivePropagation; public: /** * Construct a new CircuitPropagator with the given atoms and backEdges. */ - CircuitPropagator(const std::vector<TNode>& atoms, const std::hash_map<TNode, std::vector<TNode>, TNodeHashFunction>& backEdges) - : d_atoms(atoms), - d_backEdges(backEdges) { + CircuitPropagator(std::vector<Node>& outLearnedLiterals, bool enableForward = true, bool enableBackward = true, bool enableExpensive = true) : + d_conflict(false), + d_learnedLiterals(outLearnedLiterals), + d_forwardPropagation(enableForward), + d_backwardPropagation(enableBackward), + d_expensivePropagation(enableExpensive) + { } + /** Assert for propagation */ + void assert(TNode assertion); + /** - * Propagate new information (in == polarity) through the circuit - * propagator. New information discovered by the propagator are put - * in the (output-only) newFacts vector. + * Propagate through the asserted circuit propagator. New information discovered by the propagator + * are put in the subsitutions vector used in construction. * * @return true iff conflict found */ - bool propagate(TNode in, bool polarity, std::vector<Node>& newFacts) CVC4_WARN_UNUSED_RESULT; + bool propagate() CVC4_WARN_UNUSED_RESULT; };/* class CircuitPropagator */ |