class
Z3::Optimize
- Z3::Optimize
- Reference
- Object
Overview
A solver with objectives. Everything Solver does with assertions it does too,
plus #maximize, #minimize and #assert_soft - soft constraints being the ones
Z3 is allowed to break, paying their weight when it does, which is MaxSAT.
Z3's objective value readers aren't bound, so read the maximised term out of the
model rather than expecting one from #maximize, which answers the objective's
index the way Z3 does.
Included Modules
Defined in:
z3/optimize.crConstructors
Instance Method Summary
- #assert(expr)
-
#assert_and_track(expr, tracker)
trackeris a Bool const standing in forexpr, and it's what shows up in#unsat_coreif the solver blames this assertion -
#assert_soft(expr, weight : String = "1")
A constraint Z3 may break, at the cost of
weight. - #assertions
- #check(*assumptions) : CheckResult
- #from_file(path : String)
-
#from_string(str : String)
Parses SMT-LIB2 and adds its assertions on top of whatever's already asserted, the same way
Solver#from_stringdoes - except that this parser knows(maximize ...),(minimize ...)and(assert-soft ...)too, so a string can bring objectives along with its assertions. - #help
- #maximize(expr)
- #minimize(expr)
- #model
-
#pop
Z3's optimizer pops one scope at a time, unlike a Solver
- #push
- #reason_unknown
-
#set_initial_value(var : AnyExpr, value)
A hint at which value to try for a variable first, the same warm start
Solver.simpletakes - but Bool and Bitvec only. - #statistics
- #to_s(io)
- #to_unsafe : LibZ3::Optimize
- #unsat_core
Instance methods inherited from module Z3::Checkable
prove!(claim : BoolExpr, io : IO = STDOUT) : Nil
prove!,
satisfiable?(*assumptions) : Bool
satisfiable?,
unsatisfiable?(*assumptions) : Bool
unsatisfiable?
Constructor Detail
Instance Method Detail
tracker is a Bool const standing in for expr, and it's what shows up in
#unsat_core if the solver blames this assertion
A constraint Z3 may break, at the cost of weight. The weight is a String
because that's Z3's own interface to it.
Parses SMT-LIB2 and adds its assertions on top of whatever's already asserted,
the same way Solver#from_string does - except that this parser knows
(maximize ...), (minimize ...) and (assert-soft ...) too, so a string can
bring objectives along with its assertions.
A hint at which value to try for a variable first, the same warm start
Solver.simple takes - but Bool and Bitvec only.
Z3's optimizer gets arithmetic ones wrong in both directions: an Int hint is
dropped by its elim_01 preprocessing before the search ever sees it, and a Real
hint which does arrive comes back out of that preprocessing scaled, so an Optimize
with an objective can answer with a model that fails its own assertions. Those two
raise here rather than being passed through; Solver.simple honours arithmetic
warm starts correctly and is where one belongs until Z3 is fixed.