[SMT-LIB] How do I rewrite the following Simplify syntax into SMT-LIB?

Ewa Rom ewuniar2 at hotmail.com
Fri Jan 16 21:49:28 EST 2009

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.

More information about the SMT-LIB mailing list