diff options
| -rw-r--r-- | src/api/cvc4cpp.cpp | 2 | ||||
| -rw-r--r-- | src/api/cvc4cppkind.h | 12 | ||||
| -rw-r--r-- | src/parser/cvc/Cvc.g | 10 | ||||
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 1 | ||||
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 4 | ||||
| -rw-r--r-- | src/theory/sets/kinds | 8 | ||||
| -rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 54 | ||||
| -rw-r--r-- | src/theory/sets/theory_sets_private.h | 11 | ||||
| -rw-r--r-- | src/theory/sets/theory_sets_type_rules.h | 26 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 5 | ||||
| -rw-r--r-- | test/regress/regress1/fmf/agree466.smt2 | 2 | ||||
| -rw-r--r-- | test/regress/regress1/fmf/agree467.smt2 | 2 | ||||
| -rw-r--r-- | test/regress/regress1/sets/choose.cvc | 11 | ||||
| -rw-r--r-- | test/regress/regress1/sets/choose1.smt2 | 11 | ||||
| -rw-r--r-- | test/regress/regress1/sets/choose2.smt2 | 6 | ||||
| -rw-r--r-- | test/regress/regress1/sets/choose3.smt2 | 7 | ||||
| -rw-r--r-- | test/regress/regress1/sets/choose4.smt2 | 13 |
17 files changed, 178 insertions, 7 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 8d6de0ade..ea5eca391 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -245,6 +245,7 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{ {JOIN_IMAGE, CVC4::Kind::JOIN_IMAGE}, {IDEN, CVC4::Kind::IDEN}, {COMPREHENSION, CVC4::Kind::COMPREHENSION}, + {CHOOSE, CVC4::Kind::CHOOSE}, /* Strings ------------------------------------------------------------- */ {STRING_CONCAT, CVC4::Kind::STRING_CONCAT}, {STRING_IN_REGEXP, CVC4::Kind::STRING_IN_REGEXP}, @@ -513,6 +514,7 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction> {CVC4::Kind::JOIN_IMAGE, JOIN_IMAGE}, {CVC4::Kind::IDEN, IDEN}, {CVC4::Kind::COMPREHENSION, COMPREHENSION}, + {CVC4::Kind::CHOOSE, CHOOSE}, /* Strings --------------------------------------------------------- */ {CVC4::Kind::STRING_CONCAT, STRING_CONCAT}, {CVC4::Kind::STRING_IN_REGEXP, STRING_IN_REGEXP}, diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h index f8e1fb90c..6c1a2256b 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -1852,6 +1852,18 @@ enum CVC4_PUBLIC Kind : int32_t * mkTerm(Kind kind, const std::vector<Term>& children) */ COMPREHENSION, + /** + * Returns an element from a given set. + * If a set A = {x}, then the term (choose A) is equivalent to the term x. + * If the set is empty, then (choose A) is an arbitrary value. + * If the set has cardinality > 1, then (choose A) will deterministically + * return an element in A. + * Parameters: 1 + * -[1]: Term of set sort + * Create with: + * mkTerm(Kind kind, Term child) + */ + CHOOSE, /* Strings --------------------------------------------------------------- */ diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 32604d03f..3f03ca43d 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -205,6 +205,9 @@ tokens { BVSLE_TOK = 'BVSLE'; BVSGE_TOK = 'BVSGE'; + // Sets + SETS_CHOOSE_TOK = 'CHOOSE'; + // Relations JOIN_TOK = 'JOIN'; TRANSPOSE_TOK = 'TRANSPOSE'; @@ -327,7 +330,8 @@ int getOperatorPrecedence(int type) { case PRODUCT_TOK: case IDEN_TOK: case JOIN_IMAGE_TOK: - case TRANSCLOSURE_TOK: return 24; + case TRANSCLOSURE_TOK: + case SETS_CHOOSE_TOK: return 24; case LEQ_TOK: case LT_TOK: case GEQ_TOK: @@ -367,10 +371,12 @@ api::Kind getOperatorKind(int type, bool& negate) { case XOR_TOK: return api::XOR; case AND_TOK: return api::AND; + case SETS_CHOOSE_TOK: return api::CHOOSE; case PRODUCT_TOK: return api::PRODUCT; case JOIN_TOK: return api::JOIN; case JOIN_IMAGE_TOK: return api::JOIN_IMAGE; + // comparisonBinop case EQUAL_TOK: return api::EQUAL; case DISEQUAL_TOK: negate = true; return api::EQUAL; @@ -2097,6 +2103,8 @@ setsTerm[CVC4::api::Term& f] /* Sets prefix operators */ : SETS_CARD_TOK LPAREN formula[f] RPAREN { f = MK_TERM(CVC4::api::CARD, f); } + | SETS_CHOOSE_TOK LPAREN formula[f] RPAREN + { f = MK_TERM(CVC4::api::CHOOSE, f); } | simpleTerm[f] ; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 3233ee7e8..2405b3402 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -670,6 +670,7 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) addOperator(api::INSERT, "insert"); addOperator(api::CARD, "card"); addOperator(api::COMPLEMENT, "complement"); + addOperator(api::CHOOSE, "choose"); addOperator(api::JOIN, "join"); addOperator(api::PRODUCT, "product"); addOperator(api::TRANSPOSE, "transpose"); diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index b5e137b4d..4013cbd08 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -741,7 +741,8 @@ void Smt2Printer::toStream(std::ostream& out, case kind::INSERT: case kind::SET_TYPE: case kind::SINGLETON: - case kind::COMPLEMENT: out << smtKindString(k, d_variant) << " "; break; + case kind::COMPLEMENT: + case kind::CHOOSE: out << smtKindString(k, d_variant) << " "; break; case kind::UNIVERSE_SET:out << "(as univset " << n.getType() << ")";break; // fp theory @@ -1134,6 +1135,7 @@ static string smtKindString(Kind k, Variant v) case kind::COMPLEMENT: return "complement"; case kind::CARD: return "card"; case kind::COMPREHENSION: return "comprehension"; + case kind::CHOOSE: return "choose"; case kind::JOIN: return "join"; case kind::PRODUCT: return "product"; case kind::TRANSPOSE: return "transpose"; diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds index 058a20aeb..452acfea0 100644 --- a/src/theory/sets/kinds +++ b/src/theory/sets/kinds @@ -61,6 +61,12 @@ nullaryoperator UNIVERSE_SET "(finite) universe set, all set variables must be i # finite sets with quantified formulas. operator COMPREHENSION 3 "set comprehension specified by a bound variable list, a predicate, and a term." +# The operator choose returns an element from a given set. +# If set A = {x}, then the term (choose A) is equivalent to the term x. +# If the set is empty, then (choose A) is an arbitrary value. +# If the set has cardinality > 1, then (choose A) will deterministically return an element in A. +operator CHOOSE 1 "return an element in the set given as a parameter" + operator JOIN 2 "set join" operator PRODUCT 2 "set cartesian product" operator TRANSPOSE 1 "set transpose" @@ -80,6 +86,7 @@ typerule CARD ::CVC4::theory::sets::CardTypeRule typerule COMPLEMENT ::CVC4::theory::sets::ComplementTypeRule typerule UNIVERSE_SET ::CVC4::theory::sets::UniverseSetTypeRule typerule COMPREHENSION ::CVC4::theory::sets::ComprehensionTypeRule +typerule CHOOSE ::CVC4::theory::sets::ChooseTypeRule typerule JOIN ::CVC4::theory::sets::RelBinaryOperatorTypeRule typerule PRODUCT ::CVC4::theory::sets::RelBinaryOperatorTypeRule @@ -95,6 +102,7 @@ construle SINGLETON ::CVC4::theory::sets::SingletonTypeRule construle INSERT ::CVC4::theory::sets::InsertTypeRule construle CARD ::CVC4::theory::sets::CardTypeRule construle COMPLEMENT ::CVC4::theory::sets::ComplementTypeRule +construle CHOOSE ::CVC4::theory::sets::ChooseTypeRule construle JOIN ::CVC4::theory::sets::RelBinaryOperatorTypeRule construle PRODUCT ::CVC4::theory::sets::RelBinaryOperatorTypeRule diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index e3db6887b..30bb4bad0 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -1485,10 +1485,58 @@ void TheorySetsPrivate::preRegisterTerm(TNode node) } } -Node TheorySetsPrivate::expandDefinition(Node n) +Node TheorySetsPrivate::expandDefinition(Node node) { - Debug("sets-proc") << "expandDefinition : " << n << std::endl; - return n; + Debug("sets-proc") << "expandDefinition : " << node << std::endl; + + if (node.getKind() == kind::CHOOSE) + { + // (choose A) is expanded as + // (witness ((x elementType)) + // (ite + // (= A (as emptyset setType)) + // (= x chooseUf(A)) + // (and (member x A) (= x chooseUf(A))) + + NodeManager* nm = NodeManager::currentNM(); + Node set = node[0]; + TypeNode setType = set.getType(); + Node chooseSkolem = getChooseFunction(setType); + Node apply = NodeManager::currentNM()->mkNode(APPLY_UF, chooseSkolem, set); + + Node witnessVariable = nm->mkBoundVar(setType.getSetElementType()); + + Node equal = witnessVariable.eqNode(apply); + Node emptySet = nm->mkConst(EmptySet(setType.toType())); + Node isEmpty = set.eqNode(emptySet); + Node member = nm->mkNode(MEMBER, witnessVariable, set); + Node memberAndEqual = member.andNode(equal); + Node ite = nm->mkNode(kind::ITE, isEmpty, equal, memberAndEqual); + Node witnessVariables = nm->mkNode(BOUND_VAR_LIST, witnessVariable); + Node witness = nm->mkNode(CHOICE, witnessVariables, ite); + return witness; + } + + return node; +} + +Node TheorySetsPrivate::getChooseFunction(const TypeNode& setType) +{ + std::map<TypeNode, Node>::iterator it = d_chooseFunctions.find(setType); + if (it != d_chooseFunctions.end()) + { + return it->second; + } + + NodeManager* nm = NodeManager::currentNM(); + TypeNode chooseUf = nm->mkFunctionType(setType, setType.getSetElementType()); + stringstream stream; + stream << "chooseUf" << setType.getId(); + string name = stream.str(); + Node chooseSkolem = nm->mkSkolem( + name, chooseUf, "choose function", NodeManager::SKOLEM_EXACT_NAME); + d_chooseFunctions[setType] = chooseSkolem; + return chooseSkolem; } Theory::PPAssertStatus TheorySetsPrivate::ppAssert( diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index 84cea99a1..a7e6f69ee 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -262,6 +262,12 @@ class TheorySetsPrivate { bool isMember(Node x, Node s); private: + /** get choose function + * + * Returns the existing uninterpreted function for the choose operator for the + * given set type, or creates a new one if it does not exist. + */ + Node getChooseFunction(const TypeNode& setType); /** The state of the sets solver at full effort */ SolverState d_state; /** The inference manager of the sets solver */ @@ -285,6 +291,11 @@ class TheorySetsPrivate { /** The theory rewriter for this theory. */ TheorySetsRewriter d_rewriter; + + /* + * a map that stores the choose functions for set types + */ + std::map<TypeNode, Node> d_chooseFunctions; };/* class TheorySetsPrivate */ diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h index 430163121..9d2dd882f 100644 --- a/src/theory/sets/theory_sets_type_rules.h +++ b/src/theory/sets/theory_sets_type_rules.h @@ -218,6 +218,32 @@ struct ComprehensionTypeRule } }; /* struct ComprehensionTypeRule */ +struct ChooseTypeRule +{ + inline static TypeNode computeType(NodeManager* nodeManager, + TNode n, + bool check) + { + Assert(n.getKind() == kind::CHOOSE); + TypeNode setType = n[0].getType(check); + if (check) + { + if (!setType.isSet()) + { + throw TypeCheckingExceptionPrivate( + n, "CHOOSE operator expects a set, a non-set is found"); + } + } + return setType.getSetElementType(); + } + inline static bool computeIsConst(NodeManager* nodeManager, TNode n) + { + Assert(n.getKind() == kind::CHOOSE); + // choose nodes should be expanded + return false; + } +}; /* struct ChooseTypeRule */ + struct InsertTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 649178f91..c5dbd38f8 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1644,6 +1644,11 @@ set(regress_1_tests regress1/sep/wand-simp-sat.smt2 regress1/sep/wand-simp-sat2.smt2 regress1/sep/wand-simp-unsat.smt2 + regress1/sets/choose.cvc + regress1/sets/choose1.smt2 + regress1/sets/choose2.smt2 + regress1/sets/choose3.smt2 + regress1/sets/choose4.smt2 regress1/sets/ListElem.hs.fqout.cvc4.38.smt2 regress1/sets/ListElts.hs.fqout.cvc4.317.smt2 regress1/sets/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 diff --git a/test/regress/regress1/fmf/agree466.smt2 b/test/regress/regress1/fmf/agree466.smt2 index d17a663c6..bfbc50c9d 100644 --- a/test/regress/regress1/fmf/agree466.smt2 +++ b/test/regress/regress1/fmf/agree466.smt2 @@ -1,7 +1,7 @@ ; COMMAND-LINE: --finite-model-find --lang=smt2.5 ; EXPECT: sat ; Preamble -------------- -(set-logic ALL_SUPPORTED) +(set-logic AUFDTLIA) (set-info :status sat) (declare-datatypes () ((UNIT (Unit)))) (declare-datatypes () ((BOOL (Truth) (Falsity)))) diff --git a/test/regress/regress1/fmf/agree467.smt2 b/test/regress/regress1/fmf/agree467.smt2 index 07180cf4f..b2ac3364e 100644 --- a/test/regress/regress1/fmf/agree467.smt2 +++ b/test/regress/regress1/fmf/agree467.smt2 @@ -1,7 +1,7 @@ ; COMMAND-LINE: --finite-model-find --lang=smt2.5 ; EXPECT: unsat ; Preamble -------------- -(set-logic ALL_SUPPORTED) +(set-logic AUFDTLIA) (set-info :status unsat) (declare-datatypes () ((UNIT (Unit)))) (declare-datatypes () ((BOOL (Truth) (Falsity)))) diff --git a/test/regress/regress1/sets/choose.cvc b/test/regress/regress1/sets/choose.cvc new file mode 100644 index 000000000..2112e702b --- /dev/null +++ b/test/regress/regress1/sets/choose.cvc @@ -0,0 +1,11 @@ +% COMMAND-LINE: --no-check-models +% EXPECT: sat + +A : SET OF INT; +a : INT; + +ASSERT NOT (A = {} :: SET OF INT); +ASSERT CHOOSE (A) = 10; +ASSERT CHOOSE (A) = a; + +CHECKSAT; diff --git a/test/regress/regress1/sets/choose1.smt2 b/test/regress/regress1/sets/choose1.smt2 new file mode 100644 index 000000000..420a0fde0 --- /dev/null +++ b/test/regress/regress1/sets/choose1.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --no-check-models +(set-logic ALL) +(set-info :status sat) +(set-option :produce-models true) +(declare-fun A () (Set Int)) +(declare-fun a () Int) +(assert (not (= A (as emptyset (Set Int))))) +(assert (= (choose A) 10)) +(assert (= a (choose A))) +(assert (exists ((x Int)) (and (= x (choose A)) (= x a)))) +(check-sat) diff --git a/test/regress/regress1/sets/choose2.smt2 b/test/regress/regress1/sets/choose2.smt2 new file mode 100644 index 000000000..85a5d18d3 --- /dev/null +++ b/test/regress/regress1/sets/choose2.smt2 @@ -0,0 +1,6 @@ +(set-logic ALL) +(set-info :status unsat) +(set-option :produce-models true) +(declare-fun A () (Set Int)) +(assert (distinct (choose A) (choose A))) +(check-sat)
\ No newline at end of file diff --git a/test/regress/regress1/sets/choose3.smt2 b/test/regress/regress1/sets/choose3.smt2 new file mode 100644 index 000000000..744192496 --- /dev/null +++ b/test/regress/regress1/sets/choose3.smt2 @@ -0,0 +1,7 @@ +(set-logic ALL) +(set-info :status sat) +(set-option :produce-models true) +(declare-fun A () (Set Int)) +(assert (= (choose A) 10)) +(assert (= A (as emptyset (Set Int)))) +(check-sat)
\ No newline at end of file diff --git a/test/regress/regress1/sets/choose4.smt2 b/test/regress/regress1/sets/choose4.smt2 new file mode 100644 index 000000000..df7c510d3 --- /dev/null +++ b/test/regress/regress1/sets/choose4.smt2 @@ -0,0 +1,13 @@ +; COMMAND-LINE: --no-check-models +(set-logic ALL) +(set-info :status sat) +(set-option :produce-models true) +(declare-fun A () (Set Int)) +(declare-fun a () Int) +(assert (not (= A (as emptyset (Set Int))))) +(assert (member 10 A)) +; this line raises an assertion error +(assert (= a (choose A))) +; this line raises an assertion error +;(assert (exists ((x Int)) (and (= x (choose A)) (= x a)))) +(check-sat)
\ No newline at end of file |