diff options
author | mudathirmahgoub <mudathir-mahgoubyahia@uiowa.edu> | 2020-04-08 18:24:16 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-04-08 18:24:16 -0500 |
commit | df1ea6b9cdc1f424073151d0f7fda639d4405622 (patch) | |
tree | f28bd734c6f78e7399f91e92d517343a779c09c3 /src/theory/sets | |
parent | a48cafdd09c3ff8cb9984bad930343958c30ce56 (diff) |
Added CHOOSE operator for sets (#4211)
This PR enables THEORY_UF by default for sets and adds the operator CHOOSE for sets which returns an element from a given set. The semantics is as follows:
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.
Diffstat (limited to 'src/theory/sets')
-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 |
4 files changed, 96 insertions, 3 deletions
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) { |