diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-14 21:58:08 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-14 21:58:08 -0500 |
| commit | 4a1b5ea5568fb6c688f407946f9a7fbb1cec3c31 (patch) | |
| tree | 016119f36abe7835183ce3ca3e2b7ffdaa383fcb /src/theory/quantifiers | |
| parent | 996f6f9e2ecf76e39c236f9c410c109807c7073d (diff) | |
Fix needsModel method for CEGQI (#5048)
There was a bug in CEGQI's needModel method which could say that it doesnt need a model built when there are no active quantifiers. However, computing active quantifiers is not done in QuantifiersEngine::check until after this method is called, meaning it was using stale data on whether a quantifier was active or not. This could lead to the use of bogus models in CEGQI in incremental mode in some corner cases, leading to the assertion failure in #5019.
Fixes #5019.
Diffstat (limited to 'src/theory/quantifiers')
| -rw-r--r-- | src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp | 7 | ||||
| -rw-r--r-- | src/theory/quantifiers/first_order_model.cpp | 3 | ||||
| -rw-r--r-- | src/theory/quantifiers/first_order_model.h | 2 |
3 files changed, 8 insertions, 4 deletions
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index ab1bb16b5..d16024ee3 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -82,9 +82,12 @@ bool InstStrategyCegqi::needsCheck(Theory::Effort e) QuantifiersModule::QEffort InstStrategyCegqi::needsModel(Theory::Effort e) { - for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ + size_t nquant = d_quantEngine->getModel()->getNumAssertedQuantifiers(); + for (size_t i = 0; i < nquant; i++) + { Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); - if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){ + if (doCbqi(q)) + { return QEFFORT_STANDARD; } } diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 61eb4ff39..51ca919bb 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -51,7 +51,8 @@ void FirstOrderModel::assertQuantifier( Node n ){ } } -unsigned FirstOrderModel::getNumAssertedQuantifiers() { +size_t FirstOrderModel::getNumAssertedQuantifiers() const +{ return d_forall_asserts.size(); } diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index bdf6d0607..b35bd6447 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -60,7 +60,7 @@ class FirstOrderModel : public TheoryModel /** assert quantifier */ void assertQuantifier( Node n ); /** get number of asserted quantifiers */ - unsigned getNumAssertedQuantifiers(); + size_t getNumAssertedQuantifiers() const; /** get asserted quantifier */ Node getAssertedQuantifier( unsigned i, bool ordered = false ); /** initialize model for term */ |