search

Z3Prover / z3

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

Cannot found `check-sat-using` in ML api #1273

Closed sangwoo-joh closed 7 years ago

sangwoo-joh commented 7 years ago

I'm trying to use check-sat-using command in OCaml, but I cound not find such api function in z3.mli. What I'm trying to do is (check-sat-using (using-params smt :random-seed 1)). Is there any support for check-sat-using in api? Or, if not, is there any plan to support this?

sangwoo-joh commented 7 years ago

I found https://github.com/Z3Prover/z3/blob/bba005154c2c753f0da108e39eb6abac2b3c7640/src/api/ml/z3.mli#L3243, and maybe is this check-sat-using for Z3 solver? This api function consists of Z3_mk_solver_from_tactic. But I could not found in Z3 optimizer, neither a function like Z3_mk_optimize_from_tactic.

NikolajBjorner commented 7 years ago

It is correct that check-sat-using corresponds to taking a tactic and either applying it directly to check satisfiability or to extract a solver object and then use that.

The Z3_optimizer objects have no integration with tactics. This is due to the somewhat specialized way that optimization is handled in Z3 and few tactics would be able to interoperate with optimization in the current form.

sangwoo-joh commented 7 years ago

@NikolajBjorner Thank you for your replying. 1) So, is there no way to interoprate Z3 optimizer with tactics in any API? 2) By Z3 binary with a SMT2-format input file, I was able to use (check-sat-using (using-params smt :random-seed 1)) command with some assert-softs(i.e. the optimizer). Is this because the way Z3 binary works differs from the way api works internally? I'm confused.

NikolajBjorner commented 7 years ago
  1. there is no way
  2. check-sat-using from the command-line ignores soft constraints and optimization objectives.
sangwoo-joh commented 7 years ago

Thank you!