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.

diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index ab1bb16b5dd7b5c47e6c740ccea1cec5becb01bc..d16024ee37df31e47b6948a78b2fa627431c9752 100644 (file)
--- 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 61eb4ff3918a2b79eff2109469142cf0db4bc8a6..51ca919bbc0383f1944cd0e42883d47054cb390e 100644 (file)
--- 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 bdf6d06073b354cf1c32575d8e091422fe2bb5a3..b35bd6447ddc7e91bde7f36c0b986c7dbd5f580c 100644 (file)
--- 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 ef09813725b37ba7c92ae39fe7758215658bde52..9e1480852ef5b4771e698aee29c417f6b8e3045b 100644 (file)
--- 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 (file)
index 0000000..85c59db
--- /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)