class Z3::Goal
Attributes
Public Class Methods
Source
# 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
Calls superclass method
Public Instance Methods
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
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
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
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
Source
# File lib/z3/goal.rb, line 33 def inconsistent? # Does it convert bool or do we need to ? LowLevel.goal_inconsistent(self) end