Remove debugging statements.

Author: roberthoenig

src/conjunctive_normal_form.jl

@@ -11,7 +11,7 @@ function get_conjunctive_normal_form(formula)
     """
     Get equivalent formula with no negation in non-literal formulas.
     """
-        function collapse_negations(formula)
+    function collapse_negations(formula)
         @match formula begin
         f::Negation => begin
             @match f.formula begin

src/helpers.jl

@@ -1,5 +1,4 @@
 export @debug
-    #    reshape
 
 function bracketsplit(str)
     parts = []
@@ -49,10 +48,7 @@ end
 
 function powerset(x)
     result = [Set()]
-    # println("collect(x) ", collect(x))
     for element in collect(x), idx = 1:length(result)
-        # println("element ", element)
-        # println("idx ", idx)
         newsubset = union(result[idx], Set([element]))
         push!(result, newsubset)
     end
@@ -87,19 +83,6 @@ function dispatch_applyrecursively(functionexpr, objectexpr,
     end
 end
 
-# function dispatch_applyrecursively(functionexpr, objectexpr,
-#                                     objecttype::Type{Val{:monotone_fields}})
-#     fsymbol, fargs = functionexpr.args[1],
-#                         functionexpr.args[2:end]
-#     quote
-#     typeof($(esc(objectexpr)))(
-#         [$fsymbol(
-#             [arg == :_ ? field : arg
-#                 for arg in $(esc(fargs))]...)
-#             for field in getfield.($(esc(objectexpr)), fieldnames($(esc(objectexpr))))]...)
-#     end
-# end
-
 macro debug(variable)
     Expr(:call,
          :println,
@@ -111,7 +94,6 @@ macro debug(variable)
         "\n"
         )
 end
-print(args...) = println(args...)
 
 let nextfreesymbol = 0
     global getnextfreesymbol
@@ -124,28 +106,3 @@ let nextfreesymbol = 0
         nextfreesymbol = 0
     end
 end
-
-# function reshape(formula::String, form::FormulaForm)
-#     form == string ? String(Formula(formula)) : reshape(Formula(formula))
-# end
-
-# function reshape(formula::Formula, form::FormulaForm)
-#     @match form begin
-#     string => String(formula)
-#     formula => formula
-#     quantifiedvariables => get_quantified_variables_form(formula)
-#     prenex => get_prenex_normal_form(formula)
-#     skolem => get_prenex_normal_form(
-#         get_skolem_normal_form(formula)
-#     )
-#     removedquantifier => get_removed_quantifier_form(formula)
-#     conjunctive => get_conjunctive_normal_form(formula)
-#     resolutionready => get_conjunctive_normal_form(
-#         get_removed_quantifier_form(
-#             get_skolem_normal_form(
-#                 get_prenex_normal_form(
-#                     get_quantified_variables_form(
-#                         Formula(formula)))))
-#     )
-#     end
-# end

src/parser.jl

@@ -59,4 +59,4 @@ Formula(str::AbstractString) = begin
         "|" => return Disjunction(Formula(formula1), Formula(formula2))
         end
     end
-end
+end

src/renamed_quantifiers_form.jl

@@ -11,7 +11,6 @@ function get_renamed_quantifiers_form(formula, replacements=Dict{Variable, Varia
     )
     f::AFormula || f::EFormula => begin
         replacements[f.variable] = Variable(getnextfreesymbol())
-        # println("got next symbol, ", replacements[f.variable])
         typeof(f)(
             replacements[f.variable],
             get_renamed_quantifiers_form(f.formula, copy(replacements)),

src/resolution.jl

@@ -4,7 +4,6 @@ function get_most_general_unifier(unifiables::Set{<:Unifiable})
     unifier = Substitution()
     unified = first(unifiables)
     for unifiable in collect(unifiables)[2:end]
-        # @debug unifier
         most_general_unifier!(unifier, unified, unifiable)
         substitute(unified, unifier)
     end
@@ -14,8 +13,6 @@ end
 function most_general_unifier!(unifier!::Substitution, unifiable1::Unifiable, unifiable2::Unifiable)
     substituted_unifiable1 = substitute(unifiable1, unifier!)
     substituted_unifiable2 = substitute(unifiable2, unifier!)
-    # @debug String(substituted_unifiable1)
-    # @debug String(substituted_unifiable2)
     @match substituted_unifiable1 begin
     u1::Literal => begin
         # Two clauses A and B can only be unified if the
@@ -70,7 +67,6 @@ end
 
 # Apply substitution in order.
 function substitute(formula::Union{Term, Formula, Literal, Clause}, substitution::Substitution)
-    # @debug substitution
     substituted_formula = formula
     for (substitutee, substituter) in substitution
         substituted_formula = substitute(substituted_formula, substitutee, substituter)
@@ -79,8 +75,6 @@ function substitute(formula::Union{Term, Formula, Literal, Clause}, substitution
 end
 
 function substitute(formula::Union{Term, Formula, Literal, Clause}, substitutee, substituter)
-    # println("substitute")
-    # @debug formula
     @match formula begin
     f::CNF => @applyrecursively substitute(:_, substitutee, substituter) f CNF
     f::Clause => @applyrecursively substitute(:_, substitutee, substituter) f Clause
@@ -141,27 +135,17 @@ function rename_all_variables(formula, replacements=Dict{Variable, Variable}())
 end
 
 function get_maybe_unifiable_literals(clause1::Clause, clause2::Clause)
-    # println("get_mabye_unifiable_literals")
-    # println(clause1)
-    # println(clause2)
     maybe_unifiable_literals = Set{Set{Literal}}()
     all_literals = union(clause1, clause2)
     literal_names = Set(map(l -> l.formula.name, all_literals))
     for literal_name in literal_names
-        # println("literal_name ", literal_name)
         for (c1, c2) in ((clause1, clause2), (clause2, clause1))
-            # println("c1 ", string(c1))
-            # println("c2 ", string(c2))
             positive_literals_in_c1 =
                 filter(l -> l.formula.name == literal_name && !l.negative, c1)
             negative_literals_in_c2 =
                 filter(l -> l.formula.name == literal_name && l.negative, c2)
             positive_literals_combinations = powerset(positive_literals_in_c1)
             negative_literals_combinations = powerset(negative_literals_in_c2)
-            # println("positive_literals_in_c1 ", positive_literals_in_c1)
-            # println("positive_literals_combinations ", positive_literals_combinations)
-            # println("negative_literals_in_c2 ", negative_literals_in_c2)
-            # println("negative_literals_combinations ", negative_literals_combinations)
             for positive_literals in positive_literals_combinations
                 for negative_literals in negative_literals_combinations
                     if length(positive_literals) > 0 && length(negative_literals) > 0
@@ -172,37 +156,24 @@ function get_maybe_unifiable_literals(clause1::Clause, clause2::Clause)
             end
         end
     end
-    # println("maybe_unifiable_literals ", maybe_unifiable_literals)
     maybe_unifiable_literals
 end
 
 function is_satisfiable(clauses::CNF; maxsearchdepth=Inf)
-    # @debug maxsearchdepth
-    # @debug length(clauses)
     if maxsearchdepth == 0
         throw(OverMaxSearchDepthError())
     end
     renamed = rename_all_variables.(collect(clauses))
     clauses = CNF(renamed)
-    # @debug String(clauses)
     newclauses = CNF()
     for clause1 in clauses
-        # @debug clause1
         for clause2 in clauses
-            # @debug String(clause1)
-            # @debug String(clause2)
             groups_of_maybe_unifiable_literals = get_maybe_unifiable_literals(clause1, clause2)
-            # @debug String(groups_of_maybe_unifiable_literals)
             for maybe_unifiable_literals in groups_of_maybe_unifiable_literals
-                # @debug String(maybe_unifiable_literals)
                 try
                     unifier = get_most_general_unifier(maybe_unifiable_literals)
                     newclause = setdiff(union(clause1, clause2), maybe_unifiable_literals)
-                    # @debug unifier
-                    # @debug String(newclause)
                     substituted_newclause = substitute(newclause, unifier)
-                    # @debug unifier
-                    # @debug String(substituted_newclause)
                     push!(newclauses, substituted_newclause)
                 catch
                     continue
@@ -211,7 +182,6 @@ function is_satisfiable(clauses::CNF; maxsearchdepth=Inf)
         end
     end
     union!(clauses, newclauses)
-    # @debug String(clauses)
     if Clause([]) in clauses
         false
     else

src/skolem_normal_form.jl

@@ -8,7 +8,6 @@ function get_skolem_normal_form(formula, replacements=Dict{Variable, Function}()
     end
     f::EFormula => begin
         replacements[f.variable] = Function(FunctionSymbol(getnextfreesymbol()), all_quantifiers)
-        # @debug replacements[f.variable]
         get_skolem_normal_form(f.formula, replacements, all_quantifiers)
     end
     f::Conjunction || f::Disjunction => typeof(f)(get_skolem_normal_form(f.formula1, replacements), get_skolem_normal_form(f.formula2, replacements))

src/testing_helpers.jl

@@ -1,34 +1,4 @@
 using Base.Test
-# import Base.Test: record, finish
-# using Base.Test: AbstractTestSet, Result, Pass, Fail, Error
-# using Base.Test: get_testset_depth, get_testset
-# using Base.Test
-
-# export FirstOrderLogicTest
-
-# type FirstOrderLogicTest <: AbstractTestSet
-#     description::AbstractString
-#     executed_tests::Int
-#     results::Vector
-#     FirstOrderLogicTest(description::String, executed_tests=0) =
-#         new(description, executed_tests, [])
-# end
-
-# record(ts::FirstOrderLogicTest, child::AbstractTestSet) = push!(ts.results, child)
-# record(testset::FirstOrderLogicTest, result::Result) = begin
-#     testset.executed_tests += 1
-#     push!(testset.results, result)
-#     println("$(testset.executed_tests): $(result.orig_expr)")
-#     resetfreesymbols()
-# end
-
-# function finish(ts::FirstOrderLogicTest)
-#     # just record if we're not the top-level parent
-#     if get_testset_depth() > 0
-#         record(get_testset(), ts)
-#     end
-#     ts
-# end
 
 export @customtest,
     @customtest_throws

src/types.jl

@@ -16,7 +16,6 @@ export Term,
     Substitution,
     Unifiable,
     OverMaxSearchDepthError
-    # FormulaForm
 
 abstract type Term end
 abstract type Formula end
@@ -73,10 +72,9 @@ end
 end
 
 const Clause = Set{Literal}
-const CNF = Set{Clause}
+const CNF = Set{Clause}  # Conjunctive xnormal form
 const Substitution = Vector{Pair{Variable, Term}}
 const Unifiable = Union{Literal, Term}
-# Conjunctive normal form
 
 String(x::PredicateSymbol) = x.symbol
 String(x::FunctionSymbol) = x.symbol
@@ -113,5 +111,3 @@ end
 
 type NotUnifiableError <: Exception
 end
-
-# @enum FormulaForm string formula quantifiedvariables prenex skolem removedquantifier conjunctive resolutionready