class Z3::Goal
Attributes
_goal[R]
Public Class Methods
new(_goal)
click to toggle source
# File lib/z3/goal.rb, line 4 def initialize(_goal) @_goal = _goal end
new(models=false, unsat_cores=false, proofs=false)
click to toggle source
Calls superclass method
# File lib/z3/goal.rb, line 59 def new(models=false, unsat_cores=false, proofs=false) super LowLevel.mk_goal(!!models, !!unsat_cores, !!proofs) end
Public Instance Methods
assert(ast)
click to toggle source
# File lib/z3/goal.rb, line 8 def assert(ast) raise Z3::Exception, "AST required" unless ast.is_a?(AST) LowLevel.goal_assert(self, ast) end
decided_sat?()
click to toggle source
# File lib/z3/goal.rb, line 38 def decided_sat? # Does it convert bool or do we need to ? LowLevel.goal_is_decided_sat(self) end
decided_unsat?()
click to toggle source
# File lib/z3/goal.rb, line 43 def decided_unsat? # Does it convert bool or do we need to ? LowLevel.goal_is_decided_unsat(self) end
depth()
click to toggle source
# File lib/z3/goal.rb, line 17 def depth LowLevel.goal_depth(self) end
formula(num)
click to toggle source
# File lib/z3/goal.rb, line 48 def formula(num) raise Z3::Exception, "Out of range" unless num.between?(0, size-1) # We should probably deal with out of bounds here Expr.new_from_pointer(LowLevel.goal_formula(self, num)) end
inconsistent?()
click to toggle source
# File lib/z3/goal.rb, line 33 def inconsistent? # Does it convert bool or do we need to ? LowLevel.goal_inconsistent(self) end
num_exprs()
click to toggle source
# File lib/z3/goal.rb, line 25 def num_exprs LowLevel.goal_num_exprs(self) end
precision()
click to toggle source
# File lib/z3/goal.rb, line 29 def precision LowLevel.goal_precision(self) end
reset()
click to toggle source
# File lib/z3/goal.rb, line 13 def reset LowLevel.goal_reset(self) end
size()
click to toggle source
# File lib/z3/goal.rb, line 21 def size LowLevel.goal_size(self) end
to_s()
click to toggle source
# File lib/z3/goal.rb, line 54 def to_s LowLevel.goal_to_string(self) end