diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-02-16 16:19:51 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-02-16 16:19:51 -0600 |
commit | 21b0cedd7dadd96e5d256885e3b65a926a7e4a81 (patch) | |
tree | 9874097e04e8d36eb8db45ce2ad7cf2a2a9803b9 | |
parent | 3a0e9d8d9a1288187db69b103dfd18ad64358f18 (diff) |
Minor fixes for relations, quantifiers dsplit.
-rw-r--r-- | src/theory/quantifiers/first_order_model.cpp | 16 | ||||
-rw-r--r-- | src/theory/quantifiers/first_order_model.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/quant_split.cpp | 2 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_rels.cpp | 4 |
4 files changed, 13 insertions, 11 deletions
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 9e29e21aa..b6743724b 100644 --- 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 44ffd095a..7ded1b05d 100644 --- 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 24d26e72f..63935f170 100644 --- 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 ac5463e13..db29843d8 100644 --- 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++) { |