How to write a function in PySMT?

[sy...@mics.snu.ac.kr]

I saw the manual about the function usage.

    pysmt.shortcuts.Function(vname, params)

But I have no idea about how to use it. Can I get any simple example implementation?

Thank you

   

[Andrea Micheli]

Hello,

The Function shortcut creates an uninterpreted function application (i.e. you are asking the solver to find an interpretation for the function that satisfies the formula).

For example:

ftype1 = FunctionType(REAL, [REAL]) # Create the function type real -> real

ftype2 = FunctionType(REAL, [REAL, INT]) # Create the function type real -> int -> real

f = Symbol("f", ftype1) # Create a function f that maps reals to reals

g = Symbol("g", ftype2) # Create a function g that maps pairs of reals * int to reals

check = Equals(Function(f, [Real(1)]), Function(g, (Real(2), Int(4))) # f(1) = g(2.0, 4)

check_sat(check) # returns true, because it is possible to construct a function f and a function g respecting the constraints

check2 = And(check, Equals(Function(f, [Real(1)]), Real(2)), Equals(Function(g, (Real(2), Int(4)), Real(3)) # f(1.0) = g(2.0, 4) & f(1.0) = 2.0 & g(2.0, 4) = 3.0

check_sat(check2) # returns false, because it is not possible to construct a function f and a function g respecting the constraints

Have a look at the file https://github.com/pysmt/pysmt/blob/master/pysmt/test/test_euf.py for other usage examples.

Hope this helps,

Andrea

--
You received this message because you are subscribed to the Google Groups "pySMT" group.
To unsubscribe from this group and stop receiving emails from it, send an email to pysmt+un...@googlegroups.com.
To post to this group, send email to py...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/pysmt/d9fe6df7-710c-4943-8fe1-ca9255a701db%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Seyoung Kim]

Thank you for your answer.

That's exactly what I wanted to know.

In addition I have one more question.

In Z3, there is a way to define a function which has a explicit relationship (not like uninterpreted function) like macro as below.

Is there any way to write this kind of function or macro in PySMT?

(define-fun my-or ((x Bool) (y Bool)) Bool (or x y))

[Andrea Micheli]

Since pysmt is a library you have no need for smtlib's define-fun,

you can simply create a python function returning a formula and use it while creating other formulae.

For example:

def my_or(x, y):

    return Or(x, y)

f = And(Symbol("a"), my_or(Symbol("b"), Symbol("c"))

Note that this is equivalent also performance-wise with smtlib's define-fun because pysmt internally memoizes all syntactically-equivalent formulae.

Hope this helps,

Andrea

[Seyoung Kim]

Yes I understood. It helps a lot.

Thanks

2018년 10월 22일 (월) 오후 5:26, Andrea Micheli <micheli...@gmail.com>님이 작성:

To view this discussion on the web visit https://groups.google.com/d/msgid/pysmt/CACbX7pc9SY%2BJeOK%3DGEBDyjJwYp9Lfw%3DVuv%2BKbwC90KDz5j7u2A%40mail.gmail.com.