From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Fri, 14 Apr 2017 22:25:18 +0000 (-0500)
Subject: Actively split for upwards closusure intersection. Minor clean up, add regressions.
X-Git-Tag: cvc5-1.0.0~5834
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=25fcfe393d1d8808a866a5f1cfc4f7edf273316d;p=cvc5.git

Actively split for upwards closusure intersection. Minor clean up, add regressions.
---

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index e9e92a5b1..66a56b2ab 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -791,7 +791,6 @@ Node NodeManager::mkBooleanTermVariable() {
 }
 
 Node NodeManager::mkNullaryOperator(const TypeNode& type, Kind k) {
-  //FIXME : this is not correct for multitheading
   std::map< TypeNode, Node >::iterator it = d_unique_vars[k].find( type );
   if( it==d_unique_vars[k].end() ){
     Node n = NodeBuilder<0>(this, k).constructNode();
@@ -799,10 +798,8 @@ Node NodeManager::mkNullaryOperator(const TypeNode& type, Kind k) {
     //setAttribute(n, TypeCheckedAttr(), true);
     d_unique_vars[k][type] = n;
     Assert( n.getMetaKind() == kind::metakind::NULLARY_OPERATOR );
-    Trace("ajr-temp") << this << "...made nullary operator " << n << " " << &n << " " << type << std::endl;
     return n;
   }else{
-    Trace("ajr-temp") << this << "...reuse nullary operator " << it->second << " " << &( it->second ) << std::endl;
     return it->second;
   }
 }
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 57ab8c0cf..626351f64 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -758,6 +758,7 @@ void TheorySetsPrivate::checkUpwardsClosure( std::vector< Node >& lemmas ) {
           Node r2 = it2->first;
           //see if there are members in second argument
           std::map< Node, std::map< Node, Node > >::iterator itm2 = d_pol_mems[0].find( r2 );
+          std::map< Node, std::map< Node, Node > >::iterator itm2n = d_pol_mems[1].find( r2 );
           if( itm2!=d_pol_mems[0].end() || k!=kind::INTERSECTION ){
             Trace("sets-debug") << "Checking " << it2->second << ", members = " << (itm1!=d_pol_mems[0].end()) << ", " << (itm2!=d_pol_mems[0].end()) << std::endl;
             //for all members of r1
@@ -782,6 +783,14 @@ void TheorySetsPrivate::checkUpwardsClosure( std::vector< Node >& lemmas ) {
                     addEqualityToExp( it2->second[1], itm2->second[xr][1], exp );
                     addEqualityToExp( x, itm2->second[xr][0], exp );
                     valid = true;
+                  }else{
+                    // if not, check whether it is definitely not a member, if unknown, split
+                    bool not_in_r2 = itm2n!=d_pol_mems[1].end() && itm2n->second.find( xr )!=itm2->second.end();
+                    if( !not_in_r2 ){
+                      exp.push_back( NodeManager::currentNM()->mkNode( kind::MEMBER, x, it2->second[1] ) );
+                      valid = true;
+                      inferType = 1;
+                    }
                   }
                 }else{
                   Assert( k==kind::SETMINUS );
@@ -1714,8 +1723,11 @@ void TheorySetsPrivate::computeCareGraph() {
           }
         }
         if( hasCareArg ){
+          Trace("sets-cg-debug") << "......adding." << std::endl;
           index[tn].addTerm( f1, reps );
           arity = reps.size();
+        }else{
+          Trace("sets-cg-debug") << "......skip." << std::endl;
         }
       }
       if( arity>0 ){
diff --git a/test/regress/regress0/rels/Makefile.am b/test/regress/regress0/rels/Makefile.am
index 7c9dca8dd..bb9c49298 100644
--- a/test/regress/regress0/rels/Makefile.am
+++ b/test/regress/regress0/rels/Makefile.am
@@ -101,7 +101,8 @@ TESTS =	\
   rel_transpose_0.cvc \
   set-strat.cvc \
   rel_tc_8.cvc \
-  atom_univ2.cvc
+  atom_univ2.cvc \
+  rels-sharing-simp.cvc
 
 # unsolved : garbage_collect.cvc
 
diff --git a/test/regress/regress0/rels/rels-sharing-simp.cvc b/test/regress/regress0/rels/rels-sharing-simp.cvc
new file mode 100644
index 000000000..26bc94a43
--- /dev/null
+++ b/test/regress/regress0/rels/rels-sharing-simp.cvc
@@ -0,0 +1,14 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+w : SET OF IntPair;
+z : SET OF IntPair;
+x : INT;
+y : INT;
+
+ASSERT (1,x) IS_IN w;
+ASSERT (y,2) IS_IN z;
+
+ASSERT NOT (1, 2) IS_IN ( w JOIN z );
+
+CHECKSAT;
diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am
index 4c65f3a6a..c2e3546d9 100644
--- a/test/regress/regress0/sets/Makefile.am
+++ b/test/regress/regress0/sets/Makefile.am
@@ -78,7 +78,8 @@ TESTS =	\
 	univset-simp.smt2 \
 	complement.cvc \
 	complement2.cvc \
-    complement3.cvc
+  complement3.cvc \
+  sharing-simp.smt2
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/sets/sharing-simp.smt2 b/test/regress/regress0/sets/sharing-simp.smt2
new file mode 100644
index 000000000..761428fde
--- /dev/null
+++ b/test/regress/regress0/sets/sharing-simp.smt2
@@ -0,0 +1,15 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(declare-fun A () (Set Int))
+(declare-fun B () (Set Int))
+(declare-fun C () (Set Int))
+(declare-fun D () (Set Int))
+
+(assert (member x A))
+(assert (member y B))
+(assert (or (= C (intersection A B)) (= D (intersection A B))))
+
+
+(check-sat)