Search code examples
z3smttheorem-proving

Is there a way to use SMT solvers for finding out how to compose functions?

I am a beginner to SMT solvers and I am trying to use them for a variation on program synthesis. Anyway, what the problem boils down to is find a sequence of applied operations (composition of previously defined functions) which for the given input gives the requested output.

Is there any existing practice of using SMT solvers for finding out in which order to compose functions in order to reach a specific output? If you have any reading material for me I am happy to read up.

I began using Z3 for the task, but if there is any reasoning to choose other SMT solvers, shoot!

Thanks.

Solution

  • You'll need to define constants that describe what operations are to be applied. First, define a compound operation that switches based on what operation to use:

    int operation; //constant, constrain it to [0, 2]
Expr result =
 operation == 0 ? applyFunction0(inputExpr) :
 operation == 1 ? applyFunction1(inputExpr) :
 applyFunction2(inputExpr);

    Very rough pseudo code for what expression to build. The ?: operator maps to ITE in Z3.

    That way Z3 can find a suitable value for operation to pick one concrete operation. You can obtain the concrete value from the model.

    You can iterate this approach to apply multiple operations in sequence.