1 files changed, 100 insertions, 0 deletions
diff --git a/src/theory/arith/arith_ite_utils.h b/src/theory/arith/arith_ite_utils.h
new file mode 100644
index 000000000..fab0f32cb
--- /dev/null
+++ b/src/theory/arith/arith_ite_utils.h
@@ -0,0 +1,100 @@
+
+
+
+
+
+// Pass 1: label the ite as (constant) or (+ constant variable)
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__ARITH__ARITH_ITE_UTILS_H
+#define __CVC4__THEORY__ARITH__ARITH_ITE_UTILS_H
+
+#include "expr/node.h"
+#include <ext/hash_map>
+#include <ext/hash_set>
+#include "context/cdo.h"
+#include "context/cdtrail_hashmap.h"
+
+namespace CVC4 {
+namespace theory {
+class ContainsTermITEVistor;
+class SubstitutionMap;
+class TheoryModel;
+
+namespace arith {
+
+class ArithIteUtils {
+  ContainsTermITEVistor& d_contains;
+  SubstitutionMap* d_subs;
+  TheoryModel* d_model;
+
+  typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
+  // cache for reduce vars
+  NodeMap d_reduceVar; // if reduceVars[n].isNull(), treat reduceVars[n] == n
+
+  // reduceVars[n] = d_constants[n] + d_varParts[n]
+  NodeMap d_constants; // d_constants[n] is a constant ite tree
+  NodeMap d_varParts; // d_varParts[n] is a polynomial
+
+
+  NodeMap d_reduceGcd;
+  typedef std::hash_map<Node, Integer, NodeHashFunction> NodeIntegerMap;
+  NodeIntegerMap d_gcds;
+
+  Integer d_one;
+
+  context::CDO<unsigned> d_subcount;
+  typedef context::CDTrailHashMap<Node, Node, NodeHashFunction> CDNodeMap;
+  CDNodeMap d_skolems;
+
+  typedef std::map<Node, std::set<Node> > ImpMap;
+  ImpMap d_implies;
+
+  std::vector<Node> d_skolemsAdded;
+
+  std::vector<Node> d_orBinEqs;
+
+public:
+  ArithIteUtils(ContainsTermITEVistor& contains,
+                context::Context* userContext,
+                TheoryModel* model);
+  ~ArithIteUtils();
+
+  //(ite ?v_2 ?v_1 (ite ?v_3 (- ?v_1 128) (- ?v_1 256)))
+
+  /** removes common sums variables sums from term ites. */
+  Node reduceVariablesInItes(Node n);
+
+  Node reduceConstantIteByGCD(Node n);
+
+  void clear();
+
+  Node applySubstitutions(TNode f);
+  unsigned getSubCount() const;
+
+  void learnSubstitutions(const std::vector<Node>& assertions);
+
+private:
+  /* applies this to all children of n and constructs the result */
+  Node applyReduceVariablesInItes(Node n);
+
+  const Integer& gcdIte(Node n);
+  Node reduceIteConstantIteByGCD_rec(Node n, const Rational& q);
+  Node reduceIteConstantIteByGCD(Node n);
+
+  void addSubstitution(TNode f, TNode t);
+  Node selectForCmp(Node n) const;
+
+  void collectAssertions(TNode assertion);
+  void addImplications(Node x, Node y);
+  Node findIteCnd(TNode tb, TNode fb) const;
+  bool solveBinOr(TNode binor);
+
+}; /* class ArithIteUtils */
+
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__ARITH__ARITH_ITE_UTILS_H */