Class: PropLogic::Term

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

Overview

monkey-patching cache generation

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

.generate_cache ⇒ Object 



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

def self.generate_cache
  Ref::WeakValueMap.new
end

.get(klass, *terms) ⇒ Object 



124
125
126
127
128
129
130
131
 
# File 'lib/prop_logic/term.rb', line 124

def self.get(klass, *terms)
  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
  cached klass, *terms
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) 


144
145
146
147
148
149
150
151
152
153
154
155
156
 
# File 'lib/prop_logic/term.rb', line 144

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 



162
163
164
 
# File 'lib/prop_logic/term.rb', line 162

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

#assign_true(*variables) ⇒ Object 



158
159
160
 
# File 'lib/prop_logic/term.rb', line 158

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

#cnf? ⇒ Boolean

check if this term is a cnf term.

Returns:

  • (Boolean) —

    false unless overridden.



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

def cnf?
  false
end

#each_sat ⇒ Enumerator?

loop with each satisfied terms.

Returns:

  • (Enumerator) —

    if block is not given.

  • (nil) —

    if block is given.



173
174
175
176
177
178
179
180
181
182
 
# File 'lib/prop_logic/term.rb', line 173

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) 


188
189
190
 
# File 'lib/prop_logic/term.rb', line 188

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) 


166
167
168
 
# File 'lib/prop_logic/term.rb', line 166

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) 


184
185
186
 
# File 'lib/prop_logic/term.rb', line 184

def unsat?
  sat? == false
end

#variables ⇒ Array

Returns variables used by this term.

Returns:

  • (Array) —

    variables used by this term.



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

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