Z3::Solver
Inherits Z3::Checkable < Reference < Object
Constructors
solver is how the alternative constructors below pass in their own, and
simple says which kind it is, because Z3 offers no way to ask one - see
#simple?. Solver.new is the general purpose one and you almost always want it:
it inspects the assertions and assembles a tactic to match them.
Class methods
Specializes the solver for one SMT-LIB2 logic ("QF_LIA", "QF_BV", ...), which can be much faster. Z3 rejects a logic name it doesn't know, and we have no list to check against, so that error comes straight from it - but an assertion outside the logic is not reliably refused, so don't count on being told.
Just the incremental SMT core, which is usually weaker than Solver.new - but
it's the only solver which implements #trail and #set_initial_value.
Instance methods
tracker is a Bool const standing in for expr, and it's what shows up in
#unsat_core if the solver blames this assertion
Assumptions are Bool exprs taken as true for this one check and nothing after it -
unlike #assert they leave no trace on the solver, so there's no #push / #pop
to pair up. They're also what #unsat_core blames, so an Unsat names the
assumptions responsible without any of #assert_and_track's tracker variables.
Everything about variables which follows from the assertions. This solves, so
it's much more work than #assertions.
One case split, for divide-and-conquer solving - each call returns the next cube,
and [false] once they're exhausted, after which it starts over. variables is
which literals to split on, or [] to let Z3 choose.
Parses SMT-LIB2 and adds its assertions on top of whatever's already asserted.
Anything it declares goes into the shared context, so (declare-const a Int)
here is the same variable as Z3.int("a") in Crystal - but the parser starts
with an empty symbol table every time, so each string has to declare what it uses.
Cancels a #check in progress, so it returns Unknown instead of an answer.
It's meant for another fiber or a signal handler - on an idle solver it does
nothing, and the flag is cleared by the time the next #check starts.
A hint at which value to try for a variable first - a warm start, for feeding a
known-good solution back in. It stays a hint: an impossible one is overridden
rather than believed, and it can't make an unsat problem sat. It survives #check
and #push / #pop, and setting it again replaces it.
Only Solver.simple implements it. Every other kind takes the call and silently
ignores it, which is worse than refusing, so this refuses on their behalf.
Z3 acts on it for Bool (the initial phase), Int and Real (the Simplex tableau is calibrated towards it) and Bitvec (a phase per bit). Other sorts - String and Seq among them - it accepts and ignores, and there's no way to be told which is which.
Whether this is the plain incremental SMT core rather than a solver built out of
tactics. It matters because two Z3 features are implemented by that solver and no
other - #trail and #set_initial_value - and Z3 won't say which kind a solver
is, so this is remembered from however it was built.
The literals the solver currently has assigned, in assignment order.
Only Solver.simple implements it - every other kind raises.
The assertions Z3 has boiled down to a single literal, and everything it hasn't - together they're a partition of what the solver currently knows
Only the trackers passed to #assert_and_track, and the assumptions passed to
#check, can ever show up here - plainly asserted formulas are never blamed