2

Using Z3 with the textual format, I can use define-fun to define functions for reuse later on. For example:

 （define-fun test((a Int) (b Int)) Int
      （ite  (and (> a 2) (<= b 3))
             1
             (ite （and (<= a 2)(> b 10))
                  2
                  a
             )
       )
  ）

so I wonder how to define fun using C# api, since Context.MkFuncDecl is used to generate uninterpreted functions only.

  • I have asked exactly the same question before: http://stackoverflow.com/questions/7740556/equivalent-of-define-fun-in-z3-api – pad Jun 28 '12 at 07:18
  • it seems that there is new C# api, I am wondering is there any direct method to define fun not by quantifiers? –  Jun 28 '12 at 07:19

1 Answers1

2

define-fun is just a mechanism for defining macros in SMT 2.0. It does not add any power to SMT solvers. We do support it in the API, since the user can create a function that implements the macro in its favorite language. That is, we can create a C# function called test that given a and b return the ite expression in your question. Here is an example on how to do it in Python:

http://rise4fun.com/Z3Py/to1

Here is another example that define a min function that receives arbitrary number of arguments:

http://rise4fun.com/Z3Py/Vvp

Leonardo de Moura
  • 21,065
  • 2
  • 47
  • 53
  • Thanks, I have solved the problem. However, there is another problem, you can about the quantifier and fixedpoint, http://stackoverflow.com/questions/11264914/an-error-appears-when-running-exist-quantifier-and-fixedpoint-z3-in-c-sharp would you pls help me? –  Jun 29 '12 at 15:52