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

1 files changed, 2 insertions, 0 deletions

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index fd831001f..8649c7bdd 100644
--- 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{