Class: PropLogic::Term

Inherits:
Object
  • Object
show all
Defined in:
lib/prop_logic/term.rb

Direct Known Subclasses

AndTerm, NotTerm, OrTerm, ThenTerm, Variable

Instance Attribute Summary collapse

Class Method Summary collapse

Instance Method Summary collapse

Constructor Details

#initialize ⇒ Term

Returns a new instance of Term.

Raises:

  • (NotImplementedError) 


5
6
7
 
# File 'lib/prop_logic/term.rb', line 5

def initialize
  raise NotImplementedError, 'Term cannot be initialized'
end

Instance Attribute Details

#terms ⇒ Object (readonly)

Returns the value of attribute terms.



17
18
19
 
# File 'lib/prop_logic/term.rb', line 17

def terms
  @terms
end

Class Method Details

.get(klass, *terms) ⇒ Object 



93
94
95
96
97
98
99
100
101
102
103
104
 
# File 'lib/prop_logic/term.rb', line 93

def self.get(klass, *terms)
  @table ||= Ref::WeakValueMap.new
  terms = validate_terms(*terms)
  if klass == AndTerm || klass == OrTerm
    terms = terms.map{|t| t.is_a?(klass) ? t.terms : t}.flatten
  end 
  key = klass.name + terms.map(&:object_id).join(',')
  return @table[key] if @table[key]
  ret = klass.__send__ :new, *terms
  @table[key] = ret
  ret.freeze
end

.validate_terms(*terms) ⇒ Object 



78
79
80
81
82
83
84
85
86
87
88
89
90
91
 
# File 'lib/prop_logic/term.rb', line 78

def self.validate_terms(*terms)
  terms.map do |term|
    case term
    when TrueClass
      True
    when FalseClass
      False
    when Term
      term
    else
      raise TypeError, "#{term.class} cannot be treated as term"
    end
  end
end

Instance Method Details

#and(*others) ⇒ Object Also known as: & 



19
20
21
22
 
# File 'lib/prop_logic/term.rb', line 19

def and(*others)
  others.unshift self
  Term.get AndTerm, *others
end

#assign(trues, falses, variables = nil) ⇒ Object

Raises:

  • (ArgumentError) 


114
115
116
117
118
119
120
121
122
123
124
125
126
 
# File 'lib/prop_logic/term.rb', line 114

def assign(trues, falses, variables = nil)
  # contradicted assignment
  raise ArgumentError, 'Contradicted assignment' unless (trues & falses).empty?
  variables ||= trues | falses
  assigned_terms = terms.map do |term|
    if (term.variables & variables).empty?
      term
    else
      term.assign(trues, falses, variables)
    end
  end
  Term.get self.class, *assigned_terms
end

#assign_false(*variables) ⇒ Object 



132
133
134
 
# File 'lib/prop_logic/term.rb', line 132

def assign_false(*variables)
  assign [], variables
end

#assign_true(*variables) ⇒ Object 



128
129
130
 
# File 'lib/prop_logic/term.rb', line 128

def assign_true(*variables)
  assign variables, []
end

#cnf? ⇒ Boolean

Returns:

  • (Boolean) 


106
107
108
 
# File 'lib/prop_logic/term.rb', line 106

def cnf?
  false
end

#equiv?(other) ⇒ Boolean

Returns:

  • (Boolean) 


144
145
146
 
# File 'lib/prop_logic/term.rb', line 144

def equiv?(other)
  ((self | other) & (~self | ~other)).unsat? 
end

#initialize_copy ⇒ Object

Raises:

  • (TypeError) 


9
10
11
 
# File 'lib/prop_logic/term.rb', line 9

def initialize_copy(*)
  raise TypeError, 'Term cannot be duplicated (immutable, not necessary)'
end

#nnf? ⇒ Boolean

Returns:

  • (Boolean) 


58
59
60
 
# File 'lib/prop_logic/term.rb', line 58

def nnf?
  false
end

#not ⇒ Object Also known as: ~, -@ 



33
34
35
 
# File 'lib/prop_logic/term.rb', line 33

def not
  Term.get NotTerm, self
end

#or(*others) ⇒ Object Also known as: | 



26
27
28
29
 
# File 'lib/prop_logic/term.rb', line 26

def or(*others)
  others.unshift self
  Term.get OrTerm, *others
end

#reduce ⇒ Object 



62
63
64
65
66
67
68
 
# File 'lib/prop_logic/term.rb', line 62

def reduce
  if reduced?
    self
  else
    Term.get self.class, *@terms.map(&:reduce)
  end
end

#reduced? ⇒ Boolean

Returns:

  • (Boolean) 


70
71
72
 
# File 'lib/prop_logic/term.rb', line 70

def reduced?
  false
end

#sat? ⇒ Boolean

Returns:

  • (Boolean) 


136
137
138
 
# File 'lib/prop_logic/term.rb', line 136

def sat?
  PropLogic.sat_solver.call(self)
end

#then(other) ⇒ Object Also known as: >> 



40
41
42
 
# File 'lib/prop_logic/term.rb', line 40

def then(other)
  Term.get ThenTerm, self, other
end

#to_cnf ⇒ Object 



74
75
76
 
# File 'lib/prop_logic/term.rb', line 74

def to_cnf
  reduce.to_cnf
end

#to_nnf ⇒ Object 



50
51
52
53
54
55
56
 
# File 'lib/prop_logic/term.rb', line 50

def to_nnf
  if nnf?
    self
  else
    Term.get self.class, *@terms.map(&:to_nnf)
  end
end

#to_s_in_term ⇒ Object 



46
47
48
 
# File 'lib/prop_logic/term.rb', line 46

def to_s_in_term
  to_s true
end

#unsat? ⇒ Boolean

Returns:

  • (Boolean) 


140
141
142
 
# File 'lib/prop_logic/term.rb', line 140

def unsat?
  sat? == false
end

#variables ⇒ Object 



110
111
112
 
# File 'lib/prop_logic/term.rb', line 110

def variables
  @terms.map(&:variables).flatten.uniq
end