Fix issue #5342 (#5349)

This PR fixes issue #5342 by adding the rewrite rule (setminus A (setminus A B)) = (intersection A B).

diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp
index 21344ee7329485cb9ac2a9c72693bded9d8b0c7b..cb0540b8675e25f7b4e8ef88dadac6641662a988 100644 (file)
--- a/src/theory/sets/cardinality_extension.cpp
+++ b/src/theory/sets/cardinality_extension.cpp
@@ -308,6 +308,9 @@ void CardinalityExtension::checkCardCycles()
       return;
     }
   }
+
+  Trace("sets") << "d_card_parent: " << d_card_parent << std::endl;
+  Trace("sets") << "d_oSetEqc: " << d_oSetEqc << std::endl;
   Trace("sets") << "Done check cardinality cycles" << std::endl;
 }
 

diff --git a/src/theory/sets/cardinality_extension.h b/src/theory/sets/cardinality_extension.h
index 6704ce4a7e5464d144448da0070ccc2ddc7132d8..08424d3c465bab0253a218b05283df22423f6694 100644 (file)
--- a/src/theory/sets/cardinality_extension.h
+++ b/src/theory/sets/cardinality_extension.h
@@ -167,7 +167,7 @@ class CardinalityExtension
   TermRegistry& d_treg;
   /** register cardinality term
    *
-   * This method add lemmas corresponding to the definition of
+   * This method adds lemmas corresponding to the definition of
    * the cardinality of set term n. For example, if n is A^B (denoting set
    * intersection as ^), then we consider the lemmas card(A^B)>=0,
    * card(A) = card(A\B) + card(A^B) and card(B) = card(B\A) + card(A^B).

diff --git a/src/theory/sets/solver_state.cpp b/src/theory/sets/solver_state.cpp
index cf9f4aa7a612f3c38ee500ac9a4a2bbad0b60300..1d58945a58d44ef61f52e89e4cc205ac28b94b03 100644 (file)
--- a/src/theory/sets/solver_state.cpp
+++ b/src/theory/sets/solver_state.cpp
@@ -444,6 +444,13 @@ SolverState::getBinaryOpIndex() const
 {
   return d_bop_index;
 }
+
+const std::map<Node, std::map<Node, Node>>& SolverState::getBinaryOpIndex(
+    Kind k)
+{
+  return d_bop_index[k];
+}
+
 const std::map<Kind, std::vector<Node> >& SolverState::getOperatorList() const
 {
   return d_op_list;

diff --git a/src/theory/sets/solver_state.h b/src/theory/sets/solver_state.h
index 32b4d611352416f7ace703fadc3588a0d47875dd..41d3ac7178b0c610d50326e7b20c8654cd5d40f6 100644 (file)
--- a/src/theory/sets/solver_state.h
+++ b/src/theory/sets/solver_state.h
@@ -146,6 +146,13 @@ class SolverState : public TheoryState
    */
   const std::map<Kind, std::map<Node, std::map<Node, Node> > >&
   getBinaryOpIndex() const;
