Class: Z3::BoolExpr

Inherits:
Expr show all
Defined in:
lib/z3/expr/bool_expr.rb

Instance Attribute Summary

Attributes inherited from Expr

#sort

Attributes inherited from AST

#_ast

Class Method Summary collapse

Instance Method Summary collapse

Methods inherited from Expr

#!=, #==, Add, And, Distinct, Eq, Ge, Gt, Le, Lt, Mul, Or, Sub, Xor, coerce_to_same_sort, #initialize, #inspect, new_from_pointer, sort_for_const

Methods inherited from AST

#arguments, #ast_kind, #func_decl, #initialize, #sexpr, #simplify, #to_s

Constructor Details

This class inherits a constructor from Z3::Expr

Class Method Details

.coerce_to_same_bool_sort(*args) ⇒ Object

Raises:



53
54
55
56
57
 
# File 'lib/z3/expr/bool_expr.rb', line 53

def coerce_to_same_bool_sort(*args)
  args = coerce_to_same_sort(*args)
  raise Z3::Exception, "Bool value expected" unless args[0].is_a?(BoolExpr)
  args
end

.Iff(a, b) ⇒ Object 



64
65
66
67
 
# File 'lib/z3/expr/bool_expr.rb', line 64

def Iff(a,b)
  a, b = coerce_to_same_bool_sort(a, b)
  BoolSort.new.new(LowLevel.mk_iff(a, b))
end

.IfThenElse(a, b, c) ⇒ Object 



69
70
71
72
73
 
# File 'lib/z3/expr/bool_expr.rb', line 69

def IfThenElse(a, b, c)
  a, = coerce_to_same_bool_sort(a)
  b, c = coerce_to_same_sort(b, c)
  b.sort.new(LowLevel.mk_ite(a, b, c))
end

.Implies(a, b) ⇒ Object 



59
60
61
62
 
# File 'lib/z3/expr/bool_expr.rb', line 59

def Implies(a,b)
  a, b = coerce_to_same_bool_sort(a, b)
  BoolSort.new.new(LowLevel.mk_implies(a, b))
end

Instance Method Details

#! ⇒ Object 



7
8
9
 
# File 'lib/z3/expr/bool_expr.rb', line 7

def !
  sort.new(LowLevel.mk_not(self))
end

#&(other) ⇒ Object 



11
12
13
 
# File 'lib/z3/expr/bool_expr.rb', line 11

def &(other)
  Expr.And(self, other)
end

#^(other) ⇒ Object 



19
20
21
 
# File 'lib/z3/expr/bool_expr.rb', line 19

def ^(other)
  Expr.Xor(self, other)
end

#iff(other) ⇒ Object 



23
24
25
 
# File 'lib/z3/expr/bool_expr.rb', line 23

def iff(other)
  BoolExpr.Iff(self, other)
end

#implies(other) ⇒ Object 



27
28
29
 
# File 'lib/z3/expr/bool_expr.rb', line 27

def implies(other)
  BoolExpr.Implies(self, other)
end

#ite(a, b) ⇒ Object 



31
32
33
 
# File 'lib/z3/expr/bool_expr.rb', line 31

def ite(a, b)
  BoolExpr.IfThenElse(self, a, b)
end

#to_b ⇒ Object 



35
36
37
38
39
40
41
42
43
44
45
46
47
48
 
# File 'lib/z3/expr/bool_expr.rb', line 35

def to_b
  s = to_s
  if ast_kind == :app and (s == "true" or s == "false")
    s == "true"
  else
    obj = simplify
    s = obj.to_s
    if ast_kind == :app and (s == "true" or s == "false")
      s == "true"
    else
      raise Z3::Exception, "Can't convert expression #{to_s} to Boolean"
    end
  end
end

#|(other) ⇒ Object 



15
16
17
 
# File 'lib/z3/expr/bool_expr.rb', line 15

def |(other)
  Expr.Or(self, other)
end

#~ ⇒ Object 



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

def ~
  sort.new(LowLevel.mk_not(self))
end