diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-01-05 03:21:35 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-01-05 03:21:35 +0000 |
| commit | f9a4fe48a4ec2355f8fec93d3f47242577df2511 (patch) | |
| tree | eb49b7760b16aa17666d59464c96979b445fbcc8 /src/theory/arith/kinds | |
| parent | eecc1e4f301711dbb2bf1508ea0ba6cd20acd593 (diff) | |
Commit for the theory engine and rewriter changes. Changes are substantial and not yet finalized but I need to put it in to work further with the theory writers. Please check the files that you 'own'. Any comments or discussion is welcome. Further details will be coming in a follow up email later.
Diffstat (limited to 'src/theory/arith/kinds')
| -rw-r--r-- | src/theory/arith/kinds | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index 6808e3d8f..9e2e3a3a7 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -4,7 +4,12 @@ # src/theory/builtin/kinds. # -theory ::CVC4::theory::arith::TheoryArith "theory_arith.h" +theory THEORY_ARITH ::CVC4::theory::arith::TheoryArith "theory/arith/theory_arith.h" + +properties stable-infinite check propagate staticLearning presolve + +rewriter ::CVC4::theory::arith::ArithRewriter "theory/arith/arith_rewriter.h" + operator PLUS 2: "arithmetic addition" operator MULT 2: "arithmetic multiplication" @@ -12,6 +17,9 @@ operator MINUS 2 "arithmetic binary subtraction operator" operator UMINUS 1 "arithmetic unary negation" operator DIVISION 2 "arithmetic division" +sort REAL_TYPE "Real type" +sort INTEGER_TYPE "Integer type" + constant CONST_RATIONAL \ ::CVC4::Rational \ ::CVC4::RationalHashStrategy \ @@ -28,3 +36,5 @@ operator LT 2 "less than, x < y" operator LEQ 2 "less than or equal, x <= y" operator GT 2 "greater than, x > y" operator GEQ 2 "greater than or equal, x >= y" + +endtheory
\ No newline at end of file |