[SMT-LIB] How do I rewrite the following Simplify syntax into SMT-LIB?
yeting at courant.nyu.edu
Sat Jan 17 10:19:15 EST 2009
A similar function could be defined in SMT pretty much like in Simplify.
:extrafuns ((fac Int Int))
(and (= (fac 1) 1) (forall (?x Int) (implies (> ?x 1) (= (fac ?x) (* (fac
(- ?x 1)) ?x)))))
(not (= (fac 5) 120)))
The difference is a function must be declared by using :extrafuns before
it can be used, and satisfiability is checked in SMT.
On Fri, 16 Jan 2009, Ewa Rom wrote:
> I know Simplify and in Simplify syntax I can create recursive functions such as:(BG_PUSH (EQ (factorial 1) 1))
> (BG_PUSH (FORALL (n ) (IMPLIES (> n 1) (EQ (factorial n) (* (factorial (- n 1)) n)))))
> (EQ (factorial 5) 120)When I feed Z3 with Simplify syntax it returns Valid.I would like to use SMT-LIB format with Z3.How can I rewrite this in SMT-LIB format?I looked into the smt-lib standard document and I see :funs and :extrafuns, but I cannot figure out how to define these functions.
> Thank you
> Ewa Romanowicz
> Keep in touch and up to date with friends and family. Make the connection now.
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
More information about the SMT-LIB