diff options
Diffstat (limited to 'src/theory/arith/kinds')
| -rw-r--r-- | src/theory/arith/kinds | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index 9e2e3a3a7..a0fc71ab4 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -6,7 +6,8 @@ theory THEORY_ARITH ::CVC4::theory::arith::TheoryArith "theory/arith/theory_arith.h" -properties stable-infinite check propagate staticLearning presolve +properties stable-infinite +properties check propagate staticLearning presolve notifyRestart rewriter ::CVC4::theory::arith::ArithRewriter "theory/arith/arith_rewriter.h" @@ -17,8 +18,8 @@ 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" +sort REAL_TYPE Cardinality::REALS "Real type" +sort INTEGER_TYPE Cardinality::INTEGERS "Integer type" constant CONST_RATIONAL \ ::CVC4::Rational \ @@ -37,4 +38,4 @@ 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 +endtheory |