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. 



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

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) 


1120
1121
1122
 
# File 'lib/udb/logic.rb', line 1120

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) 


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

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) 


1177
1178
1179
1180
1181
 
# File 'lib/udb/logic.rb', line 1177

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) 


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

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. 



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

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) 


1142
1143
1144
 
# File 'lib/udb/logic.rb', line 1142

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) 


1132
1133
1134
 
# File 'lib/udb/logic.rb', line 1132

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) 


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

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) 


1137
1138
1139
 
# File 'lib/udb/logic.rb', line 1137

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