Minor fixes for partial quantifier elimination. (#1147)

This forces "counterexample lemmas" (the formula B => ~phi[e] on page 23 of http://homepage.divms.uiowa.edu/~ajreynol/fmsd17-instla.pdf) to be added during TheoryQuantifiers::preRegisterTerm instead of at full effort check. This is required to ensure that CVC4's partial quantifier elimination algorithm produces correct results.

Some background:

"get-qe" and "get-qe-disjunct" are commands in the SMT2 parser. Here is how they can be used:

[declarations]
[assertions A]
(get-qe (exists X F))

returns a ground formula F' such that A ^ F' and A ^ (exists X F) are equivalent.

The command "get-qe-disjunct" provides an interface for doing an incremental version of "get-qe".

[declarations]
[assertions A]
(get-qe-disjunct (exists X F))

returns a ground formula F1' such that A ^ F' implies A ^ (exists X F). It moreover has the property that if you call:

[declarations]
[assertions A]
(assert F1')
(get-qe-disjunct (exists X F))

this will give you a formula F2' where eventually:

[declarations]
[assertions A]
(assert (not (or F1' ... Fn')))
(get-qe-disjunct (exists X F))

will either return "true" or "false", for some finite n.

Here is an example that failed before this commit:

(set-logic LIA)
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(assert (or (not (>= (+ a (* (- 1) b)) 1)) (not (>= (+ c (* (- 1) d)) 0))))
(get-qe-disjunct (exists ((x Int)) (and (> a b) (> c x) (> d x))))

This should return:

(not (or (not (>= (+ a (* (- 1) b)) 1)) (>= (+ c (* (- 1) d)) 1)))

Previously it was returning:

false

This is because the cbqi algorithm needs to assume the negation of the quantified formula we are doing qe on before it makes any decision.

The get-qe-partial feature is being requested by Cesare and Daniel Larraz for Kind2.

This improves our performance on quantified LIA/LRA:
https://www.starexec.org/starexec/secure/details/job.jsp?id=24480
see CVC4-092617-2-fixQePartial

diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index 8e53c97dc753e46c03c78e1ed28783bdaaddc0b7..34758c4316c1f09ac3e5ab734808deabc6053386 100644 (file)
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -167,10 +167,8 @@ void InstStrategyCbqi::reset_round( Theory::Effort effort ) {
     Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
     //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine
     if( doCbqi( q ) ){
-      if( registerCbqiLemma( q ) ){
-        Debug("cbqi-debug") << "Registered cbqi lemma." << std::endl;
-      //set inactive the quantified formulas whose CE literals are asserted false
-      }else if( d_quantEngine->getModel()->isQuantifierActive( q ) ){
+      Assert( hasAddedCbqiLemma( q ) );
+      if( d_quantEngine->getModel()->isQuantifierActive( q ) ){
         d_active_quant[q] = true;
         Debug("cbqi-debug") << "Check quantified formula " << q << "..." << std::endl;
         Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q );
@@ -373,7 +371,11 @@ void InstStrategyCbqi::preRegisterQuantifier( Node q ) {
 }
 
 void InstStrategyCbqi::registerQuantifier( Node q ) {
-
+  if( doCbqi( q ) ){
+    if( registerCbqiLemma( q ) ){
+      Trace("cbqi") << "Registered cbqi lemma for quantifier : " << q << std::endl;
+    }
+  }
 }
 
 Node InstStrategyCbqi::doNestedQENode( Node q, Node ceq, Node n, std::vector< Node >& inst_terms, bool doVts ) {
@@ -553,6 +555,7 @@ bool InstStrategyCbqi::doCbqi( Node q ){
   if( it==d_do_cbqi.end() ){
     int ret = 2;
     if( !d_quantEngine->getTermDatabase()->isQAttrQuantElim( q ) ){
+      Assert( !d_quantEngine->getTermDatabase()->isQAttrQuantElimPartial( q ) );
       //if has an instantiation pattern, don't do it
       if( q.getNumChildren()==3 && options::eMatching() && options::userPatternsQuant()!=USER_PAT_MODE_IGNORE ){
         for( unsigned i=0; i<q[2].getNumChildren(); i++ ){
@@ -776,11 +779,15 @@ CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) {
 }
 
 void InstStrategyCegqi::registerQuantifier( Node q ) {
-  if( options::cbqiPreRegInst() ){
-    if( doCbqi( q ) ){
-      //just get the instantiator
+  if( doCbqi( q ) ){
+    // get the instantiator  
+    if( options::cbqiPreRegInst() ){
       getInstantiator( q );
     }
+    // register the cbqi lemma
+    if( registerCbqiLemma( q ) ){
+      Trace("cbqi") << "Registered cbqi lemma for quantifier : " << q << std::endl;
+    }
   }
 }
 

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index fd831001f1937d896b556d773036a41cf5352533..8649c7bddbe59f5ebdf29c5d030bd5cc24ce9ca0 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -741,6 +741,8 @@ bool QuantifiersEngine::registerQuantifier( Node f ){
       //}
       Trace("quant-debug")  << "...finish." << std::endl;
       d_quants[f] = true;
+      // flush lemmas
+      flushLemmas();
       return true;
     }
   }else{