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.

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 8d6de0ade76596985f0f156154c96182bafe30a3..ea5eca391e228d67eb4f052ec1bfdc66e8136af8 100644 (file)
--- 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 f8e1fb90ce3b645b4addcfec1bb613fbdef0de5c..6c1a2256b921e45c056d8ac948e7b6bd89c93441 100644 (file)
--- 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 32604d03f3758b4b896b118fea8c5aa0160a2bac..3f03ca43db38949e26a312e6612226c5c3beda17 100644 (file)
--- 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 3233ee7e849d5b56c19201d4f62af96a74c92545..2405b3402c11087e37195930c333dfff221c6a43 100644 (file)
--- 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 b5e137b4d91f428165a85ececec6873023007804..4013cbd083bd5cee29aebbc403e74790d1710e4c 100644 (file)
--- 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 058a20aebeac3381689706bc74da33aa8f737595..452acfea060f817090b378e054d38df54c92476e 100644 (file)
--- 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 e3db6887b38bbde1956430b9a60967a96446cc6c..30bb4bad0cab79f1ec0fb26b7819a352eaf37636 100644 (file)
--- 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 84cea99a1b1d034e26d94a32017dfa866d6fa496..a7e6f69ee6077f29eadbc657cf7b4991008deb58 100644 (file)
--- 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 4301631211eceedbbc7548cc5a21dbcc28476ebc..9d2dd882f408488ff875def8ff40a17e240c0300 100644 (file)
--- 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 649178f9126b37d832aaf3bb245ce2bc3b295217..c5dbd38f875ca59c6ec3a6a8645365b16db20d11 100644 (file)
--- 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 d17a663c6dd0a445c720e8ebd753335bb561bbd9..bfbc50c9d46181d6909bb3b3523cb9886d133ae5 100644 (file)
--- 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 07180cf4fb43334992104d952cf18ffe3782a8c0..b2ac3364edc01593fe30750f8f4e5389f5eccc76 100644 (file)
--- 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 (file)
index 0000000..2112e70
--- /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 (file)
index 0000000..420a0fd
--- /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 (file)
index 0000000..85a5d18
--- /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 (file)
index 0000000..7441924
--- /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 (file)
index 0000000..df7c510
--- /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