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 | |
| 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')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 10 | ||||
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 18 |
2 files changed, 26 insertions, 2 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."); diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 73d4c8c52..387117335 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -691,6 +691,21 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) addOperator(api::TCLOSURE, "tclosure"); } + if (d_logic.isTheoryEnabled(theory::THEORY_BAGS)) + { + defineVar("emptybag", d_solver->mkEmptyBag(d_solver->getNullSort())); + addOperator(api::UNION_MAX, "union_max"); + addOperator(api::UNION_DISJOINT, "union_disjoint"); + addOperator(api::INTERSECTION_MIN, "intersection_min"); + addOperator(api::DIFFERENCE_SUBTRACT, "difference_subtract"); + addOperator(api::DIFFERENCE_REMOVE, "difference_remove"); + addOperator(api::BAG_IS_INCLUDED, "bag.is_included"); + addOperator(api::BAG_COUNT, "bag.count"); + addOperator(api::MK_BAG, "mkBag"); + addOperator(api::BAG_CARD, "bag.card"); + addOperator(api::BAG_CHOOSE, "bag.choose"); + addOperator(api::BAG_IS_SINGLETON, "bag.is_singleton"); + } if(d_logic.isTheoryEnabled(theory::THEORY_STRINGS)) { defineType("String", d_solver->getStringSort()); defineType("RegLan", d_solver->getRegExpSort()); @@ -821,7 +836,8 @@ void Smt2::checkLogicAllowsFreeSorts() if (!d_logic.isTheoryEnabled(theory::THEORY_UF) && !d_logic.isTheoryEnabled(theory::THEORY_ARRAYS) && !d_logic.isTheoryEnabled(theory::THEORY_DATATYPES) - && !d_logic.isTheoryEnabled(theory::THEORY_SETS)) + && !d_logic.isTheoryEnabled(theory::THEORY_SETS) + && !d_logic.isTheoryEnabled(theory::THEORY_BAGS)) { parseErrorLogic("Free sort symbols not allowed in "); } |