diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-05 18:44:47 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-05 18:44:56 -0500 |
| commit | c87ee73ad3d51c238700f236c18e425b80e8e7ac (patch) | |
| tree | aa4214b0fa7d6ef275605253fee88899fa3ce230 /src/parser | |
| parent | a2923ec61b601b0e3f4f78f22fffc1c2421f0d81 (diff) | |
Compute term indices lazily in TermDb. Optimization for qcf to recognize irrelevant quantifiers based on irrelevant functions. Fix rewriter for prefix merges. Minor optimizations for LFSC. Work on --literal-matching. Updates to inst propagate, move instantiation filtering within qe. Enable sygus for string inputs.
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 13 | ||||
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 2 |
2 files changed, 13 insertions, 2 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 38163c579..c28d23eac 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -760,7 +760,9 @@ sygusCommand returns [CVC4::Command* cmd = NULL] body = EXPR_MANAGER->mkExpr(kind::EXISTS, EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, PARSER_STATE->getSygusVars()), body); Debug("parser-sygus") << "...constructed exists " << body << std::endl; } - body = EXPR_MANAGER->mkExpr(kind::FORALL, EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, PARSER_STATE->getSygusFunSymbols()), body, sygusAttr); + if( !PARSER_STATE->getSygusFunSymbols().empty() ){ + body = EXPR_MANAGER->mkExpr(kind::FORALL, EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, PARSER_STATE->getSygusFunSymbols()), body, sygusAttr); + } Debug("parser-sygus") << "...constructed forall " << body << std::endl; Command* c = new SetUserAttributeCommand("sygus", sygusVar); c->setMuted(true); @@ -791,6 +793,7 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun] std::string sname; std::vector< Expr > let_vars; bool readingLet = false; + std::string s; } : LPAREN_TOK //read operator @@ -890,6 +893,12 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun] sgt.d_name = AntlrInput::tokenText($BINARY_LITERAL); sgt.d_gterm_type = SygusGTerm::gterm_op; } + | str[s,false] + { Debug("parser-sygus") << "Sygus grammar " << fun << " : string literal \"" << s << "\"" << std::endl; + sgt.d_expr = MK_CONST( ::CVC4::String(s) ); + sgt.d_name = s; + sgt.d_gterm_type = SygusGTerm::gterm_op; + } | symbol[name,CHECK_NONE,SYM_VARIABLE] ( SYGUS_ENUM_CONS_TOK symbol[name2,CHECK_NONE,SYM_VARIABLE] { readEnum = true; } )? { if( readEnum ){ name = name + "__Enum__" + name2; @@ -2773,7 +2782,7 @@ STRING_LITERAL_2_0 * will be part of the token text. Use the str[] parser rule instead. */ STRING_LITERAL_2_5 - : { PARSER_STATE->v2_5() }?=> + : { PARSER_STATE->v2_5() || PARSER_STATE->sygus() }?=> '"' (~('"') | '""')* '"' ; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index ebad90583..2da44152a 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -350,6 +350,8 @@ void Smt2::setLogic(std::string name) { name = "UFLIRA"; } else if(name == "BV") { name = "UFBV"; + } else if(name == "SLIA") { + name = "UFSLIA"; } else if(name == "ALL_SUPPORTED") { //no change } else { |