resolution.jl: Add conveniency methods for is_satisfiable.

The new methods allow testing a formula that has not been converted
to a normal form yet.

Author: roberthoenig

src/resolution.jl

@@ -187,4 +187,20 @@ function is_satisfiable(clauses::CNF; maxsearchdepth=Inf)
     else
         is_satisfiable(clauses, maxsearchdepth=maxsearchdepth-1)
     end
-end
+end
+
+function is_satisfiable(formula::Formula; maxsearchdepth=Inf)
+    is_satisfiable(
+        get_conjunctive_normal_form(
+            get_removed_quantifier_form(
+                get_skolem_normal_form(
+                    get_prenex_normal_form(
+                        get_quantified_variables_form(
+                            get_renamed_quantifiers_form(
+                                formula)))))),
+        maxsearchdepth=maxsearchdepth
+    )
+end
+
+is_satisfiable(formula::String; maxsearchdepth=Inf) =
+    is_satisfiable(Formula(formula), maxsearchdepth=maxsearchdepth)

test/test_resolution.jl

@@ -1,13 +1,3 @@
-function get_normalized_form(formula::String)
-    get_conjunctive_normal_form(
-        get_removed_quantifier_form(
-            get_skolem_normal_form(
-                get_prenex_normal_form(
-                    get_quantified_variables_form(
-                        get_renamed_quantifiers_form(
-                            Formula(formula)))))))
-end
-
 function testsatisfiability(formula, issatisfiable; maxsearchdepth=5)
     if issatisfiable == false
         @customtest is_satisfiable(formula, maxsearchdepth=maxsearchdepth) == false
@@ -18,14 +8,14 @@ end
 
 @testset "is_satisfiable" begin
     # Basic tests, easy to verify by hand.
-    testsatisfiability(get_normalized_form("P(x) & ~P(x)"), false)
-    testsatisfiability(get_normalized_form("P(x) & ~P(y)"), true)
-    testsatisfiability(get_normalized_form("(P(x) & ~P(y)) & (~P(x) & P(y))"), false)
-    testsatisfiability(get_normalized_form("(P(x) & ~P(y)) | (C(y) & ~C(y))"), true)
-    testsatisfiability(get_normalized_form("A() & (B() | ~C()) & ~B() & C()"), false)
-    testsatisfiability(get_normalized_form("*{x}(P(x) & ~P(f(x)))"), false)
-    testsatisfiability(get_normalized_form("(S(x,p) | G(p)) & (~L(x) | G(p)) & (~S(x,p)) & (~G(p))"), false)
-    testsatisfiability(get_normalized_form("(S(x,p) | G(p)) & (~L(x) | G(p))"), true)
+    testsatisfiability("P(x) & ~P(x)", false)
+    testsatisfiability("P(x) & ~P(y)", true)
+    testsatisfiability("(P(x) & ~P(y)) & (~P(x) & P(y))", false)
+    testsatisfiability("(P(x) & ~P(y)) | (C(y) & ~C(y))", true)
+    testsatisfiability("A() & (B() | ~C()) & ~B() & C()", false)
+    testsatisfiability("*{x}(P(x) & ~P(f(x)))", false)
+    testsatisfiability("(S(x,p) | G(p)) & (~L(x) | G(p)) & (~S(x,p)) & (~G(p))", false)
+    testsatisfiability("(S(x,p) | G(p)) & (~L(x) | G(p))", true)
 
     # Test based on "Logik für Informatiker", exercise 76.
     testsatisfiability(CNF([
@@ -36,10 +26,10 @@ end
         ]), false)
 
     # Test based on "Logik für Informatiker", exercise 76.
-    testsatisfiability(get_normalized_form("((~*{x}(~S(x, p) | L(x))) | G(p)) & ((~?{x}S(x,p)) & (~G(p)))"), false)
+    testsatisfiability("((~*{x}(~S(x, p) | L(x))) | G(p)) & ((~?{x}S(x,p)) & (~G(p)))", false)
 
     # Test based on "Logik für Informatiker", exercise 76.
-    testsatisfiability(get_normalized_form("((~*{x}(~S(x, p) | L(x))) | G(p)) & ((~?{x}S(x,p)) & (G(p)))"), true)
+    testsatisfiability("((~*{x}(~S(x, p) | L(x))) | G(p)) & ((~?{x}S(x,p)) & (G(p)))", true)
 
     # Test based on "Logik für Informatiker", exercise 80.
     testsatisfiability(CNF([