+
+  /** Get binary operator index
+   *
+   * This returns the binary operator index of the given kind.
+   * See getBinaryOpIndex() above.
+   */
+  const std::map<Node, std::map<Node, Node> >& getBinaryOpIndex(Kind k);
   /** get operator list
    *
    * This returns a mapping from set kinds to a list of terms of that kind

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index a382688a9c12bae1c8bd6334fa93848c96d2f092..e44c3c7a6aee815cad904c465a084049341e0496 100644 (file)
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -389,6 +389,7 @@ void TheorySetsPrivate::fullEffortCheck()
     }
     // check reduce comprehensions
     checkReduceComprehensions();
+
     d_im.doPendingLemmas();
     if (d_im.hasSent())
     {

diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index 847bf34eb903adc0510f622a9c5ac35960d70a10..1e4473d6f553c528abb9fcd997d3ea41c78aef19 100644 (file)
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -119,32 +119,52 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
     break;
   }
 
-  case kind::SETMINUS: {
-    if(node[0] == node[1]) {
+  case kind::SETMINUS:
+  {
+    if (node[0] == node[1])
+    {
       Node newNode = nm->mkConst(EmptySet(node[0].getType()));
-      Trace("sets-postrewrite") << "Sets::postRewrite returning " << newNode << std::endl;
+      Trace("sets-postrewrite")
+          << "Sets::postRewrite returning " << newNode << std::endl;
       return RewriteResponse(REWRITE_DONE, newNode);
-    } else if(node[0].getKind() == kind::EMPTYSET ||
-              node[1].getKind() == kind::EMPTYSET) {
-      Trace("sets-postrewrite") << "Sets::postRewrite returning " << node[0] << std::endl;
+    }
+    else if (node[0].getKind() == kind::EMPTYSET
+             || node[1].getKind() == kind::EMPTYSET)
+    {
+      Trace("sets-postrewrite")
+          << "Sets::postRewrite returning " << node[0] << std::endl;
       return RewriteResponse(REWRITE_AGAIN, node[0]);
-    }else if( node[1].getKind() == kind::UNIVERSE_SET ){
+    }
+    else if (node[1].getKind() == kind::SETMINUS && node[1][0] == node[0])
+    {
+      // (setminus A (setminus A B)) = (intersection A B)
+      Node intersection = nm->mkNode(INTERSECTION, node[0], node[1][1]);
+      return RewriteResponse(REWRITE_AGAIN, intersection);
+    }
+    else if (node[1].getKind() == kind::UNIVERSE_SET)
+    {
       return RewriteResponse(
           REWRITE_AGAIN,
           NodeManager::currentNM()->mkConst(EmptySet(node[1].getType())));
-    } else if(node[0].isConst() && node[1].isConst()) {
+    }
+    else if (node[0].isConst() && node[1].isConst())
+    {
       std::set<Node> left = NormalForm::getElementsFromNormalConstant(node[0]);
       std::set<Node> right = NormalForm::getElementsFromNormalConstant(node[1]);
       std::set<Node> newSet;
-      std::set_difference(left.begin(), left.end(), right.begin(), right.end(),
-        std::inserter(newSet, newSet.begin()));
+      std::set_difference(left.begin(),
+                          left.end(),
+                          right.begin(),
+                          right.end(),
+                          std::inserter(newSet, newSet.begin()));
       Node newNode = NormalForm::elementsToSet(newSet, node.getType());
       Assert(newNode.isConst());
-      Trace("sets-postrewrite") << "Sets::postRewrite returning " << newNode << std::endl;
+      Trace("sets-postrewrite")
+          << "Sets::postRewrite returning " << newNode << std::endl;
       return RewriteResponse(REWRITE_DONE, newNode);
     }
     break;
-  }//kind::SETMINUS
+  }  // kind::SETMINUS
 
   case kind::INTERSECTION: {
     if(node[0] == node[1]) {
@@ -203,11 +223,14 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
     // we don't merge non-constant unions
     break;
   }//kind::UNION
-  case kind::COMPLEMENT: {
-    Node univ = NodeManager::currentNM()->mkNullaryOperator( node[0].getType(), kind::UNIVERSE_SET );
-    return RewriteResponse( REWRITE_AGAIN, NodeManager::currentNM()->mkNode( kind::SETMINUS, univ, node[0] ) );
+  case kind::COMPLEMENT:
+  {
+    Node univ = NodeManager::currentNM()->mkNullaryOperator(node[0].getType(),
+                                                            kind::UNIVERSE_SET);
+    return RewriteResponse(
+        REWRITE_AGAIN,
+        NodeManager::currentNM()->mkNode(kind::SETMINUS, univ, node[0]));
   }
-    break;
   case kind::CARD: {
     if(node[0].isConst()) {
       std::set<Node> elements = NormalForm::getElementsFromNormalConstant(node[0]);
@@ -510,6 +533,7 @@ RewriteResponse TheorySetsRewriter::preRewrite(TNode node) {
                                       nm->mkNode(kind::UNION, node[0], node[1]),
                                       node[1]) );
   }
+
   // could have an efficient normalizer for union here
 
   return RewriteResponse(REWRITE_DONE, node);

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 334901c7ab26bfcf3589ddab75d8947a613a750b..c6c55d8478b13c3ed4ca505407105d1e19de7529 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1793,6 +1793,8 @@ set(regress_1_tests
   regress1/sets/issue4391-card-lasso.smt2
   regress1/sets/issue5271.smt2
   regress1/sets/issue5309.smt2
+  regress1/sets/issue5342.smt2
+  regress1/sets/issue5342_difference_version.smt2
   regress1/sets/lemmabug-ListElts317minimized.smt2
   regress1/sets/remove_check_free_31_6.smt2
   regress1/sets/sets-disequal.smt2

diff --git a/test/regress/regress1/sets/issue5342.smt2 b/test/regress/regress1/sets/issue5342.smt2
new file mode 100644 (file)
index 0000000..e5e7ed6
--- /dev/null
+++ b/test/regress/regress1/sets/issue5342.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --sets-ext
+(set-logic ALL)
+(set-info :status unsat)
+(declare-fun S () (Set Int))
+(assert (is_singleton (complement (complement S))))
+(assert (= 2 (card S)))
+(check-sat)
\ No newline at end of file

diff --git a/test/regress/regress1/sets/issue5342_difference_version.smt2 b/test/regress/regress1/sets/issue5342_difference_version.smt2
new file mode 100644 (file)
index 0000000..143ac56
--- /dev/null
+++ b/test/regress/regress1/sets/issue5342_difference_version.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --sets-ext
+(set-logic ALL)
+(set-info :status unsat)
+(declare-fun S () (Set Int))
+(assert (is_singleton (setminus (as univset (Set Int)) (setminus (as univset (Set Int)) S))))
+(assert (= 2 (card S)))
+(check-sat)
\ No newline at end of file