search

kino-mc / rsmt2

A generic library to interact with SMT-LIB 2 compliant solvers running in a separate system process, such as Z3 and CVC4.
Apache License 2.0
65 stars 14 forks source link

Mark CVC4 as supporting check-sat-assuming #38

Open tchajed opened 1 year ago

tchajed commented 1 year ago

It looks like CVC4 does now support check-sat-assuming, as of https://github.com/cvc5/cvc5/pull/1637. This PR adds support for it and adds a test using activation literals.

Here's a small test file that CVC4 correctly produces unsat for:

; Command:
; > z3 -in -smt2

(set-logic ALL)

(declare-fun p ( 
) Bool)

(declare-fun q ( 
) Bool)

(assert
    (and (not p) (not q) (and (= p (or p q)) (= q q)))
)

(declare-fun |rsmt2 actlit 0| () Bool)

(assert (=> |rsmt2 actlit 0|
    (not (not p))
))

(check-sat-assuming (
 |rsmt2 actlit 0|
) )

(assert (not |rsmt2 actlit 0|) )

(assert
    (not p)
)
AdrienChampion commented 1 year ago

You mean cvc5 right?

If that's the case, then your PR should probably be rewritten as adding a new cvc5 driver if that's not too much trouble 🐱

tchajed commented 1 year ago

I actually did mean CVC4. I can't find it in a changelog but the commit goes back to March 2018 and it was already in CVC4 1.6.

I've also been using CVC5 by just using the CVC4 driver with "cvc5" as the binary name; I haven't tested all that much but so far it has been compatible.