Class: Z3::Goal

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

Instance Attribute Summary collapse

Class Method Summary collapse

Instance Method Summary collapse

Constructor Details

#initialize(_goal) ⇒ Goal

Returns a new instance of Goal.



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

def initialize(_goal)
  @_goal = _goal
end

Instance Attribute Details

#_goal ⇒ Object (readonly)

Returns the value of attribute _goal.



3
4
5
 
# File 'lib/z3/goal.rb', line 3

def _goal
  @_goal
end

Class Method Details

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



59
60
61
 
# 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

Instance Method Details

#assert(ast) ⇒ Object

Raises:



8
9
10
11
 
# 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? ⇒ Boolean

Returns:

  • (Boolean) 


38
39
40
41
 
# 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? ⇒ Boolean

Returns:

  • (Boolean) 


43
44
45
46
 
# 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 ⇒ Object 



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

def depth
  LowLevel.goal_depth(self)
end

#formula(num) ⇒ Object

Raises:



48
49
50
51
52
 
# 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? ⇒ Boolean

Returns:

  • (Boolean) 


33
34
35
36
 
# 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 ⇒ Object 



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

def num_exprs
  LowLevel.goal_num_exprs(self)
end

#precision ⇒ Object 



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

def precision
  LowLevel.goal_precision(self)
end

#reset ⇒ Object 



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

def reset
  LowLevel.goal_reset(self)
end

#size ⇒ Object 



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

def size
  LowLevel.goal_size(self)
end

#to_s ⇒ Object 



54
55
56
 
# File 'lib/z3/goal.rb', line 54

def to_s
  LowLevel.goal_to_string(self)
end