From: Andrew Reynolds Date: Mon, 1 Jul 2019 22:27:53 +0000 (-0500) Subject: Refactoring of relevance vector in quantifiers (#3070) X-Git-Tag: cvc5-1.0.0~4097 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=74fd30f3ac172ac7f1e3708a5d47df1a1018c51b;p=cvc5.git Refactoring of relevance vector in quantifiers (#3070) --- diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 8d29cb8e1..dbf368e66 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -32,19 +32,6 @@ namespace CVC4 { namespace theory { namespace quantifiers { -struct sortQuantifierRelevance { - FirstOrderModel * d_fm; - bool operator() (Node i, Node j) { - int wi = d_fm->getRelevanceValue( i ); - int wj = d_fm->getRelevanceValue( j ); - if( wi==wj ){ - return i& elements) @@ -122,10 +109,13 @@ bool QRepBoundExt::getVariableOrder(Node owner, std::vector& varOrder) return false; } -FirstOrderModel::FirstOrderModel(QuantifiersEngine * qe, context::Context* c, std::string name ) : -TheoryModel( c, name, true ), -d_qe( qe ), d_forall_asserts( c ){ - d_rlv_count = 0; +FirstOrderModel::FirstOrderModel(QuantifiersEngine* qe, + context::Context* c, + std::string name) + : TheoryModel(c, name, true), + d_qe(qe), + d_forall_asserts(c) +{ } void FirstOrderModel::assertQuantifier( Node n ){ @@ -232,32 +222,40 @@ bool FirstOrderModel::checkNeeded() { void FirstOrderModel::reset_round() { d_quant_active.clear(); - + + // compute which quantified formulas are asserted if necessary + std::map qassert; + if (!d_forall_rlv_vec.empty()) + { + Trace("fm-relevant-debug") + << "Mark asserted quantified formulas..." << std::endl; + for (const Node& q : d_forall_asserts) + { + qassert[q] = true; + } + } //order the quantified formulas d_forall_rlv_assert.clear(); if( !d_forall_rlv_vec.empty() ){ Trace("fm-relevant") << "Build sorted relevant list..." << std::endl; - Trace("fm-relevant-debug") << "Mark asserted quantified formulas..." << std::endl; - std::map< Node, bool > qassert; - for( unsigned i=0; i::iterator ita; for( int i=(int)(d_forall_rlv_vec.size()-1); i>=0; i-- ){ Node q = d_forall_rlv_vec[i]; - if( qassert.find( q )!=qassert.end() ){ - Trace("fm-relevant") << " " << d_forall_rlv[q] << " : " << q << std::endl; + ita = qassert.find(q); + if (ita != qassert.end()) + { + Trace("fm-relevant") << " " << q << std::endl; d_forall_rlv_assert.push_back( q ); + qassert.erase(ita); } } Trace("fm-relevant-debug") << "Add remaining asserted formulas..." << std::endl; - for( unsigned i=0; i::iterator itr = + std::find(d_forall_rlv_vec.begin(), d_forall_rlv_vec.end(), q); + if (itr != d_forall_rlv_vec.end()) + { + d_forall_rlv_vec.erase(itr, itr + 1); } - d_forall_rlv[ q ] = d_rlv_count; - d_rlv_count++; + d_forall_rlv_vec.push_back(q); d_last_forall_rlv = q; } } -int FirstOrderModel::getRelevanceValue( Node q ) { - std::map< Node, unsigned >::iterator it = d_forall_rlv.find( q ); - if( it==d_forall_rlv.end() ){ - return -1; - }else{ - return it->second; - } -} - void FirstOrderModel::setQuantifierActive( TNode q, bool active ) { d_quant_active[q] = active; } -bool FirstOrderModel::isQuantifierActive( TNode q ) { - std::map< TNode, bool >::iterator it = d_quant_active.find( q ); +bool FirstOrderModel::isQuantifierActive(TNode q) const +{ + std::map::const_iterator it = d_quant_active.find(q); if( it==d_quant_active.end() ){ return true; - }else{ - return it->second; } + return it->second; } -bool FirstOrderModel::isQuantifierAsserted( TNode q ) { +bool FirstOrderModel::isQuantifierAsserted(TNode q) const +{ 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(); } diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index bdf1d7c15..27d21218d 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -17,9 +17,10 @@ #ifndef CVC4__FIRST_ORDER_MODEL_H #define CVC4__FIRST_ORDER_MODEL_H +#include "expr/attribute.h" +#include "theory/quantifiers_engine.h" #include "theory/theory_model.h" #include "theory/uf/theory_uf_model.h" -#include "expr/attribute.h" namespace CVC4 { namespace theory { @@ -110,17 +111,28 @@ class FirstOrderModel : public TheoryModel void reset_round(); /** mark quantified formula relevant */ void markRelevant( Node q ); - /** get relevance value */ - int getRelevanceValue( Node q ); - /** set quantified formula active/inactive - * a quantified formula may be set inactive if for instance: - * - it is entailed by other quantified formulas + /** set quantified formula active/inactive + * + * This indicates that quantified formula is "inactive", that is, it need + * not be considered during this instantiation round. + * + * A quantified formula may be set inactive if for instance: + * - It is entailed by other quantified formulas, or + * - All of its instances are known to be true in the current model. + * + * This method should be called after a call to FirstOrderModel::reset_round, + * and before calls to QuantifiersModule check calls. A common place to call + * this method is during QuantifiersModule reset_round calls. */ void setQuantifierActive( TNode q, bool active ); - /** is quantified formula active */ - bool isQuantifierActive( TNode q ); + /** is quantified formula active? + * + * Returns false if there has been a call to setQuantifierActive( q, false ) + * during this instantiation round. + */ + bool isQuantifierActive(TNode q) const; /** is quantified formula asserted */ - bool isQuantifierAsserted( TNode q ); + bool isQuantifierAsserted(TNode q) const; /** get model basis term */ Node getModelBasisTerm(TypeNode tn); /** is model basis term */ @@ -156,8 +168,6 @@ class FirstOrderModel : public TheoryModel /** list of quantifiers asserted in the current context */ context::CDList d_forall_asserts; /** quantified formulas marked as relevant */ - unsigned d_rlv_count; - std::map d_forall_rlv; std::vector d_forall_rlv_vec; Node d_last_forall_rlv; std::vector d_forall_rlv_assert;