Merge pull request #29 from kbansal/alternatefix

Fix for emptyset in smt2 parser, sets translator to quantified logic, misc

8 files changed, 186 insertions, 47 deletions

diff --git a/examples/sets-translate/sets_translate.cpp b/examples/sets-translate/sets_translate.cpp
index 6cf2b61e2..dbc7100c0 100644
--- a/examples/sets-translate/sets_translate.cpp
+++ b/examples/sets-translate/sets_translate.cpp
@@ -20,6 +20,7 @@
 #include <typeinfo>
 #include <cassert>
 #include <vector>
+#include <boost/algorithm/string.hpp> // include Boost, a C++ library
 
 
 #include "options/options.h"
@@ -36,6 +37,43 @@ using namespace CVC4::options;
 
 bool nonsense(char c) { return !isalnum(c); } 
 
+const bool enableAxioms = true;
+
+string setaxioms[] = {
+  "(declare-fun inHOLDA (HOLDB (Set HOLDB)) Bool)",
+  "",
+  "(declare-fun unionHOLDA ((Set HOLDB) (Set HOLDB)) (Set HOLDB))",
+  "(assert (forall ((?X (Set HOLDB)) (?Y (Set HOLDB)) (?x HOLDB))",
+  "                (= (inHOLDA ?x (unionHOLDA ?X ?Y))",
+  "                     (or (inHOLDA ?x ?X) (inHOLDA ?x ?Y))",
+  "                ) ) )",
+  "",
+  "",
+  "(declare-fun intersectionHOLDA ((Set HOLDB) (Set HOLDB)) (Set HOLDB))",
+  "(assert (forall ((?X (Set HOLDB)) (?Y (Set HOLDB)) (?x HOLDB))",
+  "                (= (inHOLDA ?x (intersectionHOLDA ?X ?Y))",
+  "                     (and (inHOLDA ?x ?X) (inHOLDA ?x ?Y))",
+  "                ) ) )",
+  "",
+  "(declare-fun setminusHOLDA ((Set HOLDB) (Set HOLDB)) (Set HOLDB))",
+  "(assert (forall ((?X (Set HOLDB)) (?Y (Set HOLDB)) (?x HOLDB))",
+  "                (= (inHOLDA ?x (setminusHOLDA ?X ?Y))",
+  "                     (and (inHOLDA ?x ?X) (not (inHOLDA ?x ?Y)))",
+  "                ) ) )",
+  "",
+  "(declare-fun setenumHOLDA (HOLDB) (Set HOLDB))",
+  "(assert (forall ((?x HOLDB) (?y HOLDB))",
+  "                (= (inHOLDA ?x (setenumHOLDA ?y))",
+  "                     (= ?x ?y)",
+  "                ) ) )",
+  "",
+  "(declare-fun emptysetHOLDA () (Set HOLDB))",
+  "(assert (forall ((?x HOLDB)) (not (inHOLDA ?x emptysetHOLDA)) ) )",
+  "",
+  "(define-fun subseteqHOLDA ((X (Set HOLDB)) (Y (Set HOLDB))) Bool (= (unionHOLDA X Y) Y))",
+  ""
+};
+
 class Mapper {
   set< Type > setTypes;
   map< Type, Type > mapTypes;
@@ -43,6 +81,7 @@ class Mapper {
   hash_map< Expr, Expr, ExprHashFunction > substitutions;
   ostringstream sout;
   ExprManager* em;
+  int depth;
 
   Expr add(SetType t, Expr e) {
 
@@ -70,62 +109,81 @@ class Mapper {
       elet_t.push_back(elementType);
       elet_t.push_back(t);
 
-      sout << "(define-fun emptyset" << elementTypeAsString << "    "
-           << " ()"
-           << " " << name
-           << " ( (as const " << name << ") false ) )" << endl;
+      if(!enableAxioms)
+        sout << "(define-fun emptyset" << elementTypeAsString << "    "
+             << " ()"
+             << " " << name
+             << " ( (as const " << name << ") false ) )" << endl;
       setoperators[ make_pair(t, kind::EMPTYSET) ] =
         em->mkVar( std::string("emptyset") + elementTypeAsString,
                    t);
 
-      sout << "(define-fun setenum" << elementTypeAsString << "     "
-           << " ( (x " << elementType << ") )"
-           << " " << name << ""
-           << " (store emptyset" << elementTypeAsString << " x true) )" << endl;
+      if(!enableAxioms)
+        sout << "(define-fun setenum" << elementTypeAsString << "     "
+             << " ( (x " << elementType << ") )"
+             << " " << name << ""
+             << " (store emptyset" << elementTypeAsString << " x true) )" << endl;
       setoperators[ make_pair(t, kind::SET_SINGLETON) ] =
         em->mkVar( std::string("setenum") + elementTypeAsString,
                    em->mkFunctionType( elementType, t ) );
 
-      sout << "(define-fun union" << elementTypeAsString << "       "
-           << " ( (s1 " << name << ") (s2 " << name << ") )"
-           << " " << name << ""
-           << " ((_ map or) s1 s2))" << endl;
+      if(!enableAxioms)
+        sout << "(define-fun union" << elementTypeAsString << "       "
+             << " ( (s1 " << name << ") (s2 " << name << ") )"
+             << " " << name << ""
+             << " ((_ map or) s1 s2))" << endl;
       setoperators[ make_pair(t, kind::UNION) ] =
         em->mkVar( std::string("union") + elementTypeAsString,
                    em->mkFunctionType( t_t, t ) );
 
-      sout << "(define-fun intersection" << elementTypeAsString << ""
-           << " ( (s1 " << name << ") (s2 " << name << ") )"
-           << " " << name << ""
-           << " ((_ map and) s1 s2))" << endl;
+      if(!enableAxioms)
+        sout << "(define-fun intersection" << elementTypeAsString << ""
+             << " ( (s1 " << name << ") (s2 " << name << ") )"
+             << " " << name << ""
+             << " ((_ map and) s1 s2))" << endl;
       setoperators[ make_pair(t, kind::INTERSECTION) ] =
         em->mkVar( std::string("intersection") + elementTypeAsString,
                    em->mkFunctionType( t_t, t ) );
 
-      sout << "(define-fun setminus" << elementTypeAsString << "    "
-           << " ( (s1 " << name << ") (s2 " << name << ") )"
-           << " " << name << ""
-           << " (intersection" << elementTypeAsString << " s1 ((_ map not) s2)))" << endl;
+      if(!enableAxioms)
+        sout << "(define-fun setminus" << elementTypeAsString << "    "
+             << " ( (s1 " << name << ") (s2 " << name << ") )"
+             << " " << name << ""
+             << " (intersection" << elementTypeAsString << " s1 ((_ map not) s2)))" << endl;
       setoperators[ make_pair(t, kind::SETMINUS) ] =
         em->mkVar( std::string("setminus") + elementTypeAsString,
                    em->mkFunctionType( t_t, t ) );
 
-      sout << "(define-fun in" << elementTypeAsString << "          "
-           << " ( (x " << elementType << ")" << " (s " << name << "))"
-           << " Bool"
-           << " (select s x) )" << endl;
+      if(!enableAxioms)
+        sout << "(define-fun in" << elementTypeAsString << "          "
+             << " ( (x " << elementType << ")" << " (s " << name << "))"
+             << " Bool"
+             << " (select s x) )" << endl;
       setoperators[ make_pair(t, kind::MEMBER) ] =
         em->mkVar( std::string("in") + elementTypeAsString,
                    em->mkPredicateType( elet_t ) );
 
-      sout << "(define-fun subseteq" << elementTypeAsString << "    "
-           << " ( (s1 " << name << ") (s2 " << name << ") )"
-           << " Bool"
-           <<" (= emptyset" << elementTypeAsString << " (setminus" << elementTypeAsString << " s1 s2)) )" << endl;
+      if(!enableAxioms)
+        sout << "(define-fun subseteq" << elementTypeAsString << "    "
+             << " ( (s1 " << name << ") (s2 " << name << ") )"
+             << " Bool"
+             <<" (= emptyset" << elementTypeAsString << " (setminus" << elementTypeAsString << " s1 s2)) )" << endl;
       setoperators[ make_pair(t, kind::SUBSET) ] =
         em->mkVar( std::string("subseteq") + elementTypeAsString,
                    em->mkPredicateType( t_t ) );
 
+      if(enableAxioms) {
+        int N = sizeof(setaxioms) / sizeof(setaxioms[0]);
+        for(int i = 0; i < N; ++i) {
+          string s = setaxioms[i];
+          ostringstream oss; oss << Expr::setlanguage(language::output::LANG_SMTLIB_V2) << elementType;
+          boost::replace_all(s, "HOLDA", elementTypeAsString);
+          boost::replace_all(s, "HOLDB", oss.str());
+          if( s == "" ) continue;
+          sout << s << endl;
+        }
+      }
+
     }
     Expr ret;
     if(e.getKind() == kind::EMPTYSET) {
@@ -140,7 +198,7 @@ class Mapper {
   }
 
 public:
-  Mapper(ExprManager* e) : em(e) {
+  Mapper(ExprManager* e) : em(e),depth(0) {
     sout << Expr::setlanguage(language::output::LANG_SMTLIB_V2);
   }
 
@@ -153,17 +211,24 @@ public:
 
   Expr collectSortsExpr(Expr e)
   {
+    if(substitutions.find(e) != substitutions.end()) {
+      return substitutions[e];
+    }
+    ++depth;
     Expr old_e = e;
     for(unsigned i = 0; i < e.getNumChildren(); ++i) {
       collectSortsExpr(e[i]);
     }
     e = e.substitute(substitutions);
+    // cout << "[debug] " << e << " " << e.getKind() << " " << theory::kindToTheoryId(e.getKind()) << endl;
     if(theory::kindToTheoryId(e.getKind()) == theory::THEORY_SETS) {
       SetType t = SetType(e.getType().isBoolean() ? e[1].getType() : e.getType());
       substitutions[e] = add(t, e);
       e = e.substitute(substitutions);
     }
-    // cout << old_e << " => " << e << endl;
+    substitutions[old_e] = e;
+    // cout << ";"; for(int i = 0; i < depth; ++i) cout << " "; cout << old_e << " => " << e << endl;
+    --depth;
     return e;
   }
 
@@ -187,6 +252,7 @@ int main(int argc, char* argv[])
     Options options;
     options.set(inputLanguage, language::input::LANG_SMTLIB_V2);
     cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2);
+    // cout << Expr::dag(0);
     ExprManager exprManager(options);
 
     Mapper m(&exprManager);
diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index ee4e2ff37..27a020ac5 100644
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -296,6 +296,27 @@ inline bool isSimpleChar(char ch) {
   return isalnum(ch) || (strchr("~!@$%^&*_-+=<>.?/", ch) != NULL);
 }
 
+size_t wholeWordMatch(string input, string pattern, bool (*isWordChar)(char)) {
+  size_t st = 0;
+  size_t N = input.size();
+  while(st < N) {
+    while( st < N && (*isWordChar)(input[st])  == false ) st++;
+    size_t en = st;
+    while(en + 1 < N && (*isWordChar)(input[en + 1]) == true) en++;
+    if(en - st + 1 == pattern.size()) {
+      bool match = true;
+      for(size_t i = 0; match && i < pattern.size(); ++i) {
+        match &= (pattern[i] == input[st+i]);
+      }
+      if(match == true) {
+        return st;
+      }
+    }
+    st = en + 1;
+  }
+  return string::npos;
+}
+
 /**
  * Gets part of original input and tries to visually hint where the
  * error might be.
@@ -372,12 +393,9 @@ std::string parseErrorHelper(const char* lineStart, int charPositionInLine, cons
         // likely it is also in original message? if so, very likely
         // we found the right place
         string word = slice.substr(caretPos, (caretPosOrig - caretPos + 1));
-        int messagePosSt = message.find(word);
-        int messagePosEn = messagePosSt + (caretPosOrig - caretPos);
-        if( (size_t)messagePosSt < string::npos &&
-            (messagePosSt == 0 || !isSimpleChar(message[messagePosSt-1]) ) &&
-            ((size_t)messagePosEn+1 == message.size() || !isSimpleChar(message[messagePosEn+1]) ) ) {
-          // ^the complicated if statement is just 'whole-word' match
+        size_t matchLoc = wholeWordMatch(message, word, isSimpleChar);
+        Debug("friendlyparser") << "[friendlyparser] matchLoc = " << matchLoc << endl;
+        if( matchLoc != string::npos ) {
           Debug("friendlyparser") << "[friendlyparser] Feeling good." << std::endl;
         }
       }
@@ -395,13 +413,10 @@ std::string parseErrorHelper(const char* lineStart, int charPositionInLine, cons
           --nearestWordSt;
         }
         string word = slice.substr(nearestWordSt, (nearestWordEn - nearestWordSt + 1));
+        size_t matchLoc = wholeWordMatch(message, word, isSimpleChar);
         Debug("friendlyparser") << "[friendlyparser] nearest word = " << word << std::endl;
-        int messagePosSt = message.find(word);
-        int messagePosEn = messagePosSt + (nearestWordEn - nearestWordSt + 1);
-        if( (size_t)messagePosSt < string::npos &&
-            (messagePosSt == 0 || !isSimpleChar(message[messagePosSt-1]) ) &&
-            ((size_t)messagePosEn+1 == message.size() || !isSimpleChar(message[messagePosEn+1]) ) ) {
-          // ^the complicated if statement is just 'whole-word' match
+        Debug("friendlyparser") << "[friendlyparser] matchLoc = " << matchLoc << endl;
+        if( matchLoc != string::npos ) {
           Debug("friendlyparser") << "[friendlyparser] strong evidence that caret should be at "
                                   << nearestWordSt << std::endl;
           caretPos = nearestWordSt;
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index c857f3905..63179cf42 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1786,10 +1786,10 @@ REALLCHAR_TOK : 're.allchar';
 
 FMFCARD_TOK : 'fmf.card';
 
-EMPTYSET_TOK: 'emptyset'; // Other set theory operators are not
-                          // tokenized and handled directly when
-                          // processing a term
-
+EMPTYSET_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) }? 'emptyset';
+// Other set theory operators are not
+// tokenized and handled directly when
+// processing a term
 
 /**
  * A sequence of printable ASCII characters (except backslash) that starts
diff --git a/test/Makefile.am b/test/Makefile.am
index 1da15dc43..236443eb9 100644
--- a/test/Makefile.am
+++ b/test/Makefile.am
@@ -57,6 +57,7 @@ subdirs_to_check = \
 	regress/regress0/fmf \
 	regress/regress0/strings \
 	regress/regress0/sets \
+	regress/regress0/parser \
 	regress/regress1 \
 	regress/regress1/arith \
 	regress/regress2 \
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 521993db3..10148e5bc 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -1,4 +1,4 @@
-SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf strings sets
+SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf strings sets parser
 DIST_SUBDIRS = $(SUBDIRS) #. arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf strings sets
 
 # don't override a BINARY imported from a personal.mk
diff --git a/test/regress/regress0/parser/Makefile b/test/regress/regress0/parser/Makefile
new file mode 100644
index 000000000..be157f57a
--- /dev/null
+++ b/test/regress/regress0/parser/Makefile
@@ -0,0 +1,8 @@
+topdir = ../../../..
+srcdir = test/regress/regress0/parser
+
+include $(topdir)/Makefile.subdir
+
+# synonyms for "check"
+.PHONY: test
+test: check
diff --git a/test/regress/regress0/parser/Makefile.am b/test/regress/regress0/parser/Makefile.am
new file mode 100644
index 000000000..389c80e09
--- /dev/null
+++ b/test/regress/regress0/parser/Makefile.am
@@ -0,0 +1,42 @@
+# don't override a BINARY imported from a personal.mk
+@mk_if@eq ($(BINARY),)
+@mk_empty@BINARY = cvc4
+end@mk_if@
+
+LOG_COMPILER = @srcdir@/../../run_regression
+AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT)
+
+if AUTOMAKE_1_11
+# old-style (pre-automake 1.12) test harness
+TESTS_ENVIRONMENT = \
+	$(LOG_COMPILER) \
+	$(AM_LOG_FLAGS) $(LOG_FLAGS)
+endif
+
+MAKEFLAGS = -k
+
+# These are run for all build profiles.
+# If a test shouldn't be run in e.g. competition mode,
+# put it below in "TESTS +="
+TESTS =	\
+	declarefun-emptyset-uf.smt2
+
+EXTRA_DIST = $(TESTS)
+
+#if CVC4_BUILD_PROFILE_COMPETITION
+#else
+#TESTS += \
+#	error.cvc
+#endif
+
+# disabled tests, yet distribute
+#EXTRA_DIST += \
+#	setofsets-disequal.smt2
+
+# synonyms for "check"
+.PHONY: regress regress0 test
+regress regress0 test: check
+
+# do nothing in this subdir
+.PHONY: regress1 regress2 regress3
+regress1 regress2 regress3:
diff --git a/test/regress/regress0/parser/declarefun-emptyset-uf.smt2 b/test/regress/regress0/parser/declarefun-emptyset-uf.smt2
new file mode 100644
index 000000000..a6e514407
--- /dev/null
+++ b/test/regress/regress0/parser/declarefun-emptyset-uf.smt2
@@ -0,0 +1,7 @@
+; EXPECT: sat
+(set-logic QF_UF)
+(declare-sort T 0)
+(declare-fun union () T)
+(declare-fun emptyset () T)
+(assert (= union emptyset))
+(check-sat)