From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Wed, 7 Dec 2016 21:26:12 +0000 (-0600)
Subject: Add sets regression, fixes bug 754.  Minor fix to regexp in strings.
X-Git-Tag: cvc5-1.0.0~5946
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=314db5e1c4fdbfca001b1f3a679831d086b25e5c;p=cvc5.git

Add sets regression, fixes bug 754.  Minor fix to regexp in strings.
---

diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index 1112c2ef2..e9ac9b484 100644
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -605,7 +605,7 @@ Node BoundedIntegers::getSetRangeValue( Node q, Node v, RepSetIterator * rsi ) {
     Trace("bound-int-rsi") << "Get value in model for..." << sr << std::endl;
     sr = d_quantEngine->getModel()->getCurrentModelValue( sr );
     Trace("bound-int-rsi") << "Value is " << sr << std::endl;
-    //map to term model
+    //as heuristic, map to term model
     if( sr.getKind()!=EMPTYSET ){
       std::map< Node, Node > val_to_term;
       while( sr.getKind()==UNION ){
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index db07a0b51..6c4a00541 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -4273,10 +4273,13 @@ void TheoryStrings::checkMemberships() {
   for( unsigned i=0; i<mems.size(); i++ ){
     Node n = mems[i];
     Assert( d_extf_info_tmp.find( n )!=d_extf_info_tmp.end() );
-    Assert( d_extf_info_tmp[n].d_pol==1 || d_extf_info_tmp[n].d_pol==-1 );
-    bool pol = d_extf_info_tmp[n].d_pol==1;
-    Trace("strings-process-debug") << "  add membership : " << n << ", pol = " << pol << std::endl;
-    addMembership( pol ? n : n.negate() );
+    if( d_extf_info_tmp[n].d_pol==1 || d_extf_info_tmp[n].d_pol==-1 ){
+      bool pol = d_extf_info_tmp[n].d_pol==1;
+      Trace("strings-process-debug") << "  add membership : " << n << ", pol = " << pol << std::endl;
+      addMembership( pol ? n : n.negate() );
+    }else{
+      Trace("strings-process-debug") << "  irrelevant (non-asserted) membership : " << n << std::endl;
+    }
   }
 
   bool addedLemma = false;
diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am
index ab597350e..d509a9fd5 100644
--- a/test/regress/regress0/sets/Makefile.am
+++ b/test/regress/regress0/sets/Makefile.am
@@ -64,7 +64,8 @@ TESTS =	\
 	union-2.smt2 \
 	dt-simp-mem.smt2 \
 	card3-ground.smt2 \
-	card-3sets.cvc
+	card-3sets.cvc \
+	card.smt2
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/sets/card.smt2 b/test/regress/regress0/sets/card.smt2
index 6b8c536d5..d42bf6f55 100644
--- a/test/regress/regress0/sets/card.smt2
+++ b/test/regress/regress0/sets/card.smt2
@@ -1,4 +1,5 @@
 (set-logic QF_UFLIAFS)
+(set-info :status unsat)
 (declare-sort E 0)
 (declare-fun s () (Set E))
 (declare-fun t () (Set E))