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 | |
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')
-rw-r--r-- | src/parser/parser.cpp | 4 | ||||
-rw-r--r-- | src/parser/parser.h | 1 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 10 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 18 |
4 files changed, 31 insertions, 2 deletions
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 1fdf5dda1..31ab49158 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -561,6 +561,10 @@ api::Term Parser::applyTypeAscription(api::Term t, api::Sort s) { t = d_solver->mkEmptySet(s); } + else if (k == api::EMPTYBAG) + { + t = d_solver->mkEmptyBag(s); + } else if (k == api::CONST_SEQUENCE) { if (!s.isSequence()) diff --git a/src/parser/parser.h b/src/parser/parser.h index 6f5d7fbe6..d478163b8 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -680,6 +680,7 @@ public: * Return term t with a type ascription applied to it. This is used for * syntax like (as t T) in smt2 and t::T in the CVC language. This includes: * - (as emptyset (Set T)) + * - (as emptybag (Bag T)) * - (as univset (Set T)) * - (as sep.nil T) * - (cons T) 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 "); } |