diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-24 16:58:18 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-24 16:58:18 +0200 |
| commit | 30920046fd6992b6e2c12c33ba888df5c1caf8de (patch) | |
| tree | 6cb732c7d7ffb14a9cd1cae2d7102abfb911243f /src/parser | |
| parent | ccd1638ac6b0eb93d62ca485c1f6d55966bdc056 (diff) | |
Counterexample-guided instantiation for datatypes. Make sygus parsing more liberal.
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index cfcc7df99..8dce0b639 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -366,7 +366,7 @@ command returns [CVC4::Command* cmd = NULL] { cmd = new GetAssignmentCommand(); } | /* assertion */ ASSERT_TOK { PARSER_STATE->checkThatLogicIsSet(); } - { if( PARSER_STATE->sygus() ){ PARSER_STATE->parseError("Sygus does not support assert command."); } } + /* { if( PARSER_STATE->sygus() ){ PARSER_STATE->parseError("Sygus does not support assert command."); } } */ { PARSER_STATE->clearLastNamedTerm(); } term[expr, expr2] { bool inUnsatCore = PARSER_STATE->lastNamedTerm().first == expr; @@ -1719,7 +1719,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] (term[expr, f2] | sortSymbol[type,CHECK_DECLARED] { readLetSort = true; } term[expr, f2] ) RPAREN_TOK // this is a parallel let, so we have to save up all the contributions // of the let and define them only later on - { if( readLetSort!=PARSER_STATE->sygus() ){ + { if( !PARSER_STATE->sygus() && readLetSort ){ PARSER_STATE->parseError("Bad syntax for let term."); }else if(names.count(name) == 1) { std::stringstream ss; |