diff options
author | Tim King <taking@cs.nyu.edu> | 2010-04-28 20:14:17 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-04-28 20:14:17 +0000 |
commit | c59fe5b21c218d3d6048cc5c34a7e27b3643ae78 (patch) | |
tree | bfd3c1d1eb975989b0ef4afa4e88da4eae84ba62 /src/theory/arith/arith_rewriter.h | |
parent | 2482b19ea90183d5040390b87877b7593021032c (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.h | 92 |
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 */ |