diff options
| author | Tim King <taking@cs.nyu.edu> | 2010-04-28 14:52:22 +0000 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2010-04-28 14:52:22 +0000 |
| commit | 7a8454030fdbb1e6c2a6db7ce18eafe0764eaf4a (patch) | |
| tree | 1c2044783b304516f67a1355bf16b0af7ec42a06 /src/theory | |
| parent | 0c4a6edae95b3ffc76cb82604a3d1694d42625bb (diff) | |
Added theory/arith/kind and enabled the smt parser to read in these symbols. Also a bug fix to a couple of unit tests.
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/arith/kinds | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index 3b79192d2..fafa33a68 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -8,7 +8,8 @@ theory ::CVC4::theory::arith::TheoryArith "theory_arith.h" operator PLUS 2: "arithmetic addition" operator MULT 2: "arithmetic multiplication" -operator UMINUS 1 "arithmetic negation" +operator MINUS 2 "arithmetic binary subtraction operator" +operator UMINUS 1 "arithmetic unary negation" constant CONST_RATIONAL \ ::CVC4::Rational \ @@ -21,3 +22,8 @@ constant CONST_INTEGER \ ::CVC4::IntegerHashStrategy \ "util/integer.h" \ "a multiple-precision integer constant" + +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" |