Class: PropLogic::Term

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

Overview

Abstract base class for terms of PropLogic. Actual terms are subclasses of Term.

Direct Known Subclasses

AndTerm, NotTerm, OrTerm, ThenTerm, Variable

Instance Attribute Summary collapse

Class Method Summary collapse

Instance Method Summary collapse

Methods included from Functions

all_and, all_or, new_variable, sat_loop

Constructor Details

#initialize ⇒ Term

Returns a new instance of Term.

Raises:

  • NotImplementedError Term is abstract class.



13
14
15
 
# File 'lib/prop_logic/term.rb', line 13

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

Instance Attribute Details

#terms ⇒ Object (readonly)

Returns the value of attribute terms.



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

def terms
  @terms
end

Class Method Details

.get(klass, *terms) ⇒ Object 



105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
 
# File 'lib/prop_logic/term.rb', line 105

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
    return terms[0] if terms.length == 1
  end
  key = klass.name + terms.map(&:object_id).join(',')
  return @table[key] if @table[key]
  ret = klass.__send__ :new, *terms
  @table[key] = ret
  # kick caching mechanism
  ret.variables
  ret.freeze
end

Instance Method Details

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



28
29
30
31
 
# File 'lib/prop_logic/term.rb', line 28

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

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

Raises:

  • (ArgumentError) 


132
133
134
135
136
137
138
139
140
141
142
143
144
 
# File 'lib/prop_logic/term.rb', line 132

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 



150
151
152
 
# File 'lib/prop_logic/term.rb', line 150

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

#assign_true(*variables) ⇒ Object 



146
147
148
 
# File 'lib/prop_logic/term.rb', line 146

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

#cnf? ⇒ Boolean

check if this term is a cnf term.

Returns:

  • (Boolean) —

    false unless overridden.



123
124
125
 
# File 'lib/prop_logic/term.rb', line 123

def cnf?
  false
end

#each_sat ⇒ Enumerator?

loop with each satisfied terms.

Returns:

  • (Enumerator) —

    if block is not given.

  • (nil) —

    if block is given.



161
162
163
164
165
166
167
168
169
170
 
# File 'lib/prop_logic/term.rb', line 161

def each_sat
  return to_enum(:each_sat) unless block_given?
  sat_loop(self) do |sat, solver|
    yield sat
    negated_vars = sat.terms.map do |t|
      t.is_a?(NotTerm) ? t.terms[0] : ~t
    end
    solver << PropLogic.all_or(*negated_vars)
  end
end

#equiv?(other) ⇒ Boolean

Returns:

  • (Boolean) 


176
177
178
 
# File 'lib/prop_logic/term.rb', line 176

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

#initialize_copy ⇒ Object

disallow duplication

Raises:

  • (TypeError) 


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

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

#nnf? ⇒ Boolean

Returns:

  • (Boolean) 


67
68
69
 
# File 'lib/prop_logic/term.rb', line 67

def nnf?
  false
end

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



42
43
44
 
# File 'lib/prop_logic/term.rb', line 42

def not
  Term.get NotTerm, self
end

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



35
36
37
38
 
# File 'lib/prop_logic/term.rb', line 35

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

#reduce ⇒ Object 



71
72
73
74
75
76
77
 
# File 'lib/prop_logic/term.rb', line 71

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

#reduced? ⇒ Boolean

Returns:

  • (Boolean) 


79
80
81
 
# File 'lib/prop_logic/term.rb', line 79

def reduced?
  false
end

#sat? ⇒ Boolean

Returns:

  • (Boolean) 


154
155
156
 
# File 'lib/prop_logic/term.rb', line 154

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

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



49
50
51
 
# File 'lib/prop_logic/term.rb', line 49

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

#to_cnf ⇒ Object 



83
84
85
 
# File 'lib/prop_logic/term.rb', line 83

def to_cnf
  reduce.to_cnf
end

#to_nnf ⇒ Object 



59
60
61
62
63
64
65
 
# File 'lib/prop_logic/term.rb', line 59

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

#to_s_in_term ⇒ Object 



55
56
57
 
# File 'lib/prop_logic/term.rb', line 55

def to_s_in_term
  to_s true
end

#unsat? ⇒ Boolean

Returns:

  • (Boolean) 


172
173
174
 
# File 'lib/prop_logic/term.rb', line 172

def unsat?
  sat? == false
end

#variables ⇒ Array

Returns variables used by this term.

Returns:

  • (Array) —

    variables used by this term.



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

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