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

[Yeting Ge]

Hi Ewa,

A similar function could be defined in SMT pretty much like in Simplify. 
For example:


(benchmark quant
:source {internet}
:logic AUFLIA
:extrafuns ((fac Int Int))
:assumption
(and (= (fac 1) 1) (forall (?x Int) (implies (> ?x 1) (= (fac ?x) (* (fac 
(- ?x 1)) ?x)))))
:formula
(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.
> http://www.microsoft.com/windows/windowslive/
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>

Thank you,
Yeting