Class: Z3::Goal

Inherits:
Object
  • Object
show all
Includes:
ReferenceCounted
Defined in:
lib/z3/goal.rb

Instance Attribute Summary collapse

Class Method Summary collapse

Instance Method Summary collapse

Methods included from ReferenceCounted

finalizer

Constructor Details

#initialize(_goal) ⇒ Goal

Returns a new instance of Goal.



6
7
8
9
 
# File 'lib/z3/goal.rb', line 6

def initialize(_goal)
  @_goal = _goal
  inc_ref! :goal, _goal
end

Instance Attribute Details

#_goal ⇒ Object (readonly)

Returns the value of attribute _goal.



5
6
7
 
# File 'lib/z3/goal.rb', line 5

def _goal
  @_goal
end

Class Method Details

.new(models = false, unsat_cores = false, proofs = false) ⇒ Object 



66
67
68
 
# File 'lib/z3/goal.rb', line 66

def new(models=false, unsat_cores=false, proofs=false)
  super LowLevel.mk_goal(!!models, !!unsat_cores, !!proofs)
end

Instance Method Details

#assert(ast) ⇒ Object

Raises:



11
12
13
14
 
# File 'lib/z3/goal.rb', line 11

def assert(ast)
  raise Z3::Exception, "AST required" unless ast.is_a?(AST)
  LowLevel.goal_assert(self, ast)
end

#decided_sat? ⇒ Boolean

Returns:

  • (Boolean) 


41
42
43
44
 
# File 'lib/z3/goal.rb', line 41

def decided_sat?
  # Does it convert bool or do we need to ?
  LowLevel.goal_is_decided_sat(self)
end

#decided_unsat? ⇒ Boolean

Returns:

  • (Boolean) 


46
47
48
49
 
# File 'lib/z3/goal.rb', line 46

def decided_unsat?
  # Does it convert bool or do we need to ?
  LowLevel.goal_is_decided_unsat(self)
end

#depth ⇒ Object 



20
21
22
 
# File 'lib/z3/goal.rb', line 20

def depth
  LowLevel.goal_depth(self)
end

#formula(num) ⇒ Object

Raises:



51
52
53
54
55
 
# File 'lib/z3/goal.rb', line 51

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? ⇒ Boolean

Returns:

  • (Boolean) 


36
37
38
39
 
# File 'lib/z3/goal.rb', line 36

def inconsistent?
  # Does it convert bool or do we need to ?
  LowLevel.goal_inconsistent(self)
end

#num_exprs ⇒ Object 



28
29
30
 
# File 'lib/z3/goal.rb', line 28

def num_exprs
  LowLevel.goal_num_exprs(self)
end

#precision ⇒ Object 



32
33
34
 
# File 'lib/z3/goal.rb', line 32

def precision
  LowLevel.goal_precision(self)
end

#reset ⇒ Object 



16
17
18
 
# File 'lib/z3/goal.rb', line 16

def reset
  LowLevel.goal_reset(self)
end

#size ⇒ Object 



24
25
26
 
# File 'lib/z3/goal.rb', line 24

def size
  LowLevel.goal_size(self)
end

#to_dimacs(include_names = true) ⇒ Object 



61
62
63
 
# File 'lib/z3/goal.rb', line 61

def to_dimacs(include_names=true)
  LowLevel.goal_to_dimacs_string(self, include_names)
end

#to_s ⇒ Object 



57
58
59
 
# File 'lib/z3/goal.rb', line 57

def to_s
  LowLevel.goal_to_string(self)
end