diff options
| -rw-r--r-- | src/api/cvc4cpp.cpp | 2 | ||||
| -rw-r--r-- | src/api/cvc4cppkind.h | 8 | ||||
| -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 | 17 | ||||
| -rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 105 | ||||
| -rw-r--r-- | src/theory/sets/theory_sets_private.h | 12 | ||||
| -rw-r--r-- | src/theory/sets/theory_sets_rewriter.cpp | 23 | ||||
| -rw-r--r-- | src/theory/sets/theory_sets_type_rules.h | 121 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/sets/is_singleton1.smt2 | 9 |
11 files changed, 193 insertions, 110 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 5b3384439..f0dabc11b 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -253,6 +253,7 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{ {IDEN, CVC4::Kind::IDEN}, {COMPREHENSION, CVC4::Kind::COMPREHENSION}, {CHOOSE, CVC4::Kind::CHOOSE}, + {IS_SINGLETON, CVC4::Kind::IS_SINGLETON}, /* Strings ------------------------------------------------------------- */ {STRING_CONCAT, CVC4::Kind::STRING_CONCAT}, {STRING_IN_REGEXP, CVC4::Kind::STRING_IN_REGEXP}, @@ -542,6 +543,7 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction> {CVC4::Kind::IDEN, IDEN}, {CVC4::Kind::COMPREHENSION, COMPREHENSION}, {CVC4::Kind::CHOOSE, CHOOSE}, + {CVC4::Kind::IS_SINGLETON, IS_SINGLETON}, /* 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 48addc67a..f1f035460 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -1956,6 +1956,14 @@ enum CVC4_PUBLIC Kind : int32_t * mkTerm(Kind kind, Term child) */ CHOOSE, + /** + * Set is_singleton predicate. + * Parameters: 1 + * -[1]: Term of set sort, is [1] a singleton set? + * Create with: + * mkTerm(Kind kind, Term child) + */ + IS_SINGLETON, /* Strings --------------------------------------------------------------- */ diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index c4899c8a8..6d69a3388 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -684,6 +684,7 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) addOperator(api::CARD, "card"); addOperator(api::COMPLEMENT, "complement"); addOperator(api::CHOOSE, "choose"); + addOperator(api::IS_SINGLETON, "is_singleton"); 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 6c43c9eb1..960d17cdc 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -740,7 +740,8 @@ void Smt2Printer::toStream(std::ostream& out, case kind::SET_TYPE: case kind::SINGLETON: case kind::COMPLEMENT: - case kind::CHOOSE: out << smtKindString(k, d_variant) << " "; break; + case kind::CHOOSE: + case kind::IS_SINGLETON: out << smtKindString(k, d_variant) << " "; break; case kind::UNIVERSE_SET:out << "(as univset " << n.getType() << ")";break; // fp theory @@ -1145,6 +1146,7 @@ static string smtKindString(Kind k, Variant v) case kind::CARD: return "card"; case kind::COMPREHENSION: return "comprehension"; case kind::CHOOSE: return "choose"; + case kind::IS_SINGLETON: return "is_singleton"; 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 d3c42ef27..fd941ab29 100644 --- a/src/theory/sets/kinds +++ b/src/theory/sets/kinds @@ -67,6 +67,9 @@ operator COMPREHENSION 3 "set comprehension specified by a bound variable list, # 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" +# The operator is_singleton returns whether the given set is a singleton +operator IS_SINGLETON 1 "return whether the given set is a singleton" + operator JOIN 2 "set join" operator PRODUCT 2 "set cartesian product" operator TRANSPOSE 1 "set transpose" @@ -87,6 +90,7 @@ 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 IS_SINGLETON ::CVC4::theory::sets::IsSingletonTypeRule typerule JOIN ::CVC4::theory::sets::RelBinaryOperatorTypeRule typerule PRODUCT ::CVC4::theory::sets::RelBinaryOperatorTypeRule @@ -96,19 +100,6 @@ typerule JOIN_IMAGE ::CVC4::theory::sets::JoinImageTypeRule typerule IDEN ::CVC4::theory::sets::RelIdenTypeRule construle UNION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule -construle INTERSECTION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule -construle SETMINUS ::CVC4::theory::sets::SetsBinaryOperatorTypeRule 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 -construle TRANSPOSE ::CVC4::theory::sets::RelTransposeTypeRule -construle TCLOSURE ::CVC4::theory::sets::RelTransClosureTypeRule -construle JOIN_IMAGE ::CVC4::theory::sets::JoinImageTypeRule -construle IDEN ::CVC4::theory::sets::RelIdenTypeRule endtheory diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index a88374980..741f45dd8 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -1397,35 +1397,88 @@ TrustNode TheorySetsPrivate::expandDefinition(Node node) { Debug("sets-proc") << "expandDefinition : " << node << std::endl; - if (node.getKind() == kind::CHOOSE) + switch (node.getKind()) + { + case kind::CHOOSE: return expandChooseOperator(node); + case kind::IS_SINGLETON: return expandIsSingletonOperator(node); + default: return TrustNode::null(); + } +} + +TrustNode TheorySetsPrivate::expandChooseOperator(const Node& node) +{ + Assert(node.getKind() == CHOOSE); + + // we call the rewriter here to handle the pattern (choose (singleton x)) + // because the rewriter is called after expansion + Node rewritten = Rewriter::rewrite(node); + if (rewritten.getKind() != CHOOSE) + { + return TrustNode::mkTrustRewrite(node, rewritten, nullptr); + } + + // (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 = rewritten[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)); + Node isEmpty = set.eqNode(emptySet); + Node member = nm->mkNode(MEMBER, witnessVariable, set); + Node memberAndEqual = member.andNode(equal); + Node ite = nm->mkNode(ITE, isEmpty, equal, memberAndEqual); + Node witnessVariables = nm->mkNode(BOUND_VAR_LIST, witnessVariable); + Node witness = nm->mkNode(WITNESS, witnessVariables, ite); + return TrustNode::mkTrustRewrite(node, witness, nullptr); +} + +TrustNode TheorySetsPrivate::expandIsSingletonOperator(const Node& node) +{ + Assert(node.getKind() == IS_SINGLETON); + + // we call the rewriter here to handle the pattern + // (is_singleton (singleton x)) because the rewriter is called after expansion + Node rewritten = Rewriter::rewrite(node); + if (rewritten.getKind() != IS_SINGLETON) + { + return TrustNode::mkTrustRewrite(node, rewritten, nullptr); + } + + // (is_singleton A) is expanded as + // (exists ((x: T)) (= A (singleton x))) + // where T is the sort of elements of A + + NodeManager* nm = NodeManager::currentNM(); + Node set = rewritten[0]; + + std::map<Node, Node>::iterator it = d_isSingletonNodes.find(rewritten); + + if (it != d_isSingletonNodes.end()) { - // (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)); - 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(WITNESS, witnessVariables, ite); - return TrustNode::mkTrustRewrite(node, witness, nullptr); + return TrustNode::mkTrustRewrite(rewritten, it->second, nullptr); } - return TrustNode::null(); + TypeNode setType = set.getType(); + Node boundVar = nm->mkBoundVar(setType.getSetElementType()); + Node singleton = nm->mkNode(kind::SINGLETON, boundVar); + Node equal = set.eqNode(singleton); + std::vector<Node> variables = {boundVar}; + Node boundVars = nm->mkNode(BOUND_VAR_LIST, variables); + Node exists = nm->mkNode(kind::EXISTS, boundVars, equal); + d_isSingletonNodes[rewritten] = exists; + + return TrustNode::mkTrustRewrite(node, exists, nullptr); } Node TheorySetsPrivate::getChooseFunction(const TypeNode& setType) diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index 1c038e02f..71ad3781d 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -256,6 +256,10 @@ class TheorySetsPrivate { * given set type, or creates a new one if it does not exist. */ Node getChooseFunction(const TypeNode& setType); + /** expand the definition of the choose operator */ + TrustNode expandChooseOperator(const Node& node); + /** expand the definition of is_singleton operator */ + TrustNode expandIsSingletonOperator(const Node& node); /** subtheory solver for the theory of relations */ std::unique_ptr<TheorySetsRels> d_rels; /** subtheory solver for the theory of sets with cardinality */ @@ -276,10 +280,12 @@ class TheorySetsPrivate { /** The theory rewriter for this theory. */ TheorySetsRewriter d_rewriter; - /* - * a map that stores the choose functions for set types - */ + /** a map that stores the choose functions for set types */ std::map<TypeNode, Node> d_chooseFunctions; + + /** a map that maps each set to an existential quantifier generated for + * operator is_singleton */ + std::map<Node, Node> d_isSingletonNodes; };/* class TheorySetsPrivate */ diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index a7fbc8a38..eb168c6ed 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -240,6 +240,29 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { } break; } + + case kind::CHOOSE: + { + if (node[0].getKind() == SINGLETON) + { + //(= (choose (singleton x)) x) is a tautology + // we return x for (choose (singleton x)) + return RewriteResponse(REWRITE_AGAIN, node[0][0]); + } + break; + } // kind::CHOOSE + case kind::IS_SINGLETON: + { + if (node[0].getKind() == SINGLETON) + { + //(= (is_singleton (singleton x)) is a tautology + // we return true for (is_singleton (singleton x)) + return RewriteResponse(REWRITE_AGAIN, + NodeManager::currentNM()->mkConst(true)); + } + break; + } // kind::IS_SINGLETON + case kind::TRANSPOSE: { if(node[0].getKind() == kind::TRANSPOSE) { return RewriteResponse(REWRITE_AGAIN, node[0][0]); diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h index 5d01a966a..42fc583b8 100644 --- a/src/theory/sets/theory_sets_type_rules.h +++ b/src/theory/sets/theory_sets_type_rules.h @@ -25,42 +25,53 @@ namespace CVC4 { namespace theory { namespace sets { -struct SetsBinaryOperatorTypeRule { - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) +struct SetsBinaryOperatorTypeRule +{ + inline static TypeNode computeType(NodeManager* nodeManager, + TNode n, + bool check) { - Assert(n.getKind() == kind::UNION || n.getKind() == kind::INTERSECTION - || n.getKind() == kind::SETMINUS); + Assert(n.getKind() == kind::UNION || + n.getKind() == kind::INTERSECTION || + n.getKind() == kind::SETMINUS); TypeNode setType = n[0].getType(check); - if( check ) { - if(!setType.isSet()) { - throw TypeCheckingExceptionPrivate(n, "operator expects a set, first argument is not"); + if (check) + { + if (!setType.isSet()) + { + throw TypeCheckingExceptionPrivate( + n, "operator expects a set, first argument is not"); } TypeNode secondSetType = n[1].getType(check); - if(secondSetType != setType) { - if( n.getKind() == kind::INTERSECTION ){ - setType = TypeNode::mostCommonTypeNode( secondSetType, setType ); - }else{ - setType = TypeNode::leastCommonTypeNode( secondSetType, setType ); + if (secondSetType != setType) + { + if (n.getKind() == kind::INTERSECTION) + { + setType = TypeNode::mostCommonTypeNode(secondSetType, setType); + } + else + { + setType = TypeNode::leastCommonTypeNode(secondSetType, setType); } - if( setType.isNull() ){ - throw TypeCheckingExceptionPrivate(n, "operator expects two sets of comparable types"); + if (setType.isNull()) + { + throw TypeCheckingExceptionPrivate( + n, "operator expects two sets of comparable types"); } - } } return setType; } - inline static bool computeIsConst(NodeManager* nodeManager, TNode n) { - Assert(n.getKind() == kind::UNION || n.getKind() == kind::INTERSECTION - || n.getKind() == kind::SETMINUS); - if(n.getKind() == kind::UNION) { - return NormalForm::checkNormalConstant(n); - } else { - return false; - } + inline static bool computeIsConst(NodeManager* nodeManager, TNode n) + { + // only UNION has a const rule in kinds. + // INTERSECTION and SETMINUS are not used in the canonical representation of + // sets and therefore they do not have const rules in kinds + Assert(n.getKind() == kind::UNION); + return NormalForm::checkNormalConstant(n); } -};/* struct SetUnionTypeRule */ +}; /* struct SetsBinaryOperatorTypeRule */ struct SubsetTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) @@ -155,11 +166,6 @@ struct CardTypeRule { } return nodeManager->integerType(); } - - inline static bool computeIsConst(NodeManager* nodeManager, TNode n) { - Assert(n.getKind() == kind::CARD); - return false; - } };/* struct CardTypeRule */ struct ComplementTypeRule { @@ -174,11 +180,6 @@ struct ComplementTypeRule { } return setType; } - - inline static bool computeIsConst(NodeManager* nodeManager, TNode n) { - Assert(n.getKind() == kind::COMPLEMENT); - return false; - } };/* struct ComplementTypeRule */ struct UniverseSetTypeRule { @@ -235,13 +236,27 @@ struct ChooseTypeRule } return setType.getSetElementType(); } - inline static bool computeIsConst(NodeManager* nodeManager, TNode n) +}; /* struct ChooseTypeRule */ + +struct IsSingletonTypeRule +{ + inline static TypeNode computeType(NodeManager* nodeManager, + TNode n, + bool check) { - Assert(n.getKind() == kind::CHOOSE); - // choose nodes should be expanded - return false; + Assert(n.getKind() == kind::IS_SINGLETON); + TypeNode setType = n[0].getType(check); + if (check) + { + if (!setType.isSet()) + { + throw TypeCheckingExceptionPrivate( + n, "IS_SINGLETON operator expects a set, a non-set is found"); + } + } + return nodeManager->booleanType(); } -}; /* struct ChooseTypeRule */ +}; /* struct IsSingletonTypeRule */ struct InsertTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) @@ -264,11 +279,6 @@ struct InsertTypeRule { } return setType; } - - inline static bool computeIsConst(NodeManager* nodeManager, TNode n) { - Assert(n.getKind() == kind::INSERT); - return false; - } };/* struct InsertTypeRule */ struct RelBinaryOperatorTypeRule { @@ -308,11 +318,6 @@ struct RelBinaryOperatorTypeRule { return resultType; } - - inline static bool computeIsConst(NodeManager* nodeManager, TNode n) { - Assert(n.getKind() == kind::JOIN || n.getKind() == kind::PRODUCT); - return false; - } };/* struct RelBinaryOperatorTypeRule */ struct RelTransposeTypeRule { @@ -327,10 +332,6 @@ struct RelTransposeTypeRule { std::reverse(tupleTypes.begin(), tupleTypes.end()); return nodeManager->mkSetType(nodeManager->mkTupleType(tupleTypes)); } - - inline static bool computeIsConst(NodeManager* nodeManager, TNode n) { - return false; - } };/* struct RelTransposeTypeRule */ struct RelTransClosureTypeRule { @@ -352,11 +353,6 @@ struct RelTransClosureTypeRule { } return setType; } - - inline static bool computeIsConst(NodeManager* nodeManager, TNode n) { - Assert(n.getKind() == kind::TCLOSURE); - return false; - } };/* struct RelTransClosureTypeRule */ struct JoinImageTypeRule { @@ -399,11 +395,6 @@ struct JoinImageTypeRule { newTupleTypes.push_back(tupleTypes[0]); return nodeManager->mkSetType(nodeManager->mkTupleType(newTupleTypes)); } - - inline static bool computeIsConst(NodeManager* nodeManager, TNode n) { - Assert(n.getKind() == kind::JOIN_IMAGE); - return false; - } };/* struct JoinImageTypeRule */ struct RelIdenTypeRule { @@ -423,10 +414,6 @@ struct RelIdenTypeRule { tupleTypes.push_back(tupleTypes[0]); return nodeManager->mkSetType(nodeManager->mkTupleType(tupleTypes)); } - - inline static bool computeIsConst(NodeManager* nodeManager, TNode n) { - return false; - } };/* struct RelIdenTypeRule */ struct SetsProperties { diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index b92f767b2..e06abc0a5 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1762,6 +1762,7 @@ set(regress_1_tests regress1/sets/infinite-type/sets-card-int-1.smt2 regress1/sets/infinite-type/sets-card-int-2.smt2 regress1/sets/insert_invariant_37_2.smt2 + regress1/sets/is_singleton1.smt2 regress1/sets/issue2568.smt2 regress1/sets/issue2904.smt2 regress1/sets/issue4391-card-lasso.smt2 diff --git a/test/regress/regress1/sets/is_singleton1.smt2 b/test/regress/regress1/sets/is_singleton1.smt2 new file mode 100644 index 000000000..01b633d8e --- /dev/null +++ b/test/regress/regress1/sets/is_singleton1.smt2 @@ -0,0 +1,9 @@ +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(declare-fun S () (Set Int)) +(declare-fun x () Int) +(assert (= (choose (singleton x)) 5)) +(assert (= (singleton x) S)) +(assert (is_singleton S)) +(assert (is_singleton (singleton 3))) +(check-sat)
\ No newline at end of file |