From 9348417ac5f12e8269a52a7c9b5a01a4aa558c74 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Tue, 12 Jun 2012 21:11:15 +0000
Subject: Fix to SMT-LIBv1 parser: QF_UF declares sort "U", but other *UF*
 logics do not (e.g. QF_UFLIA).

Also fix a syntax error in a regression test (CVC4 is too lenient to catch it though---CVC3 tripped over it).

Also add additional parts for "make submission" in the top-level makefile
---
 src/parser/smt/smt.cpp | 42 +++++++++++++++++++++---------------------
 src/parser/smt/smt.h   |  1 -
 2 files changed, 21 insertions(+), 22 deletions(-)

(limited to 'src/parser/smt')

diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp
index 4d3c1d086..e554cee10 100644
--- a/src/parser/smt/smt.cpp
+++ b/src/parser/smt/smt.cpp
@@ -175,11 +175,6 @@ bool Smt::logicIsSet() {
   return d_logicSet;
 }
 
-inline void Smt::addUf() {
-  addTheory(Smt::THEORY_EMPTY);
-  addOperator(kind::APPLY_UF);
-}
-
 void Smt::setLogic(const std::string& name) {
   d_logicSet = true;
   d_logic = toLogic(name);
@@ -209,24 +204,25 @@ void Smt::setLogic(const std::string& name) {
   case QF_UFLIA:
   case QF_UFNIA:// nonstandard logic
     addTheory(THEORY_INTS);
-    addUf();
+    addOperator(kind::APPLY_UF);
     break;
 
   case QF_UFLRA:
   case QF_UFNRA:
     addTheory(THEORY_REALS);
-    addUf();
+    addOperator(kind::APPLY_UF);
     break;
 
   case QF_UFLIRA:// nonstandard logic
   case QF_UFNIRA:// nonstandard logic
     addTheory(THEORY_INTS);
     addTheory(THEORY_REALS);
-    addUf();
+    addOperator(kind::APPLY_UF);
     break;
 
   case QF_UF:
-    addUf();
+    addTheory(THEORY_EMPTY);
+    addOperator(kind::APPLY_UF);
     break;
 
   case QF_BV:
@@ -239,25 +235,25 @@ void Smt::setLogic(const std::string& name) {
     break;
 
   case QF_UFBV:
-    addUf();
+    addOperator(kind::APPLY_UF);
     addTheory(THEORY_BITVECTORS);
     break;
 
   case QF_AUFBV:
-    addUf();
+    addOperator(kind::APPLY_UF);
     addTheory(THEORY_ARRAYS_EX);
     addTheory(THEORY_BITVECTORS);
     break;
 
   case QF_AUFBVLIA:
-    addUf();
+    addOperator(kind::APPLY_UF);
     addTheory(THEORY_ARRAYS_EX);
     addTheory(THEORY_BITVECTORS);
     addTheory(THEORY_INTS);
     break;
 
   case QF_AUFBVLRA:
-    addUf();
+    addOperator(kind::APPLY_UF);
     addTheory(THEORY_ARRAYS_EX);
     addTheory(THEORY_BITVECTORS);
     addTheory(THEORY_REALS);
@@ -265,13 +261,13 @@ void Smt::setLogic(const std::string& name) {
 
   case QF_AUFLIA:
     addTheory(THEORY_INT_ARRAYS_EX);
-    addUf();
+    addOperator(kind::APPLY_UF);
     addTheory(THEORY_INTS);
     break;
 
   case QF_AUFLIRA:
     addTheory(THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX);
-    addUf();
+    addOperator(kind::APPLY_UF);
     addTheory(THEORY_INTS);
     addTheory(THEORY_REALS);
     break;
@@ -281,14 +277,14 @@ void Smt::setLogic(const std::string& name) {
     /* fall through */
   case QF_ALL_SUPPORTED:
     addTheory(THEORY_ARRAYS_EX);
-    addUf();
+    addOperator(kind::APPLY_UF);
     addTheory(THEORY_INTS);
     addTheory(THEORY_REALS);
     addTheory(THEORY_BITVECTORS);
     break;
 
   case AUFLIA:
-    addUf();
+    addOperator(kind::APPLY_UF);
     addTheory(THEORY_INTS);
     addTheory(THEORY_INT_ARRAYS_EX);
     addTheory(THEORY_QUANTIFIERS);
@@ -296,7 +292,7 @@ void Smt::setLogic(const std::string& name) {
 
   case AUFLIRA:
   case AUFNIRA:
-    addUf();
+    addOperator(kind::APPLY_UF);
     addTheory(THEORY_INTS);
     addTheory(THEORY_REALS);
     addTheory(THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX);
@@ -304,20 +300,24 @@ void Smt::setLogic(const std::string& name) {
     break;
 
   case LRA:
+    addTheory(THEORY_REALS);
+    addTheory(THEORY_QUANTIFIERS);
+    break;
+
   case UFNIA:
-    addUf();
+    addOperator(kind::APPLY_UF);
     addTheory(THEORY_INTS);
     addTheory(THEORY_QUANTIFIERS);
     break;
   case UFNIRA:
-    addUf();
+    addOperator(kind::APPLY_UF);
     addTheory(THEORY_INTS);
     addTheory(THEORY_REALS);
     addTheory(THEORY_QUANTIFIERS);
     break;
 
   case UFLRA:
-    addUf();
+    addOperator(kind::APPLY_UF);
     addTheory(THEORY_REALS);
     addTheory(THEORY_QUANTIFIERS);
     break;
diff --git a/src/parser/smt/smt.h b/src/parser/smt/smt.h
index 7b1dfc345..b82d3a01c 100644
--- a/src/parser/smt/smt.h
+++ b/src/parser/smt/smt.h
@@ -116,7 +116,6 @@ public:
 private:
 
   void addArithmeticOperators();
-  void addUf();
   static std::hash_map<const std::string, Logic, CVC4::StringHashFunction> newLogicMap();
 };/* class Smt */
 
-- 
cgit v1.2.3