diff options
-rw-r--r-- | examples/sets-translate/sets_translate.cpp | 126 | ||||
-rw-r--r-- | src/parser/antlr_input.cpp | 39 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 8 | ||||
-rw-r--r-- | test/Makefile.am | 1 | ||||
-rw-r--r-- | test/regress/regress0/Makefile.am | 2 | ||||
-rw-r--r-- | test/regress/regress0/parser/Makefile | 8 | ||||
-rw-r--r-- | test/regress/regress0/parser/Makefile.am | 42 | ||||
-rw-r--r-- | test/regress/regress0/parser/declarefun-emptyset-uf.smt2 | 7 |
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) |