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