Merge from nonclausal-simplification-v2 branch:

* Preprocessing-time, non-clausal, Boolean simplification round to
  support "quasi-non-linear rewrites" as discussed at last few meetings.

* --simplification=none is the default for now, but we'll probably
  change that to --simplification=incremental.  --simplification=batch
  is also a possibility.  See --simplification=help for details.

* RecursionBreaker<T> now uses a hash set for the seen trail.
* Fixes to TLS stuff to support that.
* Fixes to theory and SmtEngine documentation.
* Fixes to stream indentation.
* Other miscellaneous stuff.

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 */