Patsolve_smt2

Google Group
1

I would like to announce the availability of patsolve_smt2 for turning ATS
constraints
into SMT-LIBv2 format:

https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/ATS-extsolve/ATS-extsolve-smt2

This implementation is largely based on some earlier piloting work by Will
Blair and Hanwen Wu.

Here is an example of some generated constraints in SMT-LIBv2 format:

;;;
;;;By [patsolve_smt2]:
;;;
(declare-sort s2rt_cls 0)
(declare-sort s2rt_eff 0)
(declare-sort s2rt_type 0)
(declare-sort s2rt_vtype 0)
(declare-sort s2rt_t0ype 0)
(declare-sort s2rt_vt0ype 0)
(declare-sort s2rt_prop 0)
(declare-sort s2rt_view 0)
(declare-sort s2rt_tkind 0)
(declare-sort s2rt_error 0)
(define-sort s2rt_int () Int)
(define-sort s2rt_addr () Int)
(define-sort s2rt_bool () Bool)
(define-sort file_mode () Int)
(define-fun unit_p () Bool true)
(define-fun s2exp_fun ((x Bool)) Bool x)
(define-fun s2exp_eqeq ((x Bool)) Bool x)
(define-fun s2exp_metdec ((x Bool)) Bool x)
(declare-fun s2exp_sizeof (s2rt_t0ype) Int)
(define-fun neg_int ((x Int)) Int (- x))
(define-fun abs_int ((x Int)) Int (abs x))
(define-fun add_int_int ((x Int) (y Int)) Int (+ x y))
(define-fun sub_int_int ((x Int) (y Int)) Int (- x y))
(define-fun mul_int_int ((x Int) (y Int)) Int (* x y))
(define-fun div_int_int ((x Int) (y Int)) Int (div x y))
(define-fun mod_int_int ((x Int) (y Int)) Int (mod x y))
(define-fun idiv_int_int ((x Int) (y Int)) Int (div x y))
(define-fun ndiv_int_int ((x Int) (y Int)) Int (div x y))
(define-fun eq_int_int ((x Int) (y Int)) Bool (= x y))
(define-fun lt_int_int ((x Int) (y Int)) Bool (< x y))
(define-fun gt_int_int ((x Int) (y Int)) Bool (> x y))
(define-fun lte_int_int ((x Int) (y Int)) Bool (<= x y))
(define-fun gte_int_int ((x Int) (y Int)) Bool (>= x y))
(define-fun neq_int_int ((x Int) (y Int)) Bool (not (= x y)))
(define-fun sgn_int ((x Int)) Int (ite (< x 0) -1 (ite (> x 0) 1 0)))
(define-fun max_int_int ((x Int) (y Int)) Int (ite (>= x y) x y))
(define-fun min_int_int ((x Int) (y Int)) Int (ite (<= x y) x y))
(define-fun null_addr () s2rt_addr 0)
(define-fun add_addr_int ((x s2rt_addr) (y Int)) s2rt_addr (+ x y))
(define-fun sub_addr_int ((x s2rt_addr) (y Int)) s2rt_addr (- x y))
(define-fun eq_addr_addr ((x s2rt_addr) (y s2rt_addr)) Bool (= x y))
(define-fun lt_addr_addr ((x s2rt_addr) (y s2rt_addr)) Bool (< x y))
(define-fun gt_addr_addr ((x s2rt_addr) (y s2rt_addr)) Bool (> x y))
(define-fun lte_addr_addr ((x s2rt_addr) (y s2rt_addr)) Bool (<= x y))
(define-fun gte_addr_addr ((x s2rt_addr) (y s2rt_addr)) Bool (>= x y))
(define-fun neq_addr_addr ((x s2rt_addr) (y s2rt_addr)) Bool (not (= x y)))
(define-fun true_bool () Bool true)
(define-fun false_bool () Bool false)
(define-fun neg_bool ((x Bool)) Bool (not x))
(define-fun add_bool_bool ((x Bool) (y Bool)) Bool (or x y))
(define-fun mul_bool_bool ((x Bool) (y Bool)) Bool (and x y))
(define-fun eq_bool_bool ((x Bool) (y Bool)) Bool (= x y))
(define-fun lt_bool_bool ((x Bool) (y Bool)) Bool (and (not x) y))
(define-fun gt_bool_bool ((x Bool) (y Bool)) Bool (and x (not y)))
(define-fun neq_bool_bool ((x Bool) (y Bool)) Bool (not (= x y)))
(define-fun lte_bool_bool ((x Bool) (y Bool)) Bool (or (not x) y))
(define-fun gte_bool_bool ((x Bool) (y Bool)) Bool (or x (not y)))
;;;
;;;emit_the_s2cstmap()
;;;
(declare-fun fact!745 (s2rt_int) s2rt_int)
(push)
(push)
(push)
(declare-fun n!3980 () s2rt_int)
(assert (gte_int_int n!3980 0))
(push)
(push)
(push)
(declare-fun n!3981 () s2rt_int)
(assert (gte_int_int n!3981 0))
(push)
(declare-fun r!3982 () s2rt_int)
(push)
(push)
(assert (not (gte_int_int n!3981 0)))
(echo “/home/hwxi/Research/ATS-Postiats-contrib/projects/MEDIUM/ATS-extsolve/ATS-extsolve-smt2/TEST/fact.dats:
352(line=33, offs=9) – 558(line=47, offs=2)”)
(check-sat)
(pop)
(pop)
(push)
(push)
(assert (eq_int_int n!3981 0))
(assert (eq_int_int (fact!745 0) 1))
(push)
(push)
(assert (not (s2exp_eqeq (= r!3982 (mul_int_int (fact!745 n!3981) r!3982
)))))
(echo “/home/hwxi/Research/ATS-Postiats-contrib/projects/MEDIUM/ATS-extsolve/ATS-extsolve-smt2/TEST/fact.dats:
455(line=41, offs=29) – 456(line=41, offs=30)”)
(check-sat)
(pop)
(pop)
(push)
(pop)
(pop)
(push)
(assert (neg_bool (eq_int_int n!3981 0)))
(push)
(push)
(assert (not (gt_int_int n!3981 0)))
(echo “/home/hwxi/Research/ATS-Postiats-contrib/projects/MEDIUM/ATS-extsolve/ATS-extsolve-smt2/TEST/fact.dats:
501(line=44, offs=14) – 512(line=44, offs=25)”)
(check-sat)
(pop)
(pop)
(assert (eq_int_int (fact!745 n!3981) (mul_int_int n!3981 (fact!745 (sub_int_int
n!3981 1)))))
(push)
(push)
(assert (not (s2exp_metdec (< (sub_int_int n!3981 1) n!3981))))
(echo “/home/hwxi/Research/ATS-Postiats-contrib/projects/MEDIUM/ATS-extsolve/ATS-extsolve-smt2/TEST/fact.dats:
522(line=44, offs=35) – 522(line=44, offs=35)”)
(check-sat)
(pop)
(pop)
(push)
(push)
(assert (not (gte_int_int (sub_int_int n!3981 1) 0)))
(echo “/home/hwxi/Research/ATS-Postiats-contrib/projects/MEDIUM/ATS-extsolve/ATS-extsolve-smt2/TEST/fact.dats:
522(line=44, offs=35) – 522(line=44, offs=35)”)
(check-sat)
(pop)
(pop)
(push)
(push)
(assert (not (s2exp_eqeq (= (mul_int_int (fact!745 (sub_int_int n!3981 1)) (mul_int_int
n!3981 r!3982)) (mul_int_int (fact!745 n!3981) r!3982)))))
(echo “/home/hwxi/Research/ATS-Postiats-contrib/projects/MEDIUM/ATS-extsolve/ATS-extsolve-smt2/TEST/fact.dats:
518(line=44, offs=31) – 532(line=44, offs=45)”)
(check-sat)
(pop)
(pop)
(push)
(pop)
(pop)
(pop)
(pop)
(pop)
(pop)
(push)
(push)
(assert (not (gte_int_int n!3980 0)))
(echo “/home/hwxi/Research/ATS-Postiats-contrib/projects/MEDIUM/ATS-extsolve/ATS-extsolve-smt2/TEST/fact.dats:
591(line=50, offs=7) – 591(line=50, offs=7)”)
(check-sat)
(pop)
(pop)
(push)
(push)
(assert (not (s2exp_eqeq (= (mul_int_int (fact!745 n!3980) 1) (fact!745 n!
3980)))))
(echo “/home/hwxi/Research/ATS-Postiats-contrib/projects/MEDIUM/ATS-extsolve/ATS-extsolve-smt2/TEST/fact.dats:
587(line=50, offs=3) – 597(line=50, offs=13)”)
(check-sat)
(pop)
(pop)
(pop)
(pop)
(pop)
(push)
(push)
(declare-fun n$849!3983 () s2rt_int)
(assert (gte_int_int n$849!3983 1))
(push)
(declare-fun i$887$888!4022 () s2rt_int)
(declare-fun i$893$894$895!4029 () s2rt_int)
(push)
(assert (gte_int_int n$849!3983 2))
(push)
(push)
(push)
(assert (not (lte_int_int 0 1)))
(echo “/home/hwxi/Research/ATS-Postiats-contrib/projects/MEDIUM/ATS-extsolve/ATS-extsolve-smt2/TEST/fact.dats:
726(line=62, offs=26) – 727(line=62, offs=27)”)
(check-sat)
(pop)
(pop)
(push)
(push)
(assert (not (lt_int_int 1 n$849!3983)))
(echo “/home/hwxi/Research/ATS-Postiats-contrib/projects/MEDIUM/ATS-extsolve/ATS-extsolve-smt2/TEST/fact.dats:
726(line=62, offs=26) – 727(line=62, offs=27)”)
(check-sat)
(pop)
(pop)
(pop)
(push)
(push)
(pop)
(pop)
(pop)
(push)
(assert (neg_bool (gte_int_int n$849!3983 2)))
(push)
(push)
(pop)
(pop)
(pop)
(push)
(assert (gte_int_int i$887$888!4022 0))
(push)
(push)
(push)
(assert (not (gte_int_int i$887$888!4022 0)))
(echo “/home/hwxi/Research/ATS-Postiats-contrib/projects/MEDIUM/ATS-extsolve/ATS-extsolve-smt2/TEST/fact.dats:
822(line=67, offs=25) – 823(line=67, offs=26)”)
(check-sat)
(pop)
(pop)
(pop)
(push)
(pop)
(pop)
(push)
(assert (neg_bool (gte_int_int i$887$888!4022 0)))
(push)
(push)
(push)
(assert (not (gte_int_int 0 0)))
(echo “/home/hwxi/Research/ATS-Postiats-contrib/projects/MEDIUM/ATS-extsolve/ATS-extsolve-smt2/TEST/fact.dats:
829(line=67, offs=32) – 830(line=67, offs=33)”)
(check-sat)
(pop)
(pop)
(pop)
(push)
(pop)
(pop)
(assert (gte_int_int i$893$894$895!4029 0))
(push)
(push)
(assert (not (gte_int_int i$893$894$895!4029 0)))
(echo “/home/hwxi/Research/ATS-Postiats-contrib/projects/MEDIUM/ATS-extsolve/ATS-extsolve-smt2/TEST/fact.dats:
889(line=69, offs=44) – 889(line=69, offs=44)”)
(check-sat)
(pop)
(pop)
(push)
(pop)
(pop)
(pop)
(pop)
(pop)

2

You can solve the above generated constraints using Z3.
You can also use cvc4, but some non-linear constraints are
not yet within the reach of cvc4.On Sunday, June 26, 2016 at 12:45:53 AM UTC-4, gmhwxi wrote:

I would like to announce the availability of patsolve_smt2 for turning ATS
constraints
into SMT-LIBv2 format:

https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/ATS-extsolve/ATS-extsolve-smt2

This implementation is largely based on some earlier piloting work by Will
Blair and Hanwen Wu.

Here is an example of some generated constraints in SMT-LIBv2 format:

;;;
;;;By [patsolve_smt2]:
;;;
(declare-sort s2rt_cls 0)
(declare-sort s2rt_eff 0)
(declare-sort s2rt_type 0)
(declare-sort s2rt_vtype 0)
(declare-sort s2rt_t0ype 0)
(declare-sort s2rt_vt0ype 0)
(declare-sort s2rt_prop 0)
(declare-sort s2rt_view 0)
(declare-sort s2rt_tkind 0)
(declare-sort s2rt_error 0)
(define-sort s2rt_int () Int)
(define-sort s2rt_addr () Int)
(define-sort s2rt_bool () Bool)
(define-sort file_mode () Int)
(define-fun unit_p () Bool true)
(define-fun s2exp_fun ((x Bool)) Bool x)
(define-fun s2exp_eqeq ((x Bool)) Bool x)
(define-fun s2exp_metdec ((x Bool)) Bool x)
(declare-fun s2exp_sizeof (s2rt_t0ype) Int)
(define-fun neg_int ((x Int)) Int (- x))
(define-fun abs_int ((x Int)) Int (abs x))
(define-fun add_int_int ((x Int) (y Int)) Int (+ x y))
(define-fun sub_int_int ((x Int) (y Int)) Int (- x y))
(define-fun mul_int_int ((x Int) (y Int)) Int (* x y))
(define-fun div_int_int ((x Int) (y Int)) Int (div x y))
(define-fun mod_int_int ((x Int) (y Int)) Int (mod x y))
(define-fun idiv_int_int ((x Int) (y Int)) Int (div x y))
(define-fun ndiv_int_int ((x Int) (y Int)) Int (div x y))
(define-fun eq_int_int ((x Int) (y Int)) Bool (= x y))
(define-fun lt_int_int ((x Int) (y Int)) Bool (< x y))
(define-fun gt_int_int ((x Int) (y Int)) Bool (> x y))
(define-fun lte_int_int ((x Int) (y Int)) Bool (<= x y))
(define-fun gte_int_int ((x Int) (y Int)) Bool (>= x y))
(define-fun neq_int_int ((x Int) (y Int)) Bool (not (= x y)))
(define-fun sgn_int ((x Int)) Int (ite (< x 0) -1 (ite (> x 0) 1 0)))
(define-fun max_int_int ((x Int) (y Int)) Int (ite (>= x y) x y))
(define-fun min_int_int ((x Int) (y Int)) Int (ite (<= x y) x y))
(define-fun null_addr () s2rt_addr 0)
(define-fun add_addr_int ((x s2rt_addr) (y Int)) s2rt_addr (+ x y))
(define-fun sub_addr_int ((x s2rt_addr) (y Int)) s2rt_addr (- x y))
(define-fun eq_addr_addr ((x s2rt_addr) (y s2rt_addr)) Bool (= x y))
(define-fun lt_addr_addr ((x s2rt_addr) (y s2rt_addr)) Bool (< x y))
(define-fun gt_addr_addr ((x s2rt_addr) (y s2rt_addr)) Bool (> x y))
(define-fun lte_addr_addr ((x s2rt_addr) (y s2rt_addr)) Bool (<= x y))
(define-fun gte_addr_addr ((x s2rt_addr) (y s2rt_addr)) Bool (>= x y))
(define-fun neq_addr_addr ((x s2rt_addr) (y s2rt_addr)) Bool (not (= x y
)))
(define-fun true_bool () Bool true)
(define-fun false_bool () Bool false)
(define-fun neg_bool ((x Bool)) Bool (not x))
(define-fun add_bool_bool ((x Bool) (y Bool)) Bool (or x y))
(define-fun mul_bool_bool ((x Bool) (y Bool)) Bool (and x y))
(define-fun eq_bool_bool ((x Bool) (y Bool)) Bool (= x y))
(define-fun lt_bool_bool ((x Bool) (y Bool)) Bool (and (not x) y))
(define-fun gt_bool_bool ((x Bool) (y Bool)) Bool (and x (not y)))
(define-fun neq_bool_bool ((x Bool) (y Bool)) Bool (not (= x y)))
(define-fun lte_bool_bool ((x Bool) (y Bool)) Bool (or (not x) y))
(define-fun gte_bool_bool ((x Bool) (y Bool)) Bool (or x (not y)))
;;;
;;;emit_the_s2cstmap()
;;;
(declare-fun fact!745 (s2rt_int) s2rt_int)
(push)
(push)
(push)
(declare-fun n!3980 () s2rt_int)
(assert (gte_int_int n!3980 0))
(push)
(push)
(push)
(declare-fun n!3981 () s2rt_int)
(assert (gte_int_int n!3981 0))
(push)
(declare-fun r!3982 () s2rt_int)
(push)
(push)
(assert (not (gte_int_int n!3981 0)))
(echo “/home/hwxi/Research/ATS-Postiats-contrib/projects/MEDIUM/ATS-extsolve/ATS-extsolve-smt2/TEST/fact.dats:
352(line=33, offs=9) – 558(line=47, offs=2)”)
(check-sat)
(pop)
(pop)
(push)
(push)
(assert (eq_int_int n!3981 0))
(assert (eq_int_int (fact!745 0) 1))
(push)
(push)
(assert (not (s2exp_eqeq (= r!3982 (mul_int_int (fact!745 n!3981) r!3982
)))))
(echo “/home/hwxi/Research/ATS-Postiats-contrib/projects/MEDIUM/ATS-extsolve/ATS-extsolve-smt2/TEST/fact.dats:
455(line=41, offs=29) – 456(line=41, offs=30)”)
(check-sat)
(pop)
(pop)
(push)
(pop)
(pop)
(push)
(assert (neg_bool (eq_int_int n!3981 0)))
(push)
(push)
(assert (not (gt_int_int n!3981 0)))
(echo “/home/hwxi/Research/ATS-Postiats-contrib/projects/MEDIUM/ATS-extsolve/ATS-extsolve-smt2/TEST/fact.dats:
501(line=44, offs=14) – 512(line=44, offs=25)”)
(check-sat)
(pop)
(pop)
(assert (eq_int_int (fact!745 n!3981) (mul_int_int n!3981 (fact!745 (sub_int_int
n!3981 1)))))
(push)
(push)
(assert (not (s2exp_metdec (< (sub_int_int n!3981 1) n!3981))))
(echo “/home/hwxi/Research/ATS-Postiats-contrib/projects/MEDIUM/ATS-extsolve/ATS-extsolve-smt2/TEST/fact.dats:
522(line=44, offs=35) – 522(line=44, offs=35)”)
(check-sat)
(pop)
(pop)
(push)
(push)
(assert (not (gte_int_int (sub_int_int n!3981 1) 0)))
(echo “/home/hwxi/Research/ATS-Postiats-contrib/projects/MEDIUM/ATS-extsolve/ATS-extsolve-smt2/TEST/fact.dats:
522(line=44, offs=35) – 522(line=44, offs=35)”)
(check-sat)
(pop)
(pop)
(push)
(push)
(assert (not (s2exp_eqeq (= (mul_int_int (fact!745 (sub_int_int n!3981 1))
(mul_int_int n!3981 r!3982)) (mul_int_int (fact!745 n!3981) r!3982)))))
(echo “/home/hwxi/Research/ATS-Postiats-contrib/projects/MEDIUM/ATS-extsolve/ATS-extsolve-smt2/TEST/fact.dats:
518(line=44, offs=31) – 532(line=44, offs=45)”)
(check-sat)
(pop)
(pop)
(push)
(pop)
(pop)
(pop)
(pop)
(pop)
(pop)
(push)
(push)
(assert (not (gte_int_int n!3980 0)))
(echo “/home/hwxi/Research/ATS-Postiats-contrib/projects/MEDIUM/ATS-extsolve/ATS-extsolve-smt2/TEST/fact.dats:
591(line=50, offs=7) – 591(line=50, offs=7)”)
(check-sat)
(pop)
(pop)
(push)
(push)
(assert (not (s2exp_eqeq (= (mul_int_int (fact!745 n!3980) 1) (fact!745 n!
3980)))))
(echo “/home/hwxi/Research/ATS-Postiats-contrib/projects/MEDIUM/ATS-extsolve/ATS-extsolve-smt2/TEST/fact.dats:
587(line=50, offs=3) – 597(line=50, offs=13)”)
(check-sat)
(pop)
(pop)
(pop)
(pop)
(pop)
(push)
(push)
(declare-fun n$849!3983 () s2rt_int)
(assert (gte_int_int n$849!3983 1))
(push)
(declare-fun i$887$888!4022 () s2rt_int)
(declare-fun i$893$894$895!4029 () s2rt_int)
(push)
(assert (gte_int_int n$849!3983 2))
(push)
(push)
(push)
(assert (not (lte_int_int 0 1)))
(echo “/home/hwxi/Research/ATS-Postiats-contrib/projects/MEDIUM/ATS-extsolve/ATS-extsolve-smt2/TEST/fact.dats:
726(line=62, offs=26) – 727(line=62, offs=27)”)
(check-sat)
(pop)
(pop)
(push)
(push)
(assert (not (lt_int_int 1 n$849!3983)))
(echo “/home/hwxi/Research/ATS-Postiats-contrib/projects/MEDIUM/ATS-extsolve/ATS-extsolve-smt2/TEST/fact.dats:
726(line=62, offs=26) – 727(line=62, offs=27)”)
(check-sat)
(pop)
(pop)
(pop)
(push)
(push)
(pop)
(pop)
(pop)
(push)
(assert (neg_bool (gte_int_int n$849!3983 2)))
(push)
(push)
(pop)
(pop)
(pop)
(push)
(assert (gte_int_int i$887$888!4022 0))
(push)
(push)
(push)
(assert (not (gte_int_int i$887$888!4022 0)))
(echo “/home/hwxi/Research/ATS-Postiats-contrib/projects/MEDIUM/ATS-extsolve/ATS-extsolve-smt2/TEST/fact.dats:
822(line=67, offs=25) – 823(line=67, offs=26)”)
(check-sat)
(pop)
(pop)
(pop)
(push)
(pop)
(pop)
(push)
(assert (neg_bool (gte_int_int i$887$888!4022 0)))
(push)
(push)
(push)
(assert (not (gte_int_int 0 0)))
(echo “/home/hwxi/Research/ATS-Postiats-contrib/projects/MEDIUM/ATS-extsolve/ATS-extsolve-smt2/TEST/fact.dats:
829(line=67, offs=32) – 830(line=67, offs=33)”)
(check-sat)
(pop)
(pop)
(pop)
(push)
(pop)
(pop)
(assert (gte_int_int i$893$894$895!4029 0))
(push)
(push)
(assert (not (gte_int_int i$893$894$895!4029 0)))
(echo “/home/hwxi/Research/ATS-Postiats-contrib/projects/MEDIUM/ATS-extsolve/ATS-extsolve-smt2/TEST/fact.dats:
889(line=69, offs=44) – 889(line=69, offs=44)”)
(check-sat)
(pop)
(pop)
(push)
(pop)
(pop)
(pop)
(pop)
(pop)