Added theory/arith/kind and enabled the smt parser to read in these symbols. Also...

diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index 83e3447ac0699ce0c19ad887aaa43b8401e43070..4539a6d434ba16edf19f838a99cace44431a1423 100644 (file)
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -33,9 +33,11 @@ options {
 }
 
 @lexer::includes {
-/** This suppresses warnings about the redefinition of token symbols between different
-  * parsers. The redefinitions should be harmless as long as no client: (a) #include's 
-  * the lexer headers for two grammars AND (b) uses the token symbol definitions. */
+/** This suppresses warnings about the redefinition of token symbols between
+  * different parsers. The redefinitions should be harmless as long as no
+  * client: (a) #include's the lexer headers for two grammars AND (b) uses the
+  * token symbol definitions.
+  */
 #pragma GCC system_header
 
 /* This improves performance by ~10 percent on big inputs.
@@ -90,7 +92,9 @@ void
 setLogic(ParserState *parserState, const std::string& name) {
   if( name == "QF_UF" ) {
     parserState->mkSort("U");
-  } else {
+  } else if(name == "QF_LRA"){
+    parserState->mkSort("Real");
+  } else{
     // NOTE: Theory types go here
     Unhandled(name);
   }
@@ -269,6 +273,18 @@ builtinOp[CVC4::Kind& kind]
   | IFF_TOK      { $kind = CVC4::kind::IFF;     }
   | EQUAL_TOK    { $kind = CVC4::kind::EQUAL;   }
   | DISTINCT_TOK { $kind = CVC4::kind::DISTINCT; }
+  | GREATER_THAN_TOK
+                 { $kind = CVC4::kind::GT; }
+  | GREATER_THAN_TOK EQUAL_TOK
+                 { $kind = CVC4::kind::GEQ; }
+  | LESS_THAN_TOK EQUAL_TOK
+                 { $kind = CVC4::kind::LEQ; }
+  | LESS_THAN_TOK
+                 { $kind = CVC4::kind::LT; }
+  | PLUS_TOK     { $kind = CVC4::kind::PLUS; }
+  | STAR_TOK     { $kind = CVC4::kind::MULT; }
+  | TILDE_TOK    { $kind = CVC4::kind::UMINUS; }
+  | MINUS_TOK    { $kind = CVC4::kind::MINUS; }
     // NOTE: Theory operators go here
     /* TODO: lt, gt, plus, minus, etc. */
   ;

diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index 3b79192d2b7c85fd441c7393adeffccec82f809c..fafa33a682a468992c151e588c3e550df3c545c1 100644 (file)
--- 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"

diff --git a/test/unit/expr/node_manager_white.h b/test/unit/expr/node_manager_white.h
index a43e3290898bc92ccbf42d829fa8791c13aeb031..af38c790b5aa11ed23cf50543158a077e2ca4266 100644 (file)
--- a/test/unit/expr/node_manager_white.h
+++ b/test/unit/expr/node_manager_white.h
@@ -36,7 +36,7 @@ class NodeManagerWhite : public CxxTest::TestSuite {
 public:
 
   void setUp() {
-    d_ctxt = new Context;
+    d_ctxt = new Context();
     d_nm = new NodeManager(d_ctxt);
     d_scope = new NodeManagerScope(d_nm);
   }

diff --git a/test/unit/expr/node_white.h b/test/unit/expr/node_white.h
index 9facd00f66c7bfa273eb81946af8fbc138b6c975..91a3527972f257153cc41d61ea7026efe8e495ea 100644 (file)
--- a/test/unit/expr/node_white.h
+++ b/test/unit/expr/node_white.h
@@ -39,7 +39,7 @@ class NodeWhite : public CxxTest::TestSuite {
 public:
 
   void setUp() {
-    d_ctxt = new Context;
+    d_ctxt = new Context();
     d_nm = new NodeManager(d_ctxt);
     d_scope = new NodeManagerScope(d_nm);
   }