[SMT-LIB] How do I rewrite the following Simplify syntax into SMT-LIB?
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.
Keep in touch and up to date with friends and family. Make the connection now.
More information about the SMT-LIB