From 4a1b5ea5568fb6c688f407946f9a7fbb1cec3c31 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 14 Sep 2020 21:58:08 -0500 Subject: [PATCH] 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. --- src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp | 7 +++++-- src/theory/quantifiers/first_order_model.cpp | 3 ++- src/theory/quantifiers/first_order_model.h | 2 +- test/regress/CMakeLists.txt | 1 + .../regress1/quantifiers/issue5019-cegqi-i.smt2 | 10 ++++++++++ 5 files changed, 19 insertions(+), 4 deletions(-) create mode 100644 test/regress/regress1/quantifiers/issue5019-cegqi-i.smt2 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; igetModel()->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 */ diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index ef0981372..9e1480852 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1583,6 +1583,7 @@ set(regress_1_tests regress1/quantifiers/issue4290-cegqi-r.smt2 regress1/quantifiers/issue4620-erq-witness-unsound.smt2 regress1/quantifiers/issue4685-wrewrite.smt2 + regress1/quantifiers/issue5019-cegqi-i.smt2 regress1/quantifiers/issue993.smt2 regress1/quantifiers/javafe.ast.StmtVec.009.smt2 regress1/quantifiers/lra-vts-inf.smt2 diff --git a/test/regress/regress1/quantifiers/issue5019-cegqi-i.smt2 b/test/regress/regress1/quantifiers/issue5019-cegqi-i.smt2 new file mode 100644 index 000000000..85c59db22 --- /dev/null +++ b/test/regress/regress1/quantifiers/issue5019-cegqi-i.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: sat +(set-logic BV) +(declare-const v4 Bool) +(assert (forall ((q0 Bool) (q1 Bool)) (xor true true q1 v4 q1 true true true true true true))) +(push 1) +(check-sat) +(pop 1) +(check-sat) -- 2.30.2