diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-10-10 22:15:38 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-10-10 22:15:38 +0000 |
commit | d6b37239a2e525e7878d3bb0b4372a8dabc340a9 (patch) | |
tree | 3db6b54c8b5873db1e6c91b1577d431d74632c66 /src/parser | |
parent | 7a059452ebf5729723f610da9258a47007e38253 (diff) |
additional model gen and SMT-LIBv2 compliance work: (get-assignment) now supported; work on Result type (biggest noticeable change is that CVC4 now outputs lowercase "sat" and "unsat"), Options class moved to src/smt, to allow for future work on runtime configuration via (set-option) command
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/smt2/Smt2.g | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index ddfd1804e..f549d2148 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -248,6 +248,9 @@ command returns [CVC4::Command* cmd] $cmd = seq; } } + | /* get-assignment */ + GET_ASSIGNMENT_TOK + { cmd = new GetAssignmentCommand; } | /* assertion */ ASSERT_TOK term[expr] { cmd = new AssertCommand(expr); } @@ -400,7 +403,7 @@ term[CVC4::Expr& expr] Expr func = PARSER_STATE->mkFunction(name, expr.getType()); // bind name to expr with define-fun Command* c = - new DefineFunctionCommand(func, std::vector<Expr>(), expr); + new DefineNamedFunctionCommand(func, std::vector<Expr>(), expr); PARSER_STATE->preemptCommand(c); } else { std::stringstream ss; @@ -585,6 +588,7 @@ DECLARE_SORT_TOK : 'declare-sort'; DEFINE_FUN_TOK : 'define-fun'; DEFINE_SORT_TOK : 'define-sort'; GET_VALUE_TOK : 'get-value'; +GET_ASSIGNMENT_TOK : 'get-assignment'; GET_ASSERTIONS_TOK : 'get-assertions'; EXIT_TOK : 'exit'; ITE_TOK : 'ite'; |