diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-10-08 20:18:07 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-10-08 20:18:30 -0400 |
| commit | 6a9f767abff6e6c81810cf134253399899a97424 (patch) | |
| tree | 0a6d991643e3b3a7596093458b929d44fc13d875 /src/parser/cvc | |
| parent | 7f885c4e79501827e70fe14683152af85c5f8bfd (diff) | |
Add unsat cores support to CVC native language.
Diffstat (limited to 'src/parser/cvc')
| -rw-r--r-- | src/parser/cvc/Cvc.g | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 151e2ecb6..85939dd22 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -65,6 +65,7 @@ tokens { EXIT_TOK = 'EXIT'; INCLUDE_TOK = 'INCLUDE'; DUMP_PROOF_TOK = 'DUMP_PROOF'; + DUMP_UNSAT_CORE_TOK = 'DUMP_UNSAT_CORE'; DUMP_ASSUMPTIONS_TOK = 'DUMP_ASSUMPTIONS'; DUMP_SIG_TOK = 'DUMP_SIG'; DUMP_TCC_TOK = 'DUMP_TCC'; @@ -795,6 +796,9 @@ mainCommand[CVC4::Command*& cmd] | DUMP_PROOF_TOK { cmd = new GetProofCommand(); } + | DUMP_UNSAT_CORE_TOK + { cmd = new GetUnsatCoreCommand(); } + | ( DUMP_ASSUMPTIONS_TOK | DUMP_SIG_TOK | DUMP_TCC_TOK |