Simplify reductions for set and bag choose (#8304)

Ensures that the reductions are deterministic, thus fixes cvc5/cvc5-projects#493.

The reductions can be further simplified to not introduce UF. This will be addressed in a later PR.

diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp
index 37b6415e0dca1d9c670ab971f2ef834e9f5537ac..39b5a7e3cb74ec34380725d106ccf054ad42e929 100644 (file)
--- a/src/theory/bags/theory_bags.cpp
+++ b/src/theory/bags/theory_bags.cpp
@@ -110,17 +110,14 @@ TrustNode TheoryBags::expandChooseOperator(const Node& node,
 {
   Assert(node.getKind() == BAG_CHOOSE);
 
-  // (bag.choose A) is expanded as
-  // (witness ((x elementType))
-  //    (ite
-  //      (= A (as bag.empty (Bag E)))
-  //      (= x (uf A))
-  //      (and (>= (bag.count x A) 1) (= x (uf A)))
+  // (bag.choose A) is eliminated to k, with lemma
+  // (and (= k (uf A)) (or (= A (as bag.empty (Bag E))) (>= (bag.count k A) 1)))
   // where uf: (Bag E) -> E is a skolem function, and E is the type of elements
   // of A
 
   NodeManager* nm = NodeManager::currentNM();
   SkolemManager* sm = nm->getSkolemManager();
+  Node x = sm->mkPurifySkolem(node, "bagChoose");
   Node A = node[0];
   TypeNode bagType = A.getType();
   TypeNode ufType = nm->mkFunctionType(bagType, bagType.getBagElementType());
@@ -128,21 +125,18 @@ TrustNode TheoryBags::expandChooseOperator(const Node& node,
   Node uf = sm->mkSkolemFunction(SkolemFunId::BAGS_CHOOSE, ufType, Node());
   Node ufA = NodeManager::currentNM()->mkNode(APPLY_UF, uf, A);
 
-  Node x = nm->mkBoundVar(bagType.getBagElementType());
-
   Node equal = x.eqNode(ufA);
   Node emptyBag = nm->mkConst(EmptyBag(bagType));
   Node isEmpty = A.eqNode(emptyBag);
   Node count = nm->mkNode(BAG_COUNT, x, A);
   Node one = nm->mkConstInt(Rational(1));
   Node geqOne = nm->mkNode(GEQ, count, one);
-  Node geqOneAndEqual = geqOne.andNode(equal);
-  Node ite = nm->mkNode(ITE, isEmpty, equal, geqOneAndEqual);
-  Node ret = sm->mkSkolem(x, ite, "kBagChoose");
-  lems.push_back(SkolemLemma(ret, nullptr));
+  Node lem = nm->mkNode(AND, equal, nm->mkNode(OR, isEmpty, geqOne));
+  TrustNode tlem = TrustNode::mkTrustLemma(lem, nullptr);
+  lems.push_back(SkolemLemma(tlem, x));
   Trace("TheoryBags::ppRewrite")
-      << "ppRewrite(" << node << ") = " << ret << std::endl;
-  return TrustNode::mkTrustRewrite(node, ret, nullptr);
+      << "ppRewrite(" << node << ") = " << x << std::endl;
+  return TrustNode::mkTrustRewrite(node, x, nullptr);
 }
 
 void TheoryBags::postCheck(Effort effort)

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 37215458fd3000a9bab686e978161c5450202fe7..6bc58270061d32550d6bf40acd62644be596ba63 100644 (file)
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -1366,17 +1366,14 @@ TrustNode TheorySetsPrivate::expandChooseOperator(
 {
   Assert(node.getKind() == SET_CHOOSE);
 
-  // (choose A) is expanded as
-  // (witness ((x elementType))
-  //    (ite
-  //      (= A (as emptyset (Set E)))
-  //      (= x (uf A))
-  //      (and (member x A) (= x uf(A)))
+  // (choose A) is eliminated to k, with lemma
+  //   (and (= k (uf A)) (or (= A (as set.empty (Set E))) (set.member k A)))
   // where uf: (Set E) -> E is a skolem function, and E is the type of elements
   // of A
 
   NodeManager* nm = NodeManager::currentNM();
   SkolemManager* sm = nm->getSkolemManager();
+  Node x = sm->mkPurifySkolem(node, "setChoose");
   Node A = node[0];
   TypeNode setType = A.getType();
   ensureFirstClassSetType(setType);
@@ -1385,17 +1382,14 @@ TrustNode TheorySetsPrivate::expandChooseOperator(
   Node uf = sm->mkSkolemFunction(SkolemFunId::SETS_CHOOSE, ufType, Node());
   Node ufA = NodeManager::currentNM()->mkNode(APPLY_UF, uf, A);
 
-  Node x = nm->mkBoundVar(setType.getSetElementType());
-
   Node equal = x.eqNode(ufA);
   Node emptySet = nm->mkConst(EmptySet(setType));
   Node isEmpty = A.eqNode(emptySet);
   Node member = nm->mkNode(SET_MEMBER, x, A);
-  Node memberAndEqual = member.andNode(equal);
-  Node ite = nm->mkNode(ITE, isEmpty, equal, memberAndEqual);
-  Node ret = sm->mkSkolem(x, ite, "kSetChoose");
-  lems.push_back(SkolemLemma(ret, nullptr));
-  return TrustNode::mkTrustRewrite(node, ret, nullptr);
+  Node lem = nm->mkNode(AND, equal, nm->mkNode(OR, isEmpty, member));
+  TrustNode tlem = TrustNode::mkTrustLemma(lem, nullptr);
+  lems.push_back(SkolemLemma(tlem, x));
+  return TrustNode::mkTrustRewrite(node, x, nullptr);
 }
 
 TrustNode TheorySetsPrivate::expandIsSingletonOperator(const Node& node)

diff --git a/src/theory/skolem_lemma.cpp b/src/theory/skolem_lemma.cpp
index af4d09492b9805136e622b48cd732fc8d97243e0..b0b59b7e4dfbf1f7f9fd217e36f25772a23551fa 100644 (file)
--- a/src/theory/skolem_lemma.cpp
+++ b/src/theory/skolem_lemma.cpp
@@ -25,22 +25,7 @@ SkolemLemma::SkolemLemma(TrustNode lem, Node k) : d_lemma(lem), d_skolem(k)
   Assert(lem.getKind() == TrustNodeKind::LEMMA);
 }
 
-SkolemLemma::SkolemLemma(Node k, ProofGenerator* pg) : d_lemma(), d_skolem(k)
-{
-  Node lem = getSkolemLemmaFor(k);
-  d_lemma = TrustNode::mkTrustLemma(lem, pg);
-}
-
 Node SkolemLemma::getProven() const { return d_lemma.getProven(); }
 
-Node SkolemLemma::getSkolemLemmaFor(Node k)
-{
-  Node w = SkolemManager::getWitnessForm(k);
-  Assert(w.getKind() == kind::WITNESS);
-  TNode tx = w[0][0];
-  TNode tk = k;
-  return w[1].substitute(tx, tk);
-}
-
 }  // namespace theory
 }  // namespace cvc5

diff --git a/src/theory/skolem_lemma.h b/src/theory/skolem_lemma.h
index 4f17ed9d3a78a053dd4a75ca09b6edabb96a7b28..0e78427f8b9f561d2688b78d7290cb2cb758cc99 100644 (file)
--- a/src/theory/skolem_lemma.h
+++ b/src/theory/skolem_lemma.h
@@ -41,11 +41,6 @@ class SkolemLemma
    * Make skolem from trust node lem of kind LEMMA and skolem k.
    */
   SkolemLemma(TrustNode lem, Node k);
-  /**
-   * Make skolem lemma from witness form of skolem k. If non-null, pg is
-   * proof generator that can generator a proof for getSkolemLemmaFor(k).
-   */
-  SkolemLemma(Node k, ProofGenerator* pg);
 
   /** The lemma, a trust node of kind LEMMA */
   TrustNode d_lemma;
@@ -54,11 +49,6 @@ class SkolemLemma
 
   /** Get proven from the lemma */
   Node getProven() const;
-  /**
-   * Get the lemma for skolem k based on its witness form. If k has witness
-   * form (witness ((x T)) (P x)), this is the formula (P k).
-   */
-  static Node getSkolemLemmaFor(Node k);
 };
 
 }  // namespace theory

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 67073033d18fb5caf3e37a4ba36e50396b221f2c..84aebd5ae52a02d309c87441ea3e880066f6e1cb 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1254,6 +1254,7 @@ set(regress_0_tests
   regress0/sets/pre-proc-univ.smt2
   regress0/sets/proj-issue177.smt2
   regress0/sets/proj-issue486-sets-split-eq.smt2
+  regress0/sets/proj-issue493-choose-det.smt2
   regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2
   regress0/sets/setel-eq.smt2
   regress0/sets/sets-deq-dd.smt2

diff --git a/test/regress/regress0/sets/proj-issue493-choose-det.smt2 b/test/regress/regress0/sets/proj-issue493-choose-det.smt2
new file mode 100644 (file)
index 0000000..16f8e1d
--- /dev/null
+++ b/test/regress/regress0/sets/proj-issue493-choose-det.smt2
@@ -0,0 +1,8 @@
+(set-logic ALL)
+(set-info :status unsat)
+(set-option :sets-ext true)
+(declare-const x Bool)
+(declare-const x3 Bool)
+(declare-const x4 Bool)
+(assert (forall ((x2 Bool)) (ite (not (set.choose (set.complement (set.insert x3 x4 false false (set.singleton x))))) (set.choose (set.complement (set.insert x3 x4 x2 false (set.singleton x)))) false)))
+(check-sat)