Add is_singleton operator to the theory of sets (#5033)

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.

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