From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 15 Sep 2020 02:58:08 +0000 (-0500)
Subject: Fix needsModel method for CEGQI (#5048)
X-Git-Tag: cvc5-1.0.0~2863
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4a1b5ea5568fb6c688f407946f9a7fbb1cec3c31;p=cvc5.git

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 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 */
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)