diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-04-09 15:43:37 -0500 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-04-09 15:59:38 -0500 |
| commit | 40fbc4aa1961cbeea2451251e54909285d2f4292 (patch) | |
| tree | ed4032bec587ef0e1ea0318a38c2d990e9f1f19f /src/parser | |
| parent | 8d29fef7286ab07c630c65284bfb399e2f7f5326 (diff) | |
Handle fmf.card as input from user, add support in SMT2 parser, as requested by Martin Brain. Fix two minor bugs : E-matching with datatypes, instantiation caching with incremental.
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index f030d6de0..659fc97d9 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1351,6 +1351,8 @@ builtinOp[CVC4::Kind& kind] | REOPT_TOK { $kind = CVC4::kind::REGEXP_OPT; } | RERANGE_TOK { $kind = CVC4::kind::REGEXP_RANGE; } | RELOOP_TOK { $kind = CVC4::kind::REGEXP_LOOP; } + + | FMFCARD_TOK { $kind = CVC4::kind::CARDINALITY_CONSTRAINT; } // NOTE: Theory operators go here ; @@ -1734,6 +1736,8 @@ RELOOP_TOK : 're.loop'; RENOSTR_TOK : 're.nostr'; REALLCHAR_TOK : 're.allchar'; +FMFCARD_TOK : 'fmf.card'; + EMPTYSET_TOK: 'emptyset'; // Other set theory operators are not // tokenized and handled directly when // processing a term |