Re: patsolve_smt2

[gmhwxi]

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)
>
>
>
>
>

-- 
You received this message because you are subscribed to the Google Groups 
"ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to ats-lang-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/060e6e73-5e21-4508-a97c-5de531ffba14%40googlegroups.com.