search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.26k stars 1.48k forks source link

macro-finder in C API #400

Closed nuppt closed 8 years ago

nuppt commented 8 years ago

I use C API to declare a function and assert by a quantification which can represent as definition of the function. Then, I want to use an option in C API that behaved as macro-finder option in smt2 interface. But I cannot find any in C API. So how can I do that?

wintersteiger commented 8 years ago

The easiest way to do that is to set up a goal with your constraints and then apply the tactic called 'macro-finder'. It may be helpful to also apply the simplify tactic before that.

nuppt commented 8 years ago

Thanks, wintersteiger. It's very useful. Before this, I just only use check_sat function in C API,which handle Z3_ast as argument to check satisfiability of a formula. As your suggestion, I will try solver in C API, and use macro-finder tactic.