From: Tim King <taking@cs.nyu.edu>
Date: Wed, 28 Apr 2010 14:52:22 +0000 (+0000)
Subject: Added theory/arith/kind and enabled the smt parser to read in these symbols. Also... 
X-Git-Tag: cvc5-1.0.0~9105
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7a8454030fdbb1e6c2a6db7ce18eafe0764eaf4a;p=cvc5.git

Added theory/arith/kind and enabled the smt parser to read in these symbols. Also a bug fix to a couple of unit tests.
---

diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index 83e3447ac..4539a6d43 100644
--- 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 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"
diff --git a/test/unit/expr/node_manager_white.h b/test/unit/expr/node_manager_white.h
index a43e32908..af38c790b 100644
--- 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 9facd00f6..91a352797 100644
--- 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);
   }