improvement: Balance Formula in Expression Conversion (#7)

Author: maennchen

lib/crux/formula.ex

@@ -113,8 +113,8 @@ defmodule Crux.Formula do
   @spec from_expression(Expression.t(variable)) :: t(variable) when variable: term()
   def from_expression(expression) do
     expression
-    # Expand Booleans so that they do not become variables
-    |> Expression.run(& &1)
+    |> Expression.balance()
+    |> Expression.simplify()
     |> case do
       true ->
         @simple_true

test/crux/formula_test.exs

@@ -23,20 +23,20 @@ defmodule Crux.FormulaTest do
 
       assert %Formula{
                cnf: [
-                 # :a or not :c
-                 [1, -2],
-                 # not :b or not :c
-                 [-3, -2],
                  # :a or :d
-                 [1, 4],
+                 [1, 2],
                  # not :b or :d
-                 [-3, 4]
+                 [-3, 2],
+                 # :a or not :c
+                 [1, -4],
+                 # not :b or not :c
+                 [-3, -4]
                ],
                bindings: %{
                  1 => :a,
-                 2 => :c,
+                 2 => :d,
                  3 => :b,
-                 4 => :d
+                 4 => :c
                }
              } = result
     end