Merges branches/arithmetic/atom-database r2979 through 3247 into trunk. Below is a highlight of the changes:

- This introduces a new normal form to arithmetic.
-- Equalities and disequalities are in solved form.
   Roughly speaking this means: (= x (+ y z)) is in normal form.
   (See the comments in normal_form.h for what this formally requires.)
-- The normal form for inequality atoms always uses GEQ and GT instead of GEQ and LEQ.
   Integer atoms always use GEQ.
- Constraint was added to TheoryArith.
-- A constraint is a triple of (k x v) where:
--- k is the type of the constraint (either LowerBound, UpperBound, Equality or Disequality),
--- x is an ArithVar, and
--- v is a DeltaRational value.
-- Constraints are always attached to a ConstraintDatabase.
-- A Constraint has its negation in the ConstraintDatabase [at least for now].
-- Every constraint belongs to a set of constraints for each ArithVar sorted by the delta rational values.
-- This set can be iterated over and provides efficient access to other constraints for this variable.
-- A literal may be attached to a constraint.
-- Constraints with attached literals may be marked as being asserted to the theory (sat context dependent).
-- Constraints can be propagated.
-- Every constraint has a proof (sat context dependent).
-- Proofs can be explained for either conflicts or propagations (if the node was propagated). (These proofs may be different.)
-- Equalities and disequalities can be marked as being split (user context dependent)
- This removes and replaces:
-- src/theory/arith/arith_prop_manager.*
-- src/theory/arith/atom_database.*
-- src/theory/arith/ordered_set.h
- Added isZero(), isOne() and isNegativeOne() to Rational and Integer.
- Added operator+ to CDList::const_iterator.
- Added const_iterator to CDQueue.
- Changes to regression tests.

1 files changed, 837 insertions, 0 deletions

diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
new file mode 100644
index 000000000..e1939159b
--- /dev/null
+++ b/src/theory/arith/constraint.h
@@ -0,0 +1,837 @@
+/*********************                                                        */
+/*! \file constraint.h
+ ** \verbatim
+ ** Original author: taking
+ ** 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 Defines Constraint and ConstraintDatabase which is the internal representation of variables in arithmetic
+ **
+ ** This file defines Constraint and ConstraintDatabase.
+ ** A Constraint is the internal representation of literals in TheoryArithmetic.
+ ** Constraints are fundamentally a triple:
+ **  - ArithVar associated with the constraint,
+ **  - a DeltaRational value,
+ **  - and a ConstraintType.
+ **
+ ** Literals:
+ **   The constraint may also keep track of a node corresponding to the
+ **   Constraint.
+ **   This can be accessed by getLiteral() in O(1) if it has been set.
+ **   This node must be in normal form and may be used for communication with
+ **   the TheoryEngine.
+ **
+ ** In addition, Constraints keep track of the following:
+ **  - A Constrain that is the negation of the Constraint.
+ **  - An iterator into a set of Constraints for the ArithVar sorted by
+ **    DeltaRational value.
+ **  - A context dependent internal proof of the node that can be used for
+ **    explanations.
+ **  - Whether an equality/disequality has been split in the user context via a
+ **    lemma.
+ **  - Whether a constraint, be be used in explanations sent to the context
+ **
+ ** Looking up constraints:
+ **  - All of the Constraints with associated nodes in the ConstraintDatabase can
+ **    be accessed via a single hashtable lookup until the Constraint is removed.
+ **  - Nodes that have not been associated to a constraints can be
+ **    inserted/associated to existing nodes in O(log n) time.
+ **
+ ** Implications:
+ **  - A Constraint can be used to find unate implications.
+ **  - A unate implication is an implication based purely on the ArithVar matching
+ **    and the DeltaRational value.
+ **    (implies (<= x c) (<= x d)) given c <= d
+ **  - This is done using the iterator into the sorted set of constraints.
+ **  - Given a tight constraint and previous tightest constraint, this will
+ **    efficiently propagate internally.
+ **
+ ** Additing and Removing Constraints
+ **  - Adding Constraints takes O(log n) time where n is the number of
+ **    constraints associated with the ArithVar.
+ **  - Removing Constraints takes O(1) time.
+ **
+ ** Internals:
+ **  - Constraints are pointers to ConstraintValues.
+ **  - Undefined Constraints are NullConstraint.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__ARITH__CONSTRAINT_H
+#define __CVC4__THEORY__ARITH__CONSTRAINT_H
+
+#include "expr/node.h"
+
+#include "context/context.h"
+#include "context/cdlist.h"
+#include "context/cdqueue.h"
+
+#include "theory/arith/arithvar.h"
+#include "theory/arith/arithvar_node_map.h"
+#include "theory/arith/delta_rational.h"
+
+#include "theory/arith/difference_manager.h"
+
+#include "theory/arith/constraint_forward.h"
+
+#include <vector>
+#include <list>
+#include <set>
+#include <ext/hash_map>
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+/**
+ * The types of constraints.
+ * The convex constraints are the constraints are LowerBound, Equality,
+ * and UpperBound.
+ */
+enum ConstraintType {LowerBound, Equality, UpperBound, Disequality};
+
+
+typedef context::CDList<Constraint> CDConstraintList;
+
+typedef __gnu_cxx::hash_map<Node, Constraint, NodeHashFunction> NodetoConstraintMap;
+
+typedef size_t ProofId;
+static ProofId ProofIdSentinel = std::numeric_limits<ProofId>::max();
+
+typedef size_t AssertionOrder;
+static AssertionOrder AssertionOrderSentinel = std::numeric_limits<AssertionOrder>::max();
+
+/**
+ * A ValueCollection binds together convex constraints that have the same
+ * DeltaRational value.
+ */
+class ValueCollection {
+private:
+
+  Constraint d_lowerBound;
+  Constraint d_upperBound;
+  Constraint d_equality;
+  Constraint d_disequality;
+
+public:
+  ValueCollection()
+    : d_lowerBound(NullConstraint),
+      d_upperBound(NullConstraint),
+      d_equality(NullConstraint),
+      d_disequality(NullConstraint)
+  {}
+
+  static ValueCollection mkFromConstraint(Constraint c);
+
+  bool hasLowerBound() const{
+    return d_lowerBound != NullConstraint;
+  }
+  bool hasUpperBound() const{
+    return d_upperBound != NullConstraint;
+  }
+  bool hasEquality() const{
+    return d_equality != NullConstraint;
+  }
+  bool hasDisequality() const {
+    return d_disequality != NullConstraint;
+  }
+
+  bool hasConstraintOfType(ConstraintType t) const;
+
+  Constraint getLowerBound() const {
+    Assert(hasLowerBound());
+    return d_lowerBound;
+  }
+  Constraint getUpperBound() const {
+    Assert(hasUpperBound());
+    return d_upperBound;
+  }
+  Constraint getEquality() const {
+    Assert(hasEquality());
+    return d_equality;
+  }
+  Constraint getDisequality() const {
+    Assert(hasDisequality());
+    return d_disequality;
+  }
+
+  Constraint getConstraintOfType(ConstraintType t) const;
+
+  /** Returns true if any of the constraints are non-null. */
+  bool empty() const;
+
+  /**
+   * Remove the constraint of the type t from the collection.
+   * Returns true if the ValueCollection is now empty.
+   * If true is returned, d_value is now NULL.
+   */
+  void remove(ConstraintType t);
+
+  /**
+   * Adds a constraint to the set.
+   * The collection must not have a constraint of that type already.
+   */
+  void add(Constraint c);
+
+  void push_into(std::vector<Constraint>& vec) const;
+
+  Constraint nonNull() const;
+
+  ArithVar getVariable() const;
+  const DeltaRational& getValue() const;
+};
+
+/**
+ * A Map of ValueCollections sorted by the associated DeltaRational values.
+ *
+ * Discussion:
+ * While it is more natural to consider this a set, this cannot be a set as in
+ * sets the type of both iterator and const_iterator in sets are
+ * "constant iterators".  We require iterators that dereference to
+ * ValueCollection&.
+ *
+ * See:
+ * http://gcc.gnu.org/onlinedocs/libstdc++/ext/lwg-defects.html#103
+ */
+typedef std::map<DeltaRational, ValueCollection> SortedConstraintMap;
+typedef SortedConstraintMap::iterator SortedConstraintMapIterator;
+typedef SortedConstraintMap::const_iterator SortedConstraintMapConstIterator;
+
+/** A Pair associating a variables and a Sorted ConstraintSet. */
+struct PerVariableDatabase{
+  ArithVar d_var;
+  SortedConstraintMap d_constraints;
+
+  // x ? c_1, x ? c_2, x ? c_3, ...
+  // where ? is a non-empty subset of {lb, ub, eq}
+  // c_1 < c_2 < c_3 < ...
+
+  PerVariableDatabase(ArithVar v) : d_var(v), d_constraints() {}
+
+  bool empty() const {
+    return d_constraints.empty();
+  }
+
+  static bool IsEmpty(const PerVariableDatabase& p){
+    return p.empty();
+  }
+};
+
+class ConstraintValue {
+private:
+  /** The ArithVar associated with the constraint. */
+  const ArithVar d_variable;
+
+  /** The type of the Constraint. */
+  const ConstraintType d_type;
+
+  /** The DeltaRational value with the constraint. */
+  const DeltaRational d_value;
+
+  /** A pointer to the associated database for the Constraint. */
+  ConstraintDatabase * d_database;
+
+  /**
+   * The node to be communicated with the TheoryEngine.
+   *
+   * This is not context dependent, but may be set once.
+   *
+   * This must be set if the constraint canbePropgated().
+   * This must be set if the constraint assertedToTheTheory().
+   * Otherwise, this may be null().
+   */
+  Node d_literal;
+
+  /** Pointer to the negation of the Constraint. */
+  Constraint d_negation;
+
+  /**
+   * This is true if the associated node can be propagated.
+   *
+   * This should be enabled if the node has been preregistered.
+   *
+   * Sat Context Dependent.
+   * This is initially false.
+   */
+  bool d_canBePropagated;
+
+  /**
+   * This is the order the constraint was asserted to the theory.
+   * If this has been set, the node can be used in conflicts.
+   * If this is c.d_assertedOrder < d.d_assertedOrder, then c can be used in the
+   * explanation of d.
+   *
+   * This should be set after the literal is dequeued by Theory::get().
+   *
+   * Sat Context Dependent.
+   * This is initially AssertionOrderSentinel.
+   */
+  AssertionOrder d_assertionOrder;
+
+  /**
+   * This points at the proof for the constraint in the current context.
+   *
+   * Sat Context Dependent.
+   * This is initially ProofIdSentinel.
+   */
+  ProofId d_proof;
+
+  /**
+   * True if the equality has been split.
+   * Only meaningful if ContraintType == Equality.
+   *
+   * User Context Dependent.
+   * This is initially false.
+   */
+  bool d_split;
+
+  /**
+   * Position in sorted constraint set for the variable.
+   * Unset if d_type is Disequality.
+   */
+  SortedConstraintMapIterator d_variablePosition;
+
+  friend class ConstraintDatabase;
+
+  /**
+   * This begins construction of a minimal constraint.
+   *
+   * This should only be called by ConstraintDatabase.
+   *
+   * Because of circular dependencies a Constraint is not fully valid until
+   * initialize has been called on it.
+   */
+  ConstraintValue(ArithVar x,  ConstraintType t, const DeltaRational& v);
+
+  /**
+   * Destructor for a constraint.
+   * This should only be called if safeToGarbageCollect() is true.
+   */
+  ~ConstraintValue();
+
+  bool initialized() const;
+
+  /**
+   * This initializes the fields that cannot be set in the constructor due to
+   * circular dependencies.
+   */
+  void initialize(ConstraintDatabase* db, SortedConstraintMapIterator v, Constraint negation);
+
+  class ProofCleanup {
+  public:
+    inline void operator()(Constraint* p){
+      Constraint constraint = *p;
+      Assert(constraint->d_proof != ProofIdSentinel);
+      constraint->d_proof = ProofIdSentinel;
+    }
+  };
+
+  class CanBePropagatedCleanup {
+  public:
+    inline void operator()(Constraint* p){
+      Constraint constraint = *p;
+      Assert(constraint->d_canBePropagated);
+      constraint->d_canBePropagated = false;
+    }
+  };
+
+  class AssertionOrderCleanup {
+  public:
+    inline void operator()(Constraint* p){
+      Constraint constraint = *p;
+      Assert(constraint->assertedToTheTheory());
+      constraint->d_assertionOrder = AssertionOrderSentinel;
+      Assert(!constraint->assertedToTheTheory());
+    }
+  };
+
+  class SplitCleanup {
+  public:
+    inline void operator()(Constraint* p){
+      Constraint constraint = *p;
+      Assert(constraint->d_split);
+      constraint->d_split = false;
+    }
+  };
+
+  /** Returns true if the node is safe to garbage collect. */
+  bool safeToGarbageCollect() const;
+
+  /**
+   * Returns true if the node correctly corresponds to the constraint that is
+   * being set.
+   */
+  bool sanityChecking(Node n) const;
+
+  /** Returns a reference to the map for d_variable. */
+  SortedConstraintMap& constraintSet() const;
+
+public:
+
+  ConstraintType getType() const {
+    return d_type;
+  }
+
+  ArithVar getVariable() const {
+    return d_variable;
+  }
+
+  const DeltaRational& getValue() const {
+    return d_value;
+  }
+
+  Constraint getNegation() const {
+    return d_negation;
+  }
+
+  bool isEquality() const{
+    return d_type == Equality;
+  }
+  bool isDisequality() const{
+    return d_type == Disequality;
+  }
+  bool isLowerBound() const{
+    return d_type == LowerBound;
+  }
+  bool isUpperBound() const{
+    return d_type == UpperBound;
+  }
+
+  bool isSplit() const {
+    return d_split;
+  }
+
+  /**
+   * Splits the node in the user context.
+   * Returns a lemma that is assumed to be true fro the rest of the user context.
+   * Constraint must be an equality or disequality.
+   */
+  Node split();
+
+  bool canBePropagated() const {
+    return d_canBePropagated;
+  }
+  void setCanBePropagated();
+
+  /**
+   * Light wrapper for calling setCanBePropagated(),
+   * on this and this-d_negation.
+   */
+  void setPreregistered(){
+    setCanBePropagated();
+    d_negation->setCanBePropagated();
+  }
+
+  bool assertedToTheTheory() const {
+    return d_assertionOrder < AssertionOrderSentinel;
+  }
+
+  bool assertedBefore(AssertionOrder time) const {
+    return d_assertionOrder < time;
+  }
+
+
+  void setAssertedToTheTheory();
+
+
+  bool hasLiteral() const {
+    return !d_literal.isNull();
+  }
+
+  void setLiteral(Node n);
+
+  Node getLiteral() const {
+    Assert(hasLiteral());
+    return d_literal;
+  }
+
+  /**
+   * Set the node as selfExplaining().
+   * The node must be assertedToTheTheory().
+   */
+  void selfExplaining();
+
+  /** Returns true if the node is selfExplaining.*/
+  bool isSelfExplaining() const;
+
+  /**
+   * Set the constraint to be a EqualityEngine proof.
+   */
+  void setEqualityEngineProof();
+  bool hasEqualityEngineProof() const;
+
+  /**
+   * Returns a explanation of the constraint that is appropriate for conflicts.
+   *
+   * This is not appropraite for propagation!
+   *
+   * This is the minimum fringe of the implication tree s.t.
+   * every constraint is assertedToTheTheory() or hasEqualityEngineProof().
+   */
+  Node explainForConflict() const{
+    return explainBefore(AssertionOrderSentinel);
+  }
+
+  /**
+   * Writes an explanation of a constraint into the node builder.
+   * Pushes back an explanation that is acceptable to send to the sat solver.
+   * nb is assumed to be an AND.
+   *
+   * This is the minimum fringe of the implication tree s.t.
+   * every constraint is assertedToTheTheory() or hasEqualityEngineProof().
+   *
+   * This is not appropraite for propagation!
+   * Use explainForPropagation() instead.
+   */
+  void explainForConflict(NodeBuilder<>& nb) const{
+    explainBefore(nb, AssertionOrderSentinel);
+  }
+
+  /** Utility function built from explainForConflict. */
+  static Node explainConflict(Constraint a, Constraint b);
+  static Node explainConflict(Constraint a, Constraint b, Constraint c);
+
+  /**
+   * Returns an explanation of a propagation by the ConstraintDatabase.
+   * The constraint must have a proof.
+   * The constraint cannot be selfExplaining().
+   *
+   * This is the minimum fringe of the implication tree (excluding the constraint itself)
+   * s.t. every constraint is assertedToTheTheory() or hasEqualityEngineProof().
+   */
+  Node explainForPropagation() const {
+    Assert(hasProof());
+    Assert(!isSelfExplaining());
+    return explainBefore(d_assertionOrder);
+  }
+
+private:
+  Node explainBefore(AssertionOrder order) const;
+
+  /**
+   * Returns an explanation of that was assertedBefore(order).
+   * The constraint must have a proof.
+   * The constraint cannot be selfExplaining().
+   *
+   * This is the minimum fringe of the implication tree
+   * s.t. every constraint is assertedBefore(order) or hasEqualityEngineProof().
+   */
+  void explainBefore(NodeBuilder<>& nb, AssertionOrder order) const;
+
+public:
+  bool hasProof() const {
+    return d_proof != ProofIdSentinel;
+  }
+  bool negationHasProof() const {
+    return d_negation->hasProof();
+  }
+
+  bool truthIsUnknown() const {
+    return !hasProof() && !negationHasProof();
+  }
+
+  bool isTrue() const {
+    return hasProof();
+  }
+
+  Constraint getCeiling();
+
+  Constraint getFloor();
+
+
+  static Constraint makeNegation(ArithVar v, ConstraintType t, const DeltaRational& r);
+
+  const ValueCollection& getValueCollection() const;
+
+
+  Constraint getStrictlyWeakerUpperBound(bool hasLiteral, bool mustBeAsserted) const;
+  Constraint getStrictlyWeakerLowerBound(bool hasLiteral, bool mustBeAsserted) const;
+
+  /**
+   * Marks the node as having a proof a.
+   * Adds the node the database's propagation queue.
+   *
+   * Preconditions:
+   * canBePropagated()
+   * !assertedToTheTheory()
+   */
+  void propagate(Constraint a);
+  void propagate(Constraint a, Constraint b);
+  void propagate(const std::vector<Constraint>& b);
+  /**
+   * The only restriction is that this is not known be true.
+   * This propgates if there is a node.
+   */
+  void impliedBy(Constraint a);
+  void impliedBy(Constraint a, Constraint b);
+  void impliedBy(const std::vector<Constraint>& b);
+
+
+  /** The node must have a proof already and be eligible for propagation! */
+  void propagate();
+
+private:
+  /**
+   * Marks the node as having a proof and being selfExplaining.
+   * Neither the node nor its negation can have a proof.
+   * This is internal!
+   */
+  void markAsTrue();
+  /**
+   * Marks the node as having a proof a.
+   * This is safe if the node does not have
+   */
+  void markAsTrue(Constraint a);
+
+  void markAsTrue(Constraint a, Constraint b);
+  void markAsTrue(const std::vector<Constraint>& b);
+
+public:
+
+
+private:
+
+  void debugPrint() const;
+
+  /**
+   * The proof of the node is empty.
+   * The proof must be a special proof. Either
+   *   isSelfExplaining() or
+   *    hasEqualityEngineProof()
+   */
+  bool proofIsEmpty() const;
+
+}; /* class ConstraintValue */
+
+std::ostream& operator<<(std::ostream& o, const ConstraintValue& c);
+std::ostream& operator<<(std::ostream& o, const Constraint c);
+std::ostream& operator<<(std::ostream& o, const ConstraintType t);
+std::ostream& operator<<(std::ostream& o, const ValueCollection& c);
+
+
+
+class ConstraintDatabase {
+private:
+  /**
+   * The map from ArithVars to their unique databases.
+   * When the vector changes size, we cannot allow the maps to move so this
+   * is a vector of pointers.
+   */
+  std::vector<PerVariableDatabase*> d_varDatabases;
+
+  SortedConstraintMap& getVariableSCM(ArithVar v) const{
+    Assert(variableDatabaseIsSetup(v));
+    return d_varDatabases[v]->d_constraints;
+  }
+
+  /** Maps literals to constraints.*/
+  NodetoConstraintMap d_nodetoConstraintMap;
+
+  /**
+   * A queue of propagated constraints.
+   *
+   * As Constraint are pointers, the elements of the queue do not require destruction.
+   */
+  context::CDQueue<Constraint> d_toPropagate;
+
+  /**
+   * Proof Lists.
+   * Proofs are lists of valid constraints terminated by the first smaller
+   * sentinel value in the proof list.
+   * The proof at p in d_proofs[p] of length n is
+   *  (NullConstraint, d_proofs[p-(n-1)], ... , d_proofs[p-1], d_proofs[p])
+   * The proof at p corresponds to the conjunction:
+   *  (and x_i)
+   *
+   * So the proof of a Constraint c corresponds to the horn clause:
+   *  (implies (and x_i) c)
+   * where (and x_i) is the proof at c.d_proofs.
+   *
+   * Constraints are pointers so this list is designed not to require any
+   * destruction.
+   */
+  CDConstraintList d_proofs;
+
+  /**
+   * This is a special proof for marking that nodes are their own explanation
+   * from the perspective of the theory.
+   * These must always be asserted to the theory.
+   *
+   * This proof is always a member of the list.
+   */
+  ProofId d_selfExplainingProof;
+
+  /**
+   * Marks a node as being proved by the equality engine.
+   * The equality engine will be asked for the explanation of such nodes.
+   *
+   * This is a special proof that is always a member of the list.
+   */
+  ProofId d_equalityEngineProof;
+
+  typedef context::CDList<Constraint, ConstraintValue::ProofCleanup> ProofCleanupList;
+  typedef context::CDList<Constraint, ConstraintValue::CanBePropagatedCleanup> CBPList;
+  typedef context::CDList<Constraint, ConstraintValue::AssertionOrderCleanup> AOList;
+  typedef context::CDList<Constraint, ConstraintValue::SplitCleanup> SplitList;
+
+  /**
+   * The watch lists are collected together as they need to be garbage collected
+   * carefully.
+   */
+  struct Watches{
+    /**
+     * Contains the exact list of atoms that have a proof.
+     */
+    ProofCleanupList d_proofWatches;
+
+    /**
+     * Contains the exact list of constraints that can be used for propagation.
+     */
+    CBPList d_canBePropagatedWatches;
+
+    /**
+     * Contains the exact list of constraints that have been asserted to the theory.
+     */
+    AOList d_assertionOrderWatches;
+
+
+    /**
+     * Contains the exact list of atoms that have been preregistered.
+     * This is a pointer as it must be destroyed before the elements of
+     * d_varDatabases.
+     */
+    SplitList d_splitWatches;
+    Watches(context::Context* satContext, context::Context* userContext);
+  };
+  Watches* d_watches;
+
+  void pushSplitWatch(Constraint c){
+    Assert(!c->d_split);
+    c->d_split = true;
+    d_watches->d_splitWatches.push_back(c);
+  }
+
+  void pushCanBePropagatedWatch(Constraint c){
+    Assert(!c->d_canBePropagated);
+    c->d_canBePropagated = true;
+    d_watches->d_canBePropagatedWatches.push_back(c);
+  }
+
+  void pushAssertionOrderWatch(Constraint c){
+    Assert(!c->assertedToTheTheory());
+    c->d_assertionOrder = d_watches->d_assertionOrderWatches.size();
+    d_watches->d_assertionOrderWatches.push_back(c);
+  }
+
+  void pushProofWatch(Constraint c, ProofId pid){
+    Assert(c->d_proof == ProofIdSentinel);
+    c->d_proof = pid;
+    d_watches->d_proofWatches.push_back(c);
+  }
+
+  /** Returns true if all of the entries of the vector are empty. */
+  static bool emptyDatabase(const std::vector<PerVariableDatabase>& vec);
+
+  /** Map from nodes to arithvars. */
+  const ArithVarNodeMap& d_av2nodeMap;
+
+  const ArithVarNodeMap& getArithVarNodeMap() const{
+    return d_av2nodeMap;
+  }
+
+  DifferenceManager& d_differenceManager;
+
+  //Constraint allocateConstraintForLiteral(ArithVar v, Node literal);
+
+  const context::Context * const d_satContext;
+  const int d_satAllocationLevel;
+
+  friend class ConstraintValue;
+
+public:
+
+  ConstraintDatabase( context::Context* satContext,
+                      context::Context* userContext,
+                      const ArithVarNodeMap& av2nodeMap,
+                      DifferenceManager& dm);
+
+  ~ConstraintDatabase();
+
+  Constraint addLiteral(TNode lit);
+  //Constraint addAtom(TNode atom);
+
+  /**
+   * If hasLiteral() is true, returns the constraint.
+   * Otherwise, returns NullConstraint.
+   */
+  Constraint lookup(TNode literal) const;
+
+  /**
+   * Returns true if the literal has been added to the database.
+   * This is a hash table lookup.
+   * It does not look in the database for an equivalent corresponding constraint.
+   */
+  bool hasLiteral(TNode literal) const;
+
+  bool hasMorePropagations() const{
+    return !d_toPropagate.empty();
+  }
+
+  Constraint nextPropagation(){
+    Assert(hasMorePropagations());
+
+    Constraint p = d_toPropagate.front();
+    d_toPropagate.pop();
+
+    return p;
+  }
+
+  void addVariable(ArithVar v);
+  bool variableDatabaseIsSetup(ArithVar v) const;
+
+  Node eeExplain(ConstConstraint c) const;
+  void eeExplain(ConstConstraint c, NodeBuilder<>& nb) const;
+
+  /**
+   * Returns a constraint with the variable v, the constraint type t, and a value
+   * dominated by r (explained below) if such a constraint exists in the database.
+   * If no such constraint exists, NullConstraint is returned.
+   *
+   * t must be either UpperBound or LowerBound.
+   * The returned value v is dominatated:
+   *  If t is UpperBound, r <= v
+   *  If t is LowerBound, r >= v
+   */
+  Constraint getBestImpliedBound(ArithVar v, ConstraintType t, const DeltaRational& r) const;
+
+  /**
+   * Returns a constraint with the variable v, the constraint type t and the value r.
+   * If there is such a constraint in the database already, it is returned.
+   * If there is no such constraint, this constraint is added to the database.
+   *
+   */
+  Constraint getConstraint(ArithVar v, ConstraintType t, const DeltaRational& r);
+
+
+  /**
+   * Outputs a minimal set of unate implications on the output channel
+   * for all variables.
+   */
+  void outputAllUnateLemmas(std::vector<Node>& lemmas) const;
+
+  void outputAllUnateLemmas(std::vector<Node>& lemmas, ArithVar v) const;
+
+}; /* ConstraintDatabase */
+
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__ARITH__CONSTRAINT_H */