This pull request adds a new operator is_singleton for sets to determine whether a set is a singleton.
Before this operator, the user either uses an existential quantifier or the cardinality operator in smtlib. The former affects the performance especially when polarity is negative. The latter requires the cardinality extension in sets theory.
The implementation of is_singleton only uses an internal existential quantifier with the hope of optimizing it later.
New rewriting rules:
(is_singleton (singleton x)) is rewritten as true.
(is_singleton A) is rewritten as (= A (singleton x)) where x is a fresh skolem of the same type of elements of A.
(choose (singleton x)) is rewritten as x.
{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},
{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},
* 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 --------------------------------------------------------------- */
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");
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
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";
# 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"
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
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
{
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)
* 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 */
/** 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 */
}
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]);
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)
}
return nodeManager->integerType();
}
-
- inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
- Assert(n.getKind() == kind::CARD);
- return false;
- }
};/* struct CardTypeRule */
struct ComplementTypeRule {
}
return setType;
}
-
- inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
- Assert(n.getKind() == kind::COMPLEMENT);
- return false;
- }
};/* struct ComplementTypeRule */
struct UniverseSetTypeRule {
}
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)
}
return setType;
}
-
- inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
- Assert(n.getKind() == kind::INSERT);
- return false;
- }
};/* struct InsertTypeRule */
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 {
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 {
}
return setType;
}
-
- inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
- Assert(n.getKind() == kind::TCLOSURE);
- return false;
- }
};/* struct RelTransClosureTypeRule */
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 {
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 {
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
--- /dev/null
+(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
projects / cvc5.git / commitdiff