diff options
Diffstat (limited to 'src/theory/booleans/circuit_propagator.h')
-rw-r--r-- | src/theory/booleans/circuit_propagator.h | 206 |
1 files changed, 206 insertions, 0 deletions
diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h new file mode 100644 index 000000000..f9efc20af --- /dev/null +++ b/src/theory/booleans/circuit_propagator.h @@ -0,0 +1,206 @@ +/********************* */ +/*! \file circuit_propagator.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief A non-clausal circuit propagator for Boolean simplification + ** + ** A non-clausal circuit propagator for Boolean simplification. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H +#define __CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H + +#include <vector> +#include <functional> + +#include "theory/theory.h" +#include "context/context.h" +#include "util/hash.h" +#include "expr/node.h" + +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 + * the same fact is not output twice, so that the same edge in the + * 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 */ + + enum { + ASSIGNMENT_MASK = 1, + IS_ASSIGNED_MASK = 2, + IS_PROPAGATED_FORWARD_MASK = 4, + IS_PROPAGATED_BACKWARD_MASK = 8 + };/* enum */ + + /** + * 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 + */ + 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; + } + 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; + } + } else {// if unassigned + Debug("circuit-prop") << "assigning(" << b << "): " << n << std::endl; + state |= IS_ASSIGNED_MASK | (b ? ASSIGNMENT_MASK : 0); + changed.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); + } + /** 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); + } + /** 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; + } + + /** Predicate for use in STL functions. */ + class IsAssigned : public std::unary_function<TNode, bool> { + CircuitPropagator& d_circuit; + public: + IsAssigned(CircuitPropagator& circuit) : + d_circuit(circuit) { + } + + bool operator()(TNode in) const { + return d_circuit.isAssigned(in); + } + };/* class IsAssigned */ + + /** Predicate for use in STL functions. */ + class IsAssignedTo : public std::unary_function<TNode, bool> { + CircuitPropagator& d_circuit; + bool d_value; + public: + IsAssignedTo(CircuitPropagator& circuit, bool value) : + d_circuit(circuit), + d_value(value) { + } + + bool operator()(TNode in) const { + return d_circuit.isAssignedTo(in, d_value); + } + };/* class IsAssignedTo */ + + /** + * Propagate new information (in = polarity) forward in circuit to + * the parents of "in". + */ + void propagateForward(TNode in, bool polarity, std::vector<TNode>& newFacts); + /** + * Propagate new information (in = polarity) backward in circuit to + * the children of "in". + */ + void propagateBackward(TNode in, bool polarity, std::vector<TNode>& newFacts); + +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) { + } + + /** + * Propagate new information (in == polarity) through the circuit + * propagator. New information discovered by the propagator are put + * in the (output-only) newFacts vector. + * + * @return true iff conflict found + */ + bool propagate(TNode in, bool polarity, std::vector<Node>& newFacts) CVC4_WARN_UNUSED_RESULT; + +};/* class CircuitPropagator */ + +}/* CVC4::theory::booleans namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H */ |