diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-01-31 11:06:41 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-01-31 11:06:41 -0600 |
commit | d5dcc0731061484bb6f4db8d3c04abe41ac795d2 (patch) | |
tree | 281e8ab81172a3f53ad5a71c81bf6568d304a84c /src | |
parent | 087ff3ef026440480eb7f72c75f0710b10192623 (diff) |
Refactor relevance vectors for asserted quantifiers (#3666)
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/quantifiers/first_order_model.cpp | 21 | ||||
-rw-r--r-- | src/theory/quantifiers/first_order_model.h | 23 |
2 files changed, 32 insertions, 12 deletions
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index bfef42b65..2b7f78008 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -38,7 +38,8 @@ FirstOrderModel::FirstOrderModel(QuantifiersEngine* qe, std::string name) : TheoryModel(c, name, true), d_qe(qe), - d_forall_asserts(c) + d_forall_asserts(c), + d_forallRlvComputed(false) { } @@ -55,12 +56,13 @@ unsigned FirstOrderModel::getNumAssertedQuantifiers() { } Node FirstOrderModel::getAssertedQuantifier( unsigned i, bool ordered ) { - if( !ordered ){ + if( !ordered || !d_forallRlvComputed ){ return d_forall_asserts[i]; - }else{ - Assert(d_forall_rlv_assert.size() == d_forall_asserts.size()); - return d_forall_rlv_assert[i]; } + // If we computed the relevant forall assertion vector, in reset_round, + // then it should have the same size as the default assertion vector. + Assert(d_forall_rlv_assert.size() == d_forall_asserts.size()); + return d_forall_rlv_assert[i]; } void FirstOrderModel::initialize() { @@ -160,7 +162,9 @@ void FirstOrderModel::reset_round() { } //order the quantified formulas d_forall_rlv_assert.clear(); + d_forallRlvComputed = false; if( !d_forall_rlv_vec.empty() ){ + d_forallRlvComputed = true; Trace("fm-relevant") << "Build sorted relevant list..." << std::endl; Trace("fm-relevant-debug") << "Add relevant asserted formulas..." << std::endl; std::map<Node, bool>::iterator ita; @@ -187,10 +191,6 @@ 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] ); - } } } @@ -225,8 +225,7 @@ bool FirstOrderModel::isQuantifierActive(TNode q) const 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(); + return std::find( d_forall_asserts.begin(), d_forall_asserts.end(), q )!=d_forall_asserts.end(); } Node FirstOrderModel::getModelBasisTerm(TypeNode tn) diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index a113d1b1b..ab1f7c768 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -132,10 +132,31 @@ class FirstOrderModel : public TheoryModel QuantifiersEngine* d_qe; /** list of quantifiers asserted in the current context */ context::CDList<Node> d_forall_asserts; - /** quantified formulas marked as relevant */ + /** + * The (ordered) list of quantified formulas marked as relevant using + * markRelevant, where the quantified formula q in the most recent + * call to markRelevant comes last in the list. + */ std::vector<Node> d_forall_rlv_vec; + /** The last quantified formula marked as relevant, if one exists. */ Node d_last_forall_rlv; + /** + * The list of asserted quantified formulas, ordered by relevance. + * Relevance is a dynamic partial ordering where q1 < q2 if there has been + * a call to markRelevant( q1 ) after the last call to markRelevant( q2 ) + * (or no call to markRelevant( q2 ) has been made). + * + * This list is used primarily as an optimization for conflict-based + * instantiation so that quantifed formulas that have been instantiated + * most recently are processed first, since these are (statistically) more + * likely to have conflicting instantiations. + */ std::vector<Node> d_forall_rlv_assert; + /** + * Whether the above list has been computed. This flag is updated during + * reset_round and is valid within a full effort check. + */ + bool d_forallRlvComputed; /** get variable id */ std::map<Node, std::map<Node, int> > d_quant_var_id; /** process initialize model for term */ |