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 1112c2ef25612b00086b64190e5d9108568b6fe3..e9ac9b48468f95b52478fce8f15c562298e619fc 100644 (file)
--- 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 db07a0b51b9943eca175464083eacaa9378c8db2..6c4a0054132545b9b27251de5224fa378b11c20c 100644 (file)
--- 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 ab597350e59ec53d6f4f76a399c1ab85f41cfb9d..d509a9fd5e763c96e8f457d8d8b7fda004a85a82 100644 (file)
--- 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 6b8c536d5dd1d282f62164731e72118b77c1e681..d42bf6f557a220d6ecf807352494edff9188423a 100644 (file)
--- 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))