class Z3::Solver

Z3::Solver
Reference
Object

Defined in:

z3/solver.cr

Constructors

.new

Instance Method Summary

#assert(expr)
#assert_and_track(expr, tracker)
#assertions
#check
#model
#num_scopes
#pop(n = 1)
#push
#reason_unknown
#reset
#satisfiable?
#statistics
#to_s(io)
#to_unsafe : LibZ3::Solver
#unsat_core

Constructor Detail

def self.new #

[View source]

Instance Method Detail

def assert(expr) #

[View source]

def assert_and_track(expr, tracker) #

[View source]

def assertions #

[View source]

def check #

[View source]

def model #

[View source]

def num_scopes #

[View source]

def pop(n = 1) #

[View source]

def push #

[View source]

def reason_unknown #

[View source]

def reset #

[View source]

def satisfiable? #

[View source]

def statistics #

[View source]

def to_s(io) #

[View source]

def to_unsafe : LibZ3::Solver #

[View source]

def unsat_core #

[View source]