Enabling RDL/IDL in SMT v1 and adding some simple tests

11 files changed, 69 insertions, 86 deletions

diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index a9b3c461d..4e4b0309f 100644
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -19,6 +19,7 @@
 #include "expr/expr_manager.h"
 #include "parser/input.h"
 #include "parser/parser.h"
+#include "parser/smt/smt.h"
 #include "parser/smt2/smt2.h"
 
 namespace CVC4 {
@@ -64,7 +65,7 @@ ParserBuilder::ParserBuilder(ExprManager& exprManager, const std::string& filena
 }
 
 Parser *ParserBuilder::build() throw (InputStreamException,AssertionException) {
-  Input *input;
+  Input *input = NULL;
   switch( d_inputType ) {
   case FILE_INPUT:
     input = Input::newFileInput(d_lang,d_filename,d_mmap);
@@ -77,8 +78,12 @@ Parser *ParserBuilder::build() throw (InputStreamException,AssertionException) {
   case STRING_INPUT:
     input = Input::newStringInput(d_lang,d_stringInput,d_filename);
     break;
+  default:
+    Unreachable();
   }
   switch(d_lang) {
+  case LANG_SMTLIB:
+    return new Smt(&d_exprManager, input, d_strictMode);
   case LANG_SMTLIB_V2:
     return new Smt2(&d_exprManager, input, d_strictMode);
   default:
diff --git a/src/parser/smt/Makefile.am b/src/parser/smt/Makefile.am
index 792527816..731676644 100644
--- a/src/parser/smt/Makefile.am
+++ b/src/parser/smt/Makefile.am
@@ -24,6 +24,8 @@ ANTLR_STUFF = \
 
 libparsersmt_la_SOURCES = \
 	Smt.g \
+        smt.h \
+        smt.cpp \
 	smt_input.h \
 	smt_input.cpp \
 	$(ANTLR_STUFF)
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index 9c609d0d4..c11f350a6 100644
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -64,6 +64,7 @@ namespace CVC4 {
 #include "expr/type.h"
 #include "parser/antlr_input.h"
 #include "parser/parser.h"
+#include "parser/smt/smt.h"
 #include "util/integer.h"
 #include "util/output.h"
 #include "util/rational.h"
@@ -75,7 +76,7 @@ using namespace CVC4::parser;
 /* These need to be macros so they can refer to the PARSER macro, which will be defined
  * by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */
 #undef PARSER_STATE 
-#define PARSER_STATE ((Parser*)PARSER->super)
+#define PARSER_STATE ((Smt*)PARSER->super)
 #undef EXPR_MANAGER
 #define EXPR_MANAGER PARSER_STATE->getExprManager()
 #undef MK_EXPR
@@ -83,24 +84,6 @@ using namespace CVC4::parser;
 #undef MK_CONST
 #define MK_CONST EXPR_MANAGER->mkConst
 
-/**   
- * Sets the logic for the current benchmark. Declares any logic symbols.
- *
- * @param parser the CVC4 Parser object
- * @param name the name of the logic (e.g., QF_UF, AUFLIA)
- */
-static void
-setLogic(Parser *parser, const std::string& name) {
-  if( name == "QF_UF" ) {
-    parser->mkSort("U");
-  } else if(name == "QF_LRA"){
-    parser->defineType("Real", parser->getExprManager()->realType());
-  } else if(name == "QF_BV"){
-  } else {
-    // NOTE: Theory types go here
-    Unhandled(name);
-  }
-}
 }
 
 
@@ -155,7 +138,7 @@ benchAttribute returns [CVC4::Command* smt_command]
   Expr expr;
 }
   : LOGIC_TOK identifier[name,CHECK_NONE,SYM_VARIABLE]
-    { setLogic(PARSER_STATE,name);
+    { PARSER_STATE->setLogic(name);
       smt_command = new SetBenchmarkLogicCommand(name);   }
   | ASSUMPTION_TOK annotatedFormula[expr]
     { smt_command = new AssertCommand(expr);   }
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index f6089382c..5cf902260 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -13,36 +13,13 @@
  ** Definitions of SMT2 constants.
  **/
 
-#include <ext/hash_map>
-namespace std {
-using namespace __gnu_cxx;
-}
-
 #include "parser/parser.h"
+#include "parser/smt/smt.h"
 #include "parser/smt2/smt2.h"
 
 namespace CVC4 {
 namespace parser {
 
-std::hash_map<const std::string, Smt2::Logic, CVC4::StringHashFunction> Smt2::newLogicMap() {
-  std::hash_map<const std::string, Smt2::Logic, CVC4::StringHashFunction> logicMap;
-  logicMap["QF_AX"] = QF_AX;
-  logicMap["QF_BV"] = QF_BV;
-  logicMap["QF_IDL"] = QF_IDL;
-  logicMap["QF_LIA"] = QF_LIA;
-  logicMap["QF_LRA"] = QF_LRA;
-  logicMap["QF_NIA"] = QF_NIA;
-  logicMap["QF_RDL"] = QF_RDL;
-  logicMap["QF_UF"] = QF_UF;
-  logicMap["QF_UFIDL"] = QF_UFIDL;
-  return logicMap;
-}
-
-Smt2::Logic Smt2::toLogic(const std::string& name) {
-  static std::hash_map<const std::string, Smt2::Logic, CVC4::StringHashFunction> logicMap = newLogicMap();
-  return logicMap[name];
-}
-
 Smt2::Smt2(ExprManager* exprManager, Input* input, bool strictMode) :
   Parser(exprManager,input,strictMode),
   d_logicSet(false) {
@@ -115,38 +92,38 @@ bool Smt2::logicIsSet() {
  */
 void Smt2::setLogic(const std::string& name) {
   d_logicSet = true;
-  d_logic = toLogic(name);
+  d_logic = Smt::toLogic(name);
 
   // Core theory belongs to every logic
   addTheory(THEORY_CORE);
 
   switch(d_logic) {
-  case QF_IDL:
-  case QF_LIA:
-  case QF_NIA:
+  case Smt::QF_IDL:
+  case Smt::QF_LIA:
+  case Smt::QF_NIA:
     addTheory(THEORY_INTS);
     break;
     
-  case QF_LRA:
-  case QF_RDL:
+  case Smt::QF_LRA:
+  case Smt::QF_RDL:
     addTheory(THEORY_REALS);
     break;
 
-  case QF_UFIDL:
+  case Smt::QF_UFIDL:
     addTheory(THEORY_INTS);
     // falling-through on purpose, to add UF part of UFIDL
 
-  case QF_UF:
+  case Smt::QF_UF:
     addOperator(kind::APPLY_UF);
     break;
 
-  case AUFLIA:
-  case AUFLIRA:
-  case AUFNIRA:
-  case QF_AUFBV:
-  case QF_AUFLIA:
-  case QF_AX:
-  case QF_BV:
+  case Smt::AUFLIA:
+  case Smt::AUFLIRA:
+  case Smt::AUFNIRA:
+  case Smt::QF_AUFBV:
+  case Smt::QF_AUFLIA:
+  case Smt::QF_AX:
+  case Smt::QF_BV:
     Unhandled(name);
   }
 }
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 5eae90fa3..0e057db68 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -18,11 +18,8 @@
 #ifndef __CVC4__PARSER__SMT2_H
 #define __CVC4__PARSER__SMT2_H
 
-#include <ext/hash_map>
-namespace std { using namespace __gnu_cxx; }
-
-#include "util/hash.h"
 #include "parser/parser.h"
+#include "parser/smt/smt.h"
 
 namespace CVC4 {
 
@@ -34,23 +31,6 @@ class Smt2 : public Parser {
   friend class ParserBuilder;
 
 public:
-  enum Logic {
-    AUFLIA,
-    AUFLIRA,
-    AUFNIRA,
-    QF_AUFBV,
-    QF_AUFLIA,
-    QF_AX,
-    QF_BV,
-    QF_IDL,
-    QF_LIA,
-    QF_LRA,
-    QF_NIA,
-    QF_RDL,
-    QF_UF,
-    QF_UFIDL
-  };
-
   enum Theory {
     THEORY_ARRAYS,
     THEORY_BITVECTORS,
@@ -62,7 +42,7 @@ public:
 
 private:
   bool d_logicSet;
-  Logic d_logic;
+  Smt::Logic d_logic;
 
 protected:
   Smt2(ExprManager* exprManager, Input* input, bool strictMode = false);
@@ -92,12 +72,9 @@ public:
   void
   setInfo(const std::string& flag, const SExpr& sexpr);
 
-  static Logic toLogic(const std::string& name);
-
 private:
 
   void addArithmeticOperators();
-  static std::hash_map<const std::string, Logic, CVC4::StringHashFunction> newLogicMap();
 };
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 0b8a60495..66112defc 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -14,13 +14,18 @@ TESTS =	\
 	ite_real_valid.smt \
 	let.smt \
 	let2.smt \
-	simple2.smt \
 	simple.smt \
+	simple2.smt \
+        simple-lra.smt \
+        simple-rdl.smt \
 	simple-uf.smt \
 	ite.smt2 \
 	ite2.smt2 \
 	ite3.smt2 \
 	ite4.smt2 \
+        simple-lra.smt2 \
+        simple-rdl.smt2 \
+	simple-uf.smt2 \
 	bug32.cvc \
 	hole6.cvc \
 	logops.01.cvc \
diff --git a/test/regress/regress0/simple-lra.smt b/test/regress/regress0/simple-lra.smt
new file mode 100644
index 000000000..c80632a96
--- /dev/null
+++ b/test/regress/regress0/simple-lra.smt
@@ -0,0 +1,6 @@
+(benchmark simple_lra
+  :logic QF_LRA
+  :status unsat
+  :extrafuns ((x Real) (y Real))
+  :formula (not (implies (and (> x 0) (< (* 2 x) y)) (and (> y 0) (< x y))))
+)
diff --git a/test/regress/regress0/simple-lra.smt2 b/test/regress/regress0/simple-lra.smt2
new file mode 100644
index 000000000..585c62954
--- /dev/null
+++ b/test/regress/regress0/simple-lra.smt2
@@ -0,0 +1,6 @@
+(set-logic QF_LRA)
+(set-info :status unsat)
+(declare-fun x () Real)
+(declare-fun y () Real)
+(assert (not (=> (and (> x 0) (< (* 2 x) y)) (and (> y 0) (< x y)))))
+(check-sat)
diff --git a/test/regress/regress0/simple-rdl.smt b/test/regress/regress0/simple-rdl.smt
new file mode 100644
index 000000000..080c69f93
--- /dev/null
+++ b/test/regress/regress0/simple-rdl.smt
@@ -0,0 +1,6 @@
+(benchmark simple_rdl
+  :logic QF_RDL
+  :status unsat
+  :extrafuns ((x Real) (y Real))
+  :formula (not (implies (< (- x y) 0) (< x y)))
+)
diff --git a/test/regress/regress0/simple-rdl.smt2 b/test/regress/regress0/simple-rdl.smt2
new file mode 100644
index 000000000..d2c0a4cde
--- /dev/null
+++ b/test/regress/regress0/simple-rdl.smt2
@@ -0,0 +1,7 @@
+(set-logic QF_RDL)
+(set-info :status unsat)
+(declare-fun x () Real)
+(declare-fun y () Real)
+(assert (not (=> (< (- x y) 0) (< x y))))
+(check-sat)
+
diff --git a/test/regress/regress0/simple-uf.smt2 b/test/regress/regress0/simple-uf.smt2
new file mode 100644
index 000000000..ef3b3cf86
--- /dev/null
+++ b/test/regress/regress0/simple-uf.smt2
@@ -0,0 +1,9 @@
+(set-logic QF_UF)
+(set-info :status unsat)
+(declare-sort A 0)
+(declare-sort B 0)
+(declare-fun x () A)
+(declare-fun y () A)
+(declare-fun f (A) B)
+(assert (not (=> (= x y) (= (f x) (f y)))))
+(check-sat)