CODEWITHSUNDEEP
z3smt
Cristian Petrescu-Prahova
Cristian Petrescu-Prahova

Reputation: 157

What is Z3's default solver?

[Novice]. According to http://rise4fun.com/Z3/tutorialcontent/strategies, 'smt' is the main tactic on Z3. However, using it explicitly breaks even for trivial problems. How can one reference the default Z3 solver in a tactic sequence?

http://rise4fun.com/Z3/K8nn

(declare-fun var1 () Real)
(assert (= (* var1 var1) 9.0))
(assert (< var1 0.0))
; Works
;(check-sat)
;(get-model)
; Breaks
(check-sat-using smt)
(get-info :reason-unknown)

Upvotes: 2

Views: 880

Answers (1)

Christoph Wintersteiger
Christoph Wintersteiger

Reputation: 8393

By default, Z3 will look into your formula to determine which features and logics are required and it will then call a suitable solver/tactic. You can provide a (set-logic ...) command to steer it, or you can directly use one of those default tactics. For a list of SMT logics for which Z3 has custom tactics, see default_tactic.cpp. If none of them matches and no logic is selected, "smt" is the tactic that will be executed.

To see which tactics are run, add -v:10 to the command line, and Z3 will print the tactics names and statistics as they are being executed.

For this type of non-linear reals the "smt" tactic is not very strong and it will give up quickly and return "unknown". But, it isn't the default tactic for this type of problem; instead (after some preprocessing) it is the "nlsat" tactic that solves the problem, as called via the default tactic for QF_NRA (see qfnra.cpp).

Upvotes: 7

Related Questions