summaryrefslogtreecommitdiff
path: root/src/theory/arith/arith_rewriter.h
diff options
context:
space:
mode:
authorTim King <taking@cs.nyu.edu>2010-04-28 20:14:17 +0000
committerTim King <taking@cs.nyu.edu>2010-04-28 20:14:17 +0000
commitc59fe5b21c218d3d6048cc5c34a7e27b3643ae78 (patch)
treebfd3c1d1eb975989b0ef4afa4e88da4eae84ba62 /src/theory/arith/arith_rewriter.h
parent2482b19ea90183d5040390b87877b7593021032c (diff)
Merging the arithmetic theory draft (lra-init) back into the main trunk. This should not affect other parts of the system. This code is untested, and is volatile. It is going to be improved in the future so don't pick on it too much. I am merging this code in its current state back into the main trunk because it was getting unruly to keep merging the updated trunk back into the branch.
Diffstat (limited to 'src/theory/arith/arith_rewriter.h')
-rw-r--r--src/theory/arith/arith_rewriter.h92
1 files changed, 92 insertions, 0 deletions
diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h
new file mode 100644
index 000000000..844663ce8
--- /dev/null
+++ b/src/theory/arith/arith_rewriter.h
@@ -0,0 +1,92 @@
+
+#include "expr/node.h"
+#include "util/rational.h"
+#include "theory/arith/arith_constants.h"
+
+#ifndef __CVC4__THEORY__ARITH__REWRITER_H
+#define __CVC4__THEORY__ARITH__REWRITER_H
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+
+/***********************************************/
+/***************** Normal Form *****************/
+/***********************************************/
+/***********************************************/
+
+/**
+ * Normal form for predicates:
+ * TRUE
+ * FALSE
+ * v |><| b
+ * p |><| b
+ * (+ p_1 .. p_N) |><| b
+ * where
+ * 1) b is of type CONST_RATIONAL
+ * 2) |><| is of kind <, <=, =, >= or >
+ * 3) p, p_i is in PNF,
+ * 4) p.M >= 2
+ * 5) p_i's are in strictly ascending <p,
+ * 6) N >= 2,
+ * 7) the kind of (+ p_1 .. p_N) is an N arity PLUS,
+ * 8) p.d, p_1.d are 1,
+ * 9) v has metakind variable, and
+ *
+ * PNF(t):
+ * (* d v_1 v_2 ... v_M)
+ * where
+ * 1) d is of type CONST_RATIONAL,
+ * 2) d != 0,
+ * 4) M>=1,
+ * 5) v_i are of metakind VARIABLE,
+ * 6) v_i are in increasing (not strict) nodeOrder, and
+ * 7) the kind of t is an M+1 arity MULT.
+ *
+ * <p is defined over PNF as follows (skipping some symmetry):
+ * cmp( (* d v_1 v_2 ... v_M), (* d' v'_1 v'_2 ... v'_M'):
+ * if(M == M'):
+ * then tupleCompare(v_i, v'_i)
+ * else M -M'
+ *
+ * Rewrite Normal Form for Terms:
+ * b
+ * v
+ * (+ c p_1 p_2 ... p_N) | not(N=1 and c=0 and p_1.d=1)
+ * where
+ * 1) b,c is of type CONST_RATIONAL,
+ * 3) p_i is in PNF,
+ * 4) N >= 1
+ * 5) the kind of (+ c p_1 p_2 ... p_N) is an N+1 arity PLUS,
+ * 6) and p_i's are in strictly <p.
+ *
+ */
+
+class ArithRewriter{
+private:
+ ArithConstants* d_constants;
+
+ Node rewriteAtom(TNode atom);
+ Node rewriteTerm(TNode t);
+ Node rewriteMult(TNode t);
+ Node rewritePlus(TNode t);
+ Node makeSubtractionNode(TNode l, TNode r);
+
+
+ Node var2pnf(TNode variable);
+
+public:
+ ArithRewriter(ArithConstants* ac) :
+ d_constants(ac)
+ {}
+ Node rewrite(TNode t);
+
+};
+
+
+}; /* namesapce arith */
+}; /* namespace theory */
+}; /* namespace CVC4 */
+
+#endif /* __CVC4__THEORY__ARITH__REWRITER_H */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback