Quantifier Instantiation Techniques (defaults and composition)

[thedotmatrix]

For the following total & one-to-one (scalar-sort -> Int) function assertion:

(set-logic ALL)
(declare-datatypes ((Device 0)) 
  (((heat) (thermo) (pc) (phone) (internet))))
(define-sort Interface () Int)
(declare-fun connected (Device) Interface)
(assert (forall ((d Device)) ;; total
  (exists ((i Interface)) (= (connected d) i))))
(assert (forall ((dA Device) (dB Device)) ;; one-to-one
  (=> (not (= dA dB)) 
      (not (= (connected dA) (connected dB))))))
(check-sat)
(get-model)

The latest release can prove and find a model:

$ cvc4 --version
This is CVC4 version 1.6
compiled with GCC version 7.3.0
on Sep 27 2018 13:46:13
...
$ cvc4 -im bug.smt2 
sat
(model
(declare-datatypes ((Device 0)) (((heat) (thermo) (pc) (phone) (internet))))
(define-fun connected ((BOUND_VARIABLE_850 Device)) Int (ite (= internet BOUND_VARIABLE_850) 3 (ite (= phone BOUND_VARIABLE_850) 2 (ite (= pc BOUND_VARIABLE_850) 1 (ite (= thermo BOUND_VARIABLE_850) (- 1) 0)))))
)

But the current pre-release HEAD cannot:

$ cvc4 --version
This is CVC4 version 1.7-prerelease [git master 23f51f71]
compiled with GCC version 7.3.0
on Sep 19 2018 13:55:00
...
$ cvc4 -im bug.smt2 
unknown
(model
(declare-datatypes ((Device 0)) (((heat) (thermo) (pc) (phone) (internet))))
(define-fun connected ((BOUND_VARIABLE_337 Device)) Int 0)
)

Your issue section of the README didn't specify if you only want bug reports on the latest stable build, so hopefully this is informative. Thanks!

[ajreynol]

Hello, thanks for the benchmark.

The default behavior of CVC4 has changed in the latest master, in particular, quantified formulas over small domains are not expanded by default.

If you are interested in using CVC4 for answer "sat" for problems like this one, I recommend using its finite model finding mode, enabled by: --fmf-bound With this, CVC4 quickly answers "sat" for the given benchmark.

CVC4 uses techniques from this paper when in the mode: http://homepage.divms.uiowa.edu/~ajreynol/cade24.pdf

Hope this helps, Andy

[thedotmatrix]

Thanks for the pointing out the proper fmf option for solving these problems now that the default has changed!

Does --fmf-bound just turn on finite model finding only on bounded quantification (works here because the datatype is finite), or for all quantification?

More generally, could you clarify how these modes can/cannot be composed, specifically for the quantifiers module? After reading how MCSAT/mbqi progressed (http://theory.stanford.edu/~barrett/pubs/RTJ+17.pdf), and the recent cegis/sygus work (http://theory.stanford.edu/~barrett/pubs/RDK+15.pdf), I was under the impression many of these techniques are at least compatible, if not composable. Is there a good rule of thumb here, such as only the techniques with a -interleave option can be composed?

Thanks again for the help!

[ajreynol]

--fmf-bound works on a variety of quantified formulas where bounds can be inferred, including (small) finite types, (symbolic) integer ranges, bounded set membership (e.g. forall x. x in S => P( x )). It enables a superset of the techniques enabled by --finite-model-find, which is capable of handling quantified formulas over uninterpreted sorts.

The above options enable what we call "model-based quantifier instantiation", whose main advantage is that it allows us to answer "sat" for inputs with quantified formulas. This instantiation technique can be combined with other techniques such as E-matching (by using option --fmf-inst-engine), and is combined by default with "conflict-based instantiation" (http://homepage.divms.uiowa.edu/~ajreynol/fmcad14.pdf).

The sygus work from http://theory.stanford.edu/~barrett/pubs/RDK+15.pdf is split into two techniques. The first synthesis technique in that paper, "counterexample-guided quantifier instantiation" is the default strategy for solving quantified formulas that are purely in LIA, LRA, and BV. The second technique from the paper is mostly disjoint from the above techniques, and is enabled only on sygus *.sy inputs.

For more details on how all of these combine, you can see these slides: http://homepage.divms.uiowa.edu/~ajreynol/pres-smt2017-ajr.pdf

The techniques from http://theory.stanford.edu/~barrett/pubs/RTJ+17.pdf describe the quantifier-free theory solvers of CVC4 (e.g. non-linear arithmetic and strings), which are also model-based. These are indeed composable with techniques for quantified formulas in CVC4.

[thedotmatrix]

Incredibly helpful, especially the slides. Thank you again for your time.