class Z3::Solver

Public Class Methods

Source

# File lib/z3/solver.rb, line 28
def for_logic(logic, params = {})
  new(params, LowLevel.mk_solver_for_logic(LowLevel.mk_symbol(logic)))
end

Specializes the solver for one SMT-LIB2 logic (“QF_LIA”, “QF_BV”, …), which can be much faster, at the cost of raising on anything outside that logic. Z3 rejects unknown names itself, we have no list to check against.

from_tactic (tactic, params = {})

Source

# File lib/z3/solver.rb, line 34
def from_tactic(tactic, params = {})
  raise Z3::Exception, "Tactic required" unless tactic.is_a?(Tactic)
  new(params, LowLevel.mk_solver_from_tactic(tactic))
end

Every check runs the tactic on the assertions. Tactics have no notion of scopes, so push / pop are simulated by re-running everything.

new (params = {}, _solver = LowLevel.mk_solver)

Source

# File lib/z3/solver.rb, line 8
def initialize(params = {}, _solver = LowLevel.mk_solver)
  @_solver = _solver
  inc_ref! :solver, @_solver
  reset_model!
  # Skipped for the common no-parameters case, as #set_params has to build
  # the parameter descriptions to check against, and there are hundreds of them
  set_params(params) unless params == {}
end

‘_solver` is how the alternative constructors below pass in their own solver; `Solver.new` is the general purpose one and you almost always want it

simple (params = {})

Source

# File lib/z3/solver.rb, line 21
def simple(params = {})
  new(params, LowLevel.mk_simple_solver)
end

‘Solver.new` inspects the assertions and assembles a tactic to match them. This one is just the incremental SMT core, which is usually weaker - but it’s the only solver which implements trail.

Public Instance Methods

assert (ast)

Source

# File lib/z3/solver.rb, line 82
def assert(ast)
  reset_model!
  LowLevel.solver_assert(self, ast)
end

assert_and_track (ast, tracker)

Source

# File lib/z3/solver.rb, line 89
def assert_and_track(ast, tracker)
  reset_model!
  LowLevel.solver_assert_and_track(self, ast, tracker)
end

‘tracker` is a Bool const standing in for `ast`, and it’s what shows up in unsat_core if the solver blames this assertion

assertions ()

Source

# File lib/z3/solver.rb, line 141
def assertions
  _ast_vector = LowLevel.solver_get_assertions(self)
  LowLevel.unpack_ast_vector(_ast_vector)
end

check (*assumptions)

Source

# File lib/z3/solver.rb, line 98
def check(*assumptions)
  reset_model!
  result = check_sat_results(
    if assumptions.empty?
      LowLevel.solver_check(self)
    else
      LowLevel.solver_check_assumptions(self, coerce_assumptions(assumptions))
    end
  )
  @has_model = true if result == :sat
  result
end

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.

consequences (variables, assumptions = [])

Source

# File lib/z3/solver.rb, line 156
def consequences(variables, assumptions = [])
  reset_model!
  LowLevel.with_ast_vectors(assumptions, variables, []) do |_assumptions, _variables, _consequences|
    result = check_sat_results(LowLevel.solver_get_consequences(self, _assumptions, _variables, _consequences))
    raise Z3::Exception, "Consequences need satisfiable assertions, these are #{result}" unless result == :sat
    LowLevel.unpack_ast_vector(_consequences)
  end
end

Everything about ‘variables` which follows from the assertions, as a list of `assumption => literal` implications (`true => literal` for the ones which hold outright). This solves, so it’s much more work than assertions.

cube (variables = [], backtrack_level = 0)

Source

# File lib/z3/solver.rb, line 168
def cube(variables = [], backtrack_level = 0)
  reset_model!
  LowLevel.with_ast_vectors(variables) do |_variables|
    LowLevel.unpack_ast_vector(LowLevel.solver_cube(self, _variables, backtrack_level))
  end
end

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.

from_file (path)

Source

# File lib/z3/solver.rb, line 212
def from_file(path)
  reset_model!
  LowLevel.solver_from_file(self, path)
  self
end

from_string (str)

Source

# File lib/z3/solver.rb, line 206
def from_string(str)
  reset_model!
  LowLevel.solver_from_string(self, str)
  self
end

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 Ruby - but the parser starts with an empty symbol table every time, so each string has to declare what it uses.

help ()

Source

# File lib/z3/solver.rb, line 223
def help
  LowLevel.solver_get_help(self)
end

interrupt ()

Source

# File lib/z3/solver.rb, line 197
def interrupt
  LowLevel.solver_interrupt(self)
  self
end

Cancels a check in progress, so it returns :unknown instead of an answer. It’s meant for another thread or a signal handler - on an idle solver it does nothing, and the flag is cleared by the time the next check starts.

model ()

Source

# File lib/z3/solver.rb, line 133
def model
  if @has_model
    @model ||= Z3::Model.new(LowLevel.solver_get_model(self))
  else
    raise Z3::Exception, "You need to check that it's satisfiable before asking for the model"
  end
end

non_units ()

Source

# File lib/z3/solver.rb, line 182
def non_units
  _ast_vector = LowLevel.solver_get_non_units(self)
  LowLevel.unpack_ast_vector(_ast_vector)
end

num_scopes ()

Source

# File lib/z3/solver.rb, line 227
def num_scopes
  LowLevel.solver_get_num_scopes(self)
end

param_descrs ()

Source

# File lib/z3/solver.rb, line 54
def param_descrs
  ParamDescrs.new(LowLevel.solver_get_param_descrs(self))
end

‘Z3_solver_get_param_descrs` lists every parameter the solver takes, `#help` describes them

pop (n=1)

Source

# File lib/z3/solver.rb, line 72
def pop(n=1)
  reset_model!
  LowLevel.solver_pop(self, n)
end

prove! (ast)

Source

# File lib/z3/solver.rb, line 243
def prove!(ast)
  @has_model = false
  push
  assert(~ast)
  case check
  when :sat
    puts "Counterexample exists"
    model.each do |n,v|
      puts "* #{n} = #{v}"
    end
  when :unknown
    puts "Unknown"
  when :unsat
    puts "Proven"
  else
    raise "Wrong SAT result #{r}"
  end
ensure
  pop
end

push ()

Source

# File lib/z3/solver.rb, line 67
def push
  reset_model!
  LowLevel.solver_push(self)
end

reason_unknown ()

Source

# File lib/z3/solver.rb, line 231
def reason_unknown
  LowLevel.solver_get_reason_unknown(self)
end

reset ()

Source

# File lib/z3/solver.rb, line 77
def reset
  reset_model!
  LowLevel.solver_reset(self)
end

satisfiable? (*assumptions)

Source

# File lib/z3/solver.rb, line 111
def satisfiable?(*assumptions)
  case check(*assumptions)
  when :sat
    true
  when :unsat
    false
  else
    raise Z3::Exception, "Satisfiability unknown"
  end
end

set_params (params)

Source

# File lib/z3/solver.rb, line 61
def set_params(params)
  params = Params.new(params, param_descrs) unless params.is_a?(Params)
  LowLevel.solver_set_params(self, params)
  self
end

Parameters accumulate - setting one twice overrides it, but parameters set by earlier calls stay. Pass a Params if you want to skip the name and type checks, a Hash if you don’t.

statistics ()

Source

# File lib/z3/solver.rb, line 218
def statistics
  _stats = LowLevel::solver_get_statistics(self)
  LowLevel.unpack_statistics(_stats)
end

to_dimacs (include_names=true)

Source

# File lib/z3/solver.rb, line 239
def to_dimacs(include_names=true)
  LowLevel.solver_to_dimacs_string(self, include_names)
end

to_s ()

Source

# File lib/z3/solver.rb, line 235
def to_s
  LowLevel.solver_to_string(self)
end

trail ()

Source

# File lib/z3/solver.rb, line 189
def trail
  _ast_vector = LowLevel.solver_get_trail(self)
  LowLevel.unpack_ast_vector(_ast_vector)
end

The literals the solver currently has assigned, in assignment order. Only Solver.simple implements it - every other kind raises Z3::Exception.

units ()

Source

# File lib/z3/solver.rb, line 177
def units
  _ast_vector = LowLevel.solver_get_units(self)
  LowLevel.unpack_ast_vector(_ast_vector)
end

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

unsat_core ()

Source

# File lib/z3/solver.rb, line 148
def unsat_core
  _ast_vector = LowLevel.solver_get_unsat_core(self)
  LowLevel.unpack_ast_vector(_ast_vector)
end

Only the trackers passed to assert_and_track can ever show up here, plainly asserted formulas are never blamed

unsatisfiable? (*assumptions)

Source

# File lib/z3/solver.rb, line 122
def unsatisfiable?(*assumptions)
  case check(*assumptions)
  when :unsat
    true
  when :sat
    false
  else
    raise Z3::Exception, "Satisfiability unknown"
  end
end

with_simplifier (simplifier, params = {})

Source

# File lib/z3/solver.rb, line 47
def with_simplifier(simplifier, params = {})
  raise Z3::Exception, "Simplifier required" unless simplifier.is_a?(Simplifier)
  Solver.new(params, LowLevel.solver_add_simplifier(self, simplifier))
end

Attaches a simplifier, which the solver then runs over the assertions as incremental preprocessing.

Z3 hands back a different solver rather than changing this one, so this returns a new Solver and leaves the receiver alone - and it refuses outright once anything has been asserted, so it has to come first. Parameters don’t carry over from the receiver either, as Z3 has no way to read them back.