jkr2255 / prop_logic

    def to_s(in_term = false)

      str = @terms.map(&:to_s_in_term).join(' & ')

      in_term ? "( #{str} )" : str

    end

    def nnf?

      @is_nnf

    end

    def reduced?

      @is_reduced

    end

    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

    def cnf?

      return false unless reduced?

      @terms.all?(&:cnf?)

    end

    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

    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

  end

end