class PropLogic::AndTerm

Public Class Methods

new(*terms) click to toggle source
# File lib/prop_logic/and_term.rb, line 3
def initialize(*terms)
  @terms = terms.map { |t| t.is_a?(AndTerm) ? t.terms : t }.flatten.freeze
  check_nnf_reduced
end

Public Instance Methods

cnf?() click to toggle source
# File lib/prop_logic/and_term.rb, line 39
def cnf?
  return false unless reduced?
  @terms.all?(&:cnf?)
end
nnf?() click to toggle source
# File lib/prop_logic/and_term.rb, line 13
def nnf?
  @is_nnf
end
reduce() click to toggle source
# File lib/prop_logic/and_term.rb, line 21
def reduce
  return self if reduced?
  reduced_terms = @terms.map(&:reduce).uniq
  reduced_terms.reject!{|term| term.equal?(True)}
  return True if reduced_terms.empty?
  if reduced_terms.any?{|term| term.equal?(False)}
    False
  elsif reduced_terms.length == 1
    reduced_terms[0]
  else
    # detect contradicted terms
    not_terms = reduced_terms.select{|term| term.is_a?(NotTerm)}
    negated_terms = not_terms.map{|term| term.terms[0]}
    return False unless (negated_terms & reduced_terms).empty?
    Term.get self.class, *reduced_terms
  end
end
reduced?() click to toggle source
# File lib/prop_logic/and_term.rb, line 17
def reduced?
  @is_reduced
end
to_cnf() click to toggle source
Calls superclass method
# File lib/prop_logic/and_term.rb, line 44
def to_cnf
  return super unless reduced?
  return self if cnf?
  pool = []
  without_pools = all_and(*@terms.map{|t| t.tseitin(pool)})
  all_and(without_pools, *pool)
end
to_s(in_term = false) click to toggle source
# File lib/prop_logic/and_term.rb, line 8
def to_s(in_term = false)
  str = @terms.map(&:to_s_in_term).join(' & ')
  in_term ? "( #{str} )" : str
end
tseitin(pool) click to toggle source
# File lib/prop_logic/and_term.rb, line 52
def tseitin(pool)
  val = Variable.new
  terms = @terms.map{|t| t.cnf? ? t : t.tseitin(pool)}
  pool.concat terms.map{|t| ~val | t }
  val
end