Local theory extensions in SMT

Solver options for E-matching

For CVC4, default options use E-matching (use latest development builds here). For Z3, use following command line arguments: auto_config=false smt.mbqi=false smt.ematching=true.

The solver's unkonwn answer should be treated as sat (TODO: add instructions for seeing set of instantiations made by solver).

Local theory example

SMT2 file for example in section 2 of paper.

(set-logic UFLIA)
(declare-fun f (Int) Int)
(declare-fun a () Int)
(declare-fun b () Int)
(assert (forall ((x Int) (y Int)) (! (=> (<= x y) (<= (f x) (f y))) :pattern ((f x) (f y)))))
(assert (= (+ a b) 1))
(assert (= (+ (f a) (f b)) 0))
(check-sat)

Psi-local theory example

SMT2 file for example in section 5 of paper.

(set-logic UF)
(declare-sort X 0)
(declare-sort Y 0)
(declare-fun f (X) Y)
(declare-fun g (Y) X)
(declare-fun a () X)
(declare-fun b () X)
(assert (forall ((x X) (y Y)) (! (=> (= (f x) y) (= (g y) x)) :pattern ((f x) (g y)))))
(assert (= (f a) (f b)))
(assert (not (= a b)))
;; For Z3 uncomment following line
;(declare-fun inst-closure (X) Bool)
(assert (inst-closure (g (f a))))
(assert (inst-closure (g (f b))))
(check-sat)

Benchmarks in experiments

For more interesting local theory extension benchmarks, see the details in the CAV artifact.

More

You can reach me at kshitij AT cs DOT nyu DOT edu if you need more details, or if you are unable to get these / your own examples working.