Minor fixes for relations, quantifiers dsplit.

diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 9e29e21aa2934cf78e2bfa7f2e2e8b4acd944e87..b6743724b145a19471f39e4c52fccdba4e49d7fa 100644 (file)
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -62,7 +62,7 @@ unsigned FirstOrderModel::getNumAssertedQuantifiers() {
 }
 
 Node FirstOrderModel::getAssertedQuantifier( unsigned i, bool ordered ) { 
-  if( !ordered || d_forall_rlv_assert.empty() ){
+  if( !ordered ){
     return d_forall_asserts[i]; 
   }else{
     Assert( d_forall_rlv_assert.size()==d_forall_asserts.size() );
@@ -148,9 +148,9 @@ void FirstOrderModel::reset_round() {
   d_quant_active.clear();
   
   //order the quantified formulas
+  d_forall_rlv_assert.clear();
   if( !d_forall_rlv_vec.empty() ){
     Trace("fm-relevant") << "Build sorted relevant list..." << std::endl;
-    d_forall_rlv_assert.clear();
     Trace("fm-relevant-debug") << "Mark asserted quantified formulas..." << std::endl;
     std::map< Node, bool > qassert;
     for( unsigned i=0; i<d_forall_asserts.size(); i++ ){
@@ -179,6 +179,10 @@ void FirstOrderModel::reset_round() {
     }
     Trace("fm-relevant-debug") << "Sizes : " << d_forall_rlv_assert.size() << " " << d_forall_asserts.size() << std::endl;
     Assert( d_forall_rlv_assert.size()==d_forall_asserts.size() );
+  }else{
+    for( unsigned i=0; i<d_forall_asserts.size(); i++ ){
+      d_forall_rlv_assert.push_back( d_forall_asserts[i] );
+    }
   }
 }
 
@@ -203,10 +207,6 @@ int FirstOrderModel::getRelevanceValue( Node q ) {
   }
 }
 
-//bool FirstOrderModel::isQuantifierAsserted( TNode q ) {
-//  return d_forall_asserts.find( q )!=d_forall_asserts.end();
-//}
-
 void FirstOrderModel::setQuantifierActive( TNode q, bool active ) {
   d_quant_active[q] = active;
 }
@@ -220,6 +220,10 @@ bool FirstOrderModel::isQuantifierActive( TNode q ) {
   }
 }
 
+bool FirstOrderModel::isQuantifierAsserted( TNode q ) {
+  Assert( d_forall_rlv_assert.size()==d_forall_asserts.size() );
+  return std::find( d_forall_rlv_assert.begin(), d_forall_rlv_assert.end(), q )!=d_forall_rlv_assert.end();
+}
 
 FirstOrderModelIG::FirstOrderModelIG(QuantifiersEngine * qe, context::Context* c, std::string name) :
 FirstOrderModel(qe, c,name) {

diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index 44ffd095a1e78f85084f23c95bf24248ea43ae4e..7ded1b05dc920665c3e45cbf8253d53ed98071ab 100644 (file)
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -113,6 +113,8 @@ public:
   void setQuantifierActive( TNode q, bool active );
   /** is quantified formula active */
   bool isQuantifierActive( TNode q );
+  /** is quantified formula asserted */
+  bool isQuantifierAsserted( TNode q );
 };/* class FirstOrderModel */
 
 

diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp
index 24d26e72f117c7860466fc272b91788fc6ccba17..63935f170ac0d72e4058b72bb1217417ce713241 100644 (file)
--- a/src/theory/quantifiers/quant_split.cpp
+++ b/src/theory/quantifiers/quant_split.cpp
@@ -89,7 +89,7 @@ void QuantDSplit::check( Theory::Effort e, unsigned quant_e ) {
     std::vector< Node > lemmas;
     for(std::map< Node, int >::iterator it = d_quant_to_reduce.begin(); it != d_quant_to_reduce.end(); ++it) {
       Node q = it->first;
-      if( d_quantEngine->getModel()->isQuantifierActive( q ) ){
+      if( d_quantEngine->getModel()->isQuantifierAsserted( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
         if( d_added_split.find( q )==d_added_split.end() ){
           d_added_split.insert( q );
           std::vector< Node > bvs;

diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp
index ac5463e13a9304d13fac0e19015963db505c5e4f..db29843d804c098e93ebb7eaec3aaaf3b28218d4 100644 (file)
--- a/src/theory/sets/theory_sets_rels.cpp
+++ b/src/theory/sets/theory_sets_rels.cpp
@@ -1424,10 +1424,6 @@ int TheorySetsRels::EqcInfo::counter        = 0;
     EqcInfo* t2_ei = getOrMakeEqcInfo(t2);
 
     if(t1_ei != NULL && t2_ei != NULL) {
-      // PT(t1) = PT(t2) -> t1 = t2;
-      if(!t1_ei->d_pt.get().isNull() && !t2_ei->d_pt.get().isNull()) {
-        sendInferProduct( true, t1_ei->d_pt.get(), t2_ei->d_pt.get(), explain(NodeManager::currentNM()->mkNode(kind::EQUAL,t1, t2)) );
-      }
       // Apply Product rule on (non)members of t2 and t1->pt
       if(!t1_ei->d_pt.get().isNull()) {
         for(NodeSet::key_iterator itr = t2_ei->d_mem.key_begin(); itr != t2_ei->d_mem.key_end(); itr++) {