Add docstrings.

This documents all exported functions, and important exported types.

Author: roberthoenig

src/conjunctive_normal_form.jl

@@ -1,16 +1,18 @@
 export get_conjunctive_normal_form
 
 """
-Get equivalent formula in the conjunctive normal form for a given formula.
+    get_conjunctive_normal_form(formula)
+
+Return `formula` in the conjunctive normal form, expressed as clauses.
+
+`formula` must not contain quantifiers. The returned formula is logically
+equivalent to `formula`.
 """
 function get_conjunctive_normal_form(formula)
 # Ideally, we would use a single @match clause to handle both
 # negations and junctions. The negation case is tricky to implement
 # in such a unified approach, however, so we generate the CNF in two
 # steps.
-    """
-    Get equivalent formula with no negation in non-literal formulas.
-    """
     function collapse_negations(formula)
         @match formula begin
         f::Negation => begin

src/helpers.jl

@@ -1,4 +1,7 @@
-export @debug
+export @debug,
+    powerset,
+    getnextfreesymbol,
+    resetfreesymbols
 
 function bracketsplit(str)
     parts = []
@@ -46,6 +49,11 @@ function strip_and_remove_surrounding_brackets(str)
     str
 end
 
+"""
+    powerset(x)
+
+Returns the powerset of x (a set of all subsets of x).
+"""
 function powerset(x)
     result = [Set()]
     for element in collect(x), idx = 1:length(result)
@@ -83,6 +91,11 @@ function dispatch_applyrecursively(functionexpr, objectexpr,
     end
 end
 
+"""
+    @debug variable
+
+Print the symbol `variable`, followed by its value, followed by an empty line.
+"""
 macro debug(variable)
     Expr(:call,
          :println,
@@ -95,6 +108,27 @@ macro debug(variable)
         )
 end
 
+
+"""
+    getnextfreesymbol()
+
+Returns a new, unique string that can be used
+for naming objects.
+
+This does not check if a user-entered formula
+already contains the returned string.
+"""
+function getnextfreesymbol end
+
+"""
+    resetfreesymbols()
+
+Resets the free symbol state.
+
+Newly generated symbols will "start over".
+"""
+function resetfreesymbols end
+
 let nextfreesymbol = 0
     global getnextfreesymbol
     global resetfreesymbols

src/parser.jl

@@ -1,3 +1,5 @@
+export Formula
+
 Term(str::AbstractString) = begin
     function get_term(str)
         function_match = match(r"(\w*)\((.*)\)$", str)
@@ -38,6 +40,11 @@ AFormula(str::AbstractString) = begin
     AFormula(Variable(name), Formula(formula))
 end
 
+"""
+    Formula(str::AbstractString)
+
+Parse `str` to a Formula object and return that object.
+"""
 Formula(str::AbstractString) = begin
     formula = strip_and_remove_surrounding_brackets(str)
     parts = strip.(bracketsplit(formula))

src/prenex_normal_form.jl

@@ -25,6 +25,13 @@ function handle_junction(formula1, formula2, junction)
     end
 end
 
+"""
+    get_prenex_normal_form(formula)
+
+Return the prenex normal form of `formula`.
+
+The returned formula is logically equivalent to `formula`.
+"""
 function get_prenex_normal_form(formula)
     prepared_formula = get_renamed_quantifiers_form(formula)
     @match prepared_formula begin

src/quantified_variables_form.jl

@@ -1,6 +1,13 @@
 export get_quantified_variables_form,
     get_unbound_variables
 
+"""
+    get_quantified_variables_form(formula)
+
+Return `formula` with all unbound variables bound to existential quantifiers.
+
+The returned formula is equisatisfiable with `formula`.
+"""
 function get_quantified_variables_form(formula)
     variables = get_unbound_variables(formula)
     quantified_variables_form = formula

src/removed_quantifier_form.jl

@@ -1,8 +1,10 @@
 export get_removed_quantifier_form
 
-# In "Logik für Informatiker", the removed quantifier form
-# is called the "Matrix" of a formula. This has nothing to
-# do with the general notion of matrices in mathematics.
+"""
+    get_removed_quantifier_form(formula::Union{Formula, Term})
+
+Return `formula` without any quantifiers.
+"""
 function get_removed_quantifier_form(formula::Union{Formula, Term})
     @match formula begin
         f::AFormula || f::EFormula => get_removed_quantifier_form(f.formula)

src/renamed_quantifiers_form.jl

@@ -1,5 +1,12 @@
 export get_renamed_quantifiers_form
 
+"""
+    get_renamed_quantifiers_form(formula, replacements=Dict{Variable, Variable}())
+
+Return `formula` with new, unique variable symbols assigned to each quantified variable.
+
+The returned formula is logically equivalent to `formula`.
+"""
 function get_renamed_quantifiers_form(formula, replacements=Dict{Variable, Variable}())
     @match formula begin
     f::Negation => Negation(

src/resolution.jl

@@ -1,5 +1,12 @@
 export is_satisfiable
 
+"""
+    get_most_general_unifier(unifiables::Set{<:Unifiable})
+
+Returns the most general unifier of `unifiable1` and `unifiable2`.
+
+This is a naive implementation of a unification algorithm. It is supposed to be comprehensible.
+"""
 function get_most_general_unifier(unifiables::Set{<:Unifiable})
     unifier = Substitution()
     unified = first(unifiables)
@@ -10,6 +17,13 @@ function get_most_general_unifier(unifiables::Set{<:Unifiable})
     unifier
 end
 
+"""
+    most_general_unifier!(unifier!::Substitution, unifiable1::Unifiable, unifiable2::Unifiable)
+
+Computes the most general unifier of `unifiable1` and `unifiable2` and stores it in `unifier!`.
+
+This is a naive implementation of a unification algorithm. It is supposed to be comprehensible.
+"""
 function most_general_unifier!(unifier!::Substitution, unifiable1::Unifiable, unifiable2::Unifiable)
     substituted_unifiable1 = substitute(unifiable1, unifier!)
     substituted_unifiable2 = substitute(unifiable2, unifier!)
@@ -65,7 +79,16 @@ function most_general_unifier!(unifier!::Substitution, unifiable1::Unifiable, un
     end
 end
 
-# Apply substitution in order.
+"""
+    substitute(formula::Union{Term, Formula, Literal, Clause}, substitution::Substitution)
+
+Return `formula` with all entries in `substitution` applied in order.
+
+A `substitution` entry consists of a variable and a term. An entry is applied by replacing all
+occurrences of the variable with the term.
+"""
+function substitute end
+
 function substitute(formula::Union{Term, Formula, Literal, Clause}, substitution::Substitution)
     substituted_formula = formula
     for (substitutee, substituter) in substitution
@@ -103,6 +126,14 @@ function substitute(formula::Union{Term, Formula, Literal, Clause}, substitutee,
     end
 end
 
+"""
+    rename_all_variables(formula, replacements=Dict{Variable, Variable}())
+
+Return `formula` with all variables replace by new, unique names. The returned
+formula is logically equivalent to `formula`.
+
+The `replacements` dictionary is for internal use only.
+"""
 function rename_all_variables(formula, replacements=Dict{Variable, Variable}())
     @match formula begin
     f::Clause => @applyrecursively rename_all_variables(:_, replacements) f Clause
@@ -134,6 +165,16 @@ function rename_all_variables(formula, replacements=Dict{Variable, Variable}())
     end
 end
 
+"""
+    get_maybe_unifiable_literals(clause1::Clause, clause2::Clause)
+
+Return a set of clauses that might be unifiable.
+
+Each returned clause consists of literals in `clause1` and literals in
+`clause2`. To be considered unifiable, the selected literals in `clause1`
+must have the opposite negation of the literals in `clause2`. This function
+is used to reduce the search space for literals for the unification algorithm.
+"""
 function get_maybe_unifiable_literals(clause1::Clause, clause2::Clause)
     maybe_unifiable_literals = Set{Set{Literal}}()
     all_literals = union(clause1, clause2)
@@ -159,6 +200,21 @@ function get_maybe_unifiable_literals(clause1::Clause, clause2::Clause)
     maybe_unifiable_literals
 end
 
+"""
+    is_satisfiable(formula; maxsearchdepth)
+
+Check if `formula` is satisfiable.
+
+If `formula` is unsatisfiable, this function will return `false` in finite time.
+If `formula` is satisfiable, this function may run forever. This behavior stems
+from the fundamental limit that the satisfiability problem for first-order logic
+is semidecidable. The `maxsearchdepth` parameter allows you to work around this
+limitation by specifying the maximum expansion depth of the resolution algorithm
+search tree. If the algorithm exceeds that limit, it throws an OverMaxSearchDepthError
+exception.
+"""
+function is_satisfiable end
+
 function is_satisfiable(clauses::CNF; maxsearchdepth=Inf)
     if maxsearchdepth == 0
         throw(OverMaxSearchDepthError())

src/skolem_normal_form.jl

@@ -1,5 +1,12 @@
 export get_skolem_normal_form
+"""
+    get_skolem_normal_form(formula, replacements=Dict{Variable, Function}(), all_quantifiers=Vector{Variable}())
 
+Returns the [skolem normal form](https://en.wikipedia.org/wiki/Skolem_normal_form) of `formula`.
+
+`replacements` and `all_quantifiers` are optional arguments that are only used internally.
+The returned formula is equisatisfiable with `formula`.
+"""
 function get_skolem_normal_form(formula, replacements=Dict{Variable, Function}(), all_quantifiers=Vector{Variable}())
     @match formula begin
     f::AFormula => begin

src/testing_helpers.jl

@@ -3,13 +3,22 @@ using Base.Test
 export @customtest,
     @customtest_throws
 
+#=
+customtest and customtest_throws are wrappers around the normal
+@test and @test_throws macros. They ensure that the test execution
+is independent of the test order by resetting the interal package state.
+Currently, the internal package state consists only of the next free
+symbol.
+=#
+
 macro customtest(test)
     quote
     resetfreesymbols()
     @test $(esc(test))
     resetfreesymbols()
     end
 end
+
 macro customtest_throws(exception, test)
     quote
     resetfreesymbols()