Class: Udb::FreeTerm Private

Inherits:
Object
  • Object
show all
Extended by:
T::Sig
Includes:
Comparable
Defined in:
lib/udb/logic.rb

Overview

This class is part of a private API. You should avoid using this class if possible, as it may be removed or be changed in the future.

represents a “free” term, i.e., one that is not bound to the problem at hand used by the Tseytin Transformation, which introduces new propositions to represent subformula

Instance Attribute Summary collapse

Instance Method Summary collapse

Constructor Details

#initialize

This method is part of a private API. You should avoid using this method if possible, as it may be removed or be changed in the future. 



1104
1105
1106
1107
 
# File 'lib/udb/logic.rb', line 1104

def initialize
  @id = FreeTerm.instance_variable_get(:@next_id)
  FreeTerm.instance_variable_set(:@next_id, @id + 1)
end

Instance Attribute Details

#id ⇒ Integer (readonly)

This method is part of a private API. You should avoid using this method if possible, as it may be removed or be changed in the future.

Returns:

  • (Integer) 


1101
1102
1103
 
# File 'lib/udb/logic.rb', line 1101

def id
  @id
end

Instance Method Details

#<=>(other) ⇒ Integer?

This method is part of a private API. You should avoid using this method if possible, as it may be removed or be changed in the future.

Parameters:

  • other (T.untyped)

Returns:

  • (Integer, nil) 


1138
1139
1140
1141
1142
 
# File 'lib/udb/logic.rb', line 1138

def <=>(other)
  return nil unless other.is_a?(FreeTerm)

  @id <=> other.id
end

#eql?(other) ⇒ Boolean

This method is part of a private API. You should avoid using this method if possible, as it may be removed or be changed in the future.

Parameters:

  • other (T.untyped)

Returns:

  • (Boolean) 


1158
1159
1160
1161
1162
 
# File 'lib/udb/logic.rb', line 1158

def eql?(other)
  return false unless other.is_a?(FreeTerm)

  (self <=> other) == 0
end

#hash ⇒ Integer

This method is part of a private API. You should avoid using this method if possible, as it may be removed or be changed in the future.

hash and eql? must be implemented to use ParameterTerm as a Hash key

Returns:

  • (Integer) 


1150
 
# File 'lib/udb/logic.rb', line 1150

def hash = @id.hash

#to_h ⇒ Object

This method is part of a private API. You should avoid using this method if possible, as it may be removed or be changed in the future. 



1127
 
# File 'lib/udb/logic.rb', line 1127

def to_h = {}

#to_idl(cfg_arch) ⇒ String

This method is part of a private API. You should avoid using this method if possible, as it may be removed or be changed in the future.

Parameters:

Returns:

  • (String) 


1123
1124
1125
 
# File 'lib/udb/logic.rb', line 1123

def to_idl(cfg_arch)
  "FreeTerm"
end

#to_s ⇒ String

This method is part of a private API. You should avoid using this method if possible, as it may be removed or be changed in the future.

Returns:

  • (String) 


1113
1114
1115
 
# File 'lib/udb/logic.rb', line 1113

def to_s
  "t#{@id}"
end

#to_s_pretty ⇒ String

This method is part of a private API. You should avoid using this method if possible, as it may be removed or be changed in the future.

Returns:

  • (String) 


1130
 
# File 'lib/udb/logic.rb', line 1130

def to_s_pretty = to_s

#to_z3 ⇒ Z3::BoolExpr

This method is part of a private API. You should avoid using this method if possible, as it may be removed or be changed in the future.

Returns:

  • (Z3::BoolExpr) 


1118
1119
1120
 
# File 'lib/udb/logic.rb', line 1118

def to_z3
  @z3 ||= Z3.Bool(to_s)
end