Class: Z3::BoolSort

Inherits:
Sort show all
Defined in:
lib/z3/sort/bool_sort.rb

Instance Attribute Summary

Attributes inherited from AST

#_ast

Instance Method Summary collapse

Methods inherited from Sort

#<, #<=, #<=>, #==, #>, #>=, #cast, #eql?, from_pointer, #from_value, #hash, #inspect, #new, #to_s, #value_class, #var

Methods inherited from AST

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

Constructor Details

#initialize ⇒ BoolSort

Returns a new instance of BoolSort.



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

def initialize
  super LowLevel.mk_bool_sort
end

Instance Method Details

#expr_class ⇒ Object 



7
8
9
 
# File 'lib/z3/sort/bool_sort.rb', line 7

def expr_class
  BoolExpr
end

#False ⇒ Object 



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

def False
  from_const(false)
end

#from_const(val) ⇒ Object 



11
12
13
14
15
16
17
18
19
 
# File 'lib/z3/sort/bool_sort.rb', line 11

def from_const(val)
  if val == true
    BoolExpr.new(LowLevel.mk_true, self)
  elsif val == false
    BoolExpr.new(LowLevel.mk_false, self)
  else
    raise Z3::Exception, "Cannot convert #{val.class} to #{self.class}"
  end
end

#True ⇒ Object 



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

def True
  from_const(true)
end