# 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.