This commit contains the code for allowing arbitrary equalities in the theory of arithmetic.

* This code has been partially tested. (My testing situation is currently not so great.)  The code for testing not preregistering equalities can be compile time enabled by setting the boolean turnOffEqualityPreRegister. Don't be shocked by slowdowns or failures.  This does pass make regress as well as a fresh checkout does. (The Mac version has issues.)
* I need to disable the permanent row removal heuristic by default.  We need to discuss why this needs to happen.  We should probably detect pure QF_LRA/QF_RDL problems and enable this when this can safely be done.
* I have disabled the arithmetic rewrite equality flag.  This code needs to be added to the parser. 
* For all of the above changes, I have annotated the code with the key word BREADCRUMB.
* I have renamed ArithUnatePropagator to ArithAtomDatabase.

1 files changed, 166 insertions, 0 deletions

diff --git a/src/theory/arith/atom_database.h b/src/theory/arith/atom_database.h
new file mode 100644
index 000000000..25020977a
--- /dev/null
+++ b/src/theory/arith/atom_database.h
@@ -0,0 +1,166 @@
+/*********************                                                        */
+/*! \file atom_database.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  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 ArithAtomDatabase keeps a database of the arithmetic atoms.
+ ** Importantly, ArithAtomDatabase also handles unate propagations,
+ ** i.e. it constructs implications of the form
+ ** "if x < c and c < b, then x < b" (where c and b are constants).
+ **
+ ** ArithAtomDatabase detects unate implications amongst the atoms
+ ** associated with the theory of arithmetic and informs the SAT solver of the
+ ** implication. A unate implication is an implication of the form:
+ **   "if x < c and c < b, then x < b" (where c and b are constants).
+ ** Unate implications are always 2-SAT clauses.
+ ** ArithAtomDatabase sends the implications to the SAT solver in an
+ ** online fashion.
+ ** This means that atoms may be added during solving or before.
+ **
+ ** ArithAtomDatabase maintains sorted lists containing all atoms associated
+ ** for each unique left hand side, the "x" in the inequality "x < c".
+ ** The lists are sorted by the value of the right hand side which must be a
+ ** rational constant.
+ **
+ ** ArithAtomDatabase tries to send out a minimal number of additional
+ ** lemmas per atom added.  Let (x < a), (x < b), (x < c) be arithmetic atoms s.t.
+ ** a < b < c.
+ ** If the the order of adding the atoms is (x < a), (x < b), and (x < c), then
+ ** then set of all lemmas added is:
+ **   {(=> (x<a) (x < b)), (=> (x<b) (x < c))}
+ ** If the order is changed to (x < a), (x < c), and (x < b), then
+ ** the final set of implications emitted is:
+ **   {(=> (x<a) (x < c)), (=> (x<a) (x < b)), (=> (x<b) (x < c))}
+ **
+ ** \todo document this file
+ **/
+
+
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__ARITH__ARITH_ATOM_DATABASE_H
+#define __CVC4__THEORY__ARITH__ARITH_ATOM_DATABASE_H
+
+#include "expr/node.h"
+#include "context/context.h"
+
+#include "theory/output_channel.h"
+#include "theory/arith/ordered_set.h"
+
+#include <ext/hash_map>
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+class ArithAtomDatabase {
+private:
+  /**
+   * OutputChannel for the theory of arithmetic.
+   * The propagator uses this to pass implications back to the SAT solver.
+   */
+  OutputChannel& d_arithOut;
+
+  struct VariablesSets {
+    BoundValueSet d_boundValueSet;
+    EqualValueSet d_eqValueSet;
+  };
+
+  typedef __gnu_cxx::hash_map<TNode, VariablesSets, NodeHashFunction> NodeToSetsMap;
+  NodeToSetsMap d_setsMap;
+
+public:
+  ArithAtomDatabase(context::Context* cxt, OutputChannel& arith);
+
+  /**
+   * Adds an atom to the propagator.
+   * Any resulting lemmas will be output via d_arithOut.
+   */
+  void addAtom(TNode atom);
+
+  /** Returns true if v has been added as a left hand side in an atom */
+  bool hasAnyAtoms(TNode v) const;
+
+  bool containsLiteral(TNode lit) const;
+  bool containsAtom(TNode atom) const;
+  bool containsEquality(TNode atom) const;
+  bool containsLeq(TNode atom) const;
+  bool containsGeq(TNode atom) const;
+
+
+
+private:
+  VariablesSets& getVariablesSets(TNode left);
+  BoundValueSet& getBoundValueSet(TNode left);
+  EqualValueSet& getEqualValueSet(TNode left);
+
+  const VariablesSets& getVariablesSets(TNode left) const;
+  const BoundValueSet& getBoundValueSet(TNode left) const;
+  const EqualValueSet& getEqualValueSet(TNode left) const;
+
+  /** Sends an implication (=> a b) to the PropEngine via d_arithOut. */
+  void addImplication(TNode a, TNode b);
+
+  /** Check to make sure an lhs has been properly set-up. */
+  bool leftIsSetup(TNode left) const;
+
+  /** Initializes the lists associated with a unique lhs. */
+  void setupLefthand(TNode left);
+
+
+  /**
+   * The addImplicationsUsingKAndJList(...)
+   * functions are the work horses of the unate part of ArithAtomDatabase.
+   * These take an atom of the kind K that has just been added
+   * to its associated list, and the ordered list of Js associated with the lhs,
+   * and uses these to deduce unate implications.
+   * (K and J vary over EQUAL, LEQ, and GEQ.)
+   *
+   * Input:
+   * atom - the atom being inserted of kind K
+   * Jset - the list of atoms of kind J associated with the lhs.
+   *
+   * Unfortunately, these tend to be an absolute bear to read because
+   * of all of the special casing and C++ iterator manipulation required.
+   */
+
+  void addImplicationsUsingEqualityAndEqualityValues(TNode eq);
+  void addImplicationsUsingEqualityAndBoundValues(TNode eq);
+
+  void addImplicationsUsingLeqAndEqualityValues(TNode leq);
+  void addImplicationsUsingLeqAndBoundValues(TNode leq);
+
+  void addImplicationsUsingGeqAndEqualityValues(TNode geq);
+  void addImplicationsUsingGeqAndBoundValues(TNode geq);
+
+  bool hasBoundValueEntry(TNode n);
+
+  Node getImpliedUpperBoundUsingLeq(TNode leq, bool weaker) const;
+  Node getImpliedUpperBoundUsingLT(TNode lt, bool weaker) const;
+
+  Node getImpliedLowerBoundUsingGeq(TNode geq, bool weaker) const;
+  Node getImpliedLowerBoundUsingGT(TNode gt, bool weaker) const;
+
+public:
+  Node getBestImpliedUpperBound(TNode upperBound) const;
+  Node getBestImpliedLowerBound(TNode lowerBound) const;
+
+
+  Node getWeakerImpliedUpperBound(TNode upperBound) const;
+  Node getWeakerImpliedLowerBound(TNode lowerBound) const;
+};
+
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__ARITH__ARITH_ATOM_DATABASE_H */