diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-08-25 18:40:06 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-08-26 15:20:32 -0400 |
| commit | 525e7328cad1ac8afbc60ed8103e06665cf5b163 (patch) | |
| tree | 61d8f46addfa6e76b233b234025df9bf54f7aea1 /src/parser/smt2/Smt2.g | |
| parent | 34a27e2fef540ee3d90c43f771397e0e9ce3fef9 (diff) | |
Improved SMT-LIBv2 language support for unsat cores.
Diffstat (limited to 'src/parser/smt2/Smt2.g')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 16 |
1 files changed, 12 insertions, 4 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index e1547d23d..2adad092e 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -377,9 +377,13 @@ command returns [CVC4::Command* cmd = NULL] { cmd = new GetAssignmentCommand(); } | /* assertion */ ASSERT_TOK { PARSER_STATE->checkThatLogicIsSet(); } + { PARSER_STATE->clearLastNamedTerm(); } term[expr, expr2] - { cmd = new AssertCommand(expr, /* inUnsatCore */ PARSER_STATE->lastNamedTerm() == expr); - PARSER_STATE->setLastNamedTerm(Expr()); + { bool inUnsatCore = PARSER_STATE->lastNamedTerm().first == expr; + cmd = new AssertCommand(expr, inUnsatCore); + if(inUnsatCore) { + PARSER_STATE->registerUnsatCoreName(PARSER_STATE->lastNamedTerm()); + } } | /* check-sat */ CHECKSAT_TOK { PARSER_STATE->checkThatLogicIsSet(); } @@ -398,7 +402,7 @@ command returns [CVC4::Command* cmd = NULL] { cmd = new GetProofCommand(); } | /* get-unsat-core */ GET_UNSAT_CORE_TOK { PARSER_STATE->checkThatLogicIsSet(); } - { cmd = new GetUnsatCoreCommand(); } + { cmd = new GetUnsatCoreCommand(PARSER_STATE->getUnsatCoreNames()); } | /* push */ PUSH_TOK { PARSER_STATE->checkThatLogicIsSet(); } ( k=INTEGER_LITERAL @@ -407,11 +411,13 @@ command returns [CVC4::Command* cmd = NULL] cmd = new EmptyCommand(); } else if(n == 1) { PARSER_STATE->pushScope(); + PARSER_STATE->pushUnsatCoreNameScope(); cmd = new PushCommand(); } else { CommandSequence* seq = new CommandSequence(); do { PARSER_STATE->pushScope(); + PARSER_STATE->pushUnsatCoreNameScope(); Command* c = new PushCommand(); c->setMuted(n > 1); seq->addCommand(c); @@ -434,11 +440,13 @@ command returns [CVC4::Command* cmd = NULL] if(n == 0) { cmd = new EmptyCommand(); } else if(n == 1) { + PARSER_STATE->popUnsatCoreNameScope(); PARSER_STATE->popScope(); cmd = new PopCommand(); } else { CommandSequence* seq = new CommandSequence(); do { + PARSER_STATE->popUnsatCoreNameScope(); PARSER_STATE->popScope(); Command* c = new PopCommand(); c->setMuted(n > 1); @@ -1213,7 +1221,7 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr] // define it Expr func = PARSER_STATE->mkFunction(name, expr.getType()); // remember the last term to have been given a :named attribute - PARSER_STATE->setLastNamedTerm(expr); + PARSER_STATE->setLastNamedTerm(expr, name); // bind name to expr with define-fun Command* c = new DefineNamedFunctionCommand(name, func, std::vector<Expr>(), expr); |