diff options
| author | mudathirmahgoub <mudathirmahgoub@gmail.com> | 2020-09-22 16:59:41 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-22 16:59:41 -0500 |
| commit | e4a29a6033ecc7ba5ec266f37e8f151f09ead020 (patch) | |
| tree | 26dff55bd5121dc311185dcd3071a6e8751f9f5e /src/parser/smt2/Smt2.g | |
| parent | 524c879720779abc3bc529459da8734f2eb3e3ad (diff) | |
Add skeleton for theory of bags (multisets) (#5100)
This PR adds initial headers and mostly empty source files for the theory of bags (multisets).
It acts as a basis for future commits.
It includes straightforward implementation for typing rules an enumerator for bags.
Diffstat (limited to 'src/parser/smt2/Smt2.g')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 417ef5202..65f72eb28 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -2086,7 +2086,15 @@ sortSymbol[CVC4::api::Sort& t, CVC4::parser::DeclarationCheck check] PARSER_STATE->parseError("Illegal set type."); } t = SOLVER->mkSetSort( args[0] ); - } else if(name == "Seq" && !PARSER_STATE->strictModeEnabled() && + } + else if(name == "Bag" && + PARSER_STATE->isTheoryEnabled(theory::THEORY_BAGS) ) { + if(args.size() != 1) { + PARSER_STATE->parseError("Illegal bag type."); + } + t = SOLVER->mkBagSort( args[0] ); + } + else if(name == "Seq" && !PARSER_STATE->strictModeEnabled() && PARSER_STATE->isTheoryEnabled(theory::THEORY_STRINGS) ) { if(args.size() != 1) { PARSER_STATE->parseError("Illegal sequence type."); |