CDCL refactor (#4)

gruhn · Apr 14, 2023 · 48fbdfb · 48fbdfb
1 parent 7ca130e
commit 48fbdfb
Show file tree

Hide file tree

Showing 12 changed files with 321 additions and 423 deletions.
diff --git a/SMT.cabal b/SMT.cabal
@@ -6,14 +6,13 @@ maintainer:         niklas@gruhn.me
 extra-source-files: CHANGELOG.md
 
 library
-    exposed-modules:  CLI
-                    , Expression
+    exposed-modules:  Expression
                     , Assignment
                     , CNF
-                    , Algorithm.LinearResolution
-                    , Algorithm.DPLL
-                    -- , Algorithm.CDCL
-                    , Algorithm.CDCL2
+                    , SAT.DPLL
+                    , SAT.CDCL
+                    , Theory
+                    , Theory.Propositions
                     , Theory.BitVectors
                     , Theory.UninterpretedFunctions.Lazy
                     , Theory.UninterpretedFunctions.Eager
@@ -41,17 +40,21 @@ library
                     , vector
     hs-source-dirs:   src
     default-language: Haskell2010
-    default-extensions: ScopedTypeVariables
-                      , LambdaCase
-                      , StrictData
-                      , TupleSections
+    default-extensions: 
+        ScopedTypeVariables
+      , LambdaCase
+      , StrictData
+      , TupleSections
+      , MultiParamTypeClasses
+      , FunctionalDependencies 
 
 test-suite test
     type:             exitcode-stdio-1.0 
     main-is:          Test.hs
     other-modules:    GameUnequal
                     , TestNonLinearRealArithmatic
                     , TestLinearArithmatic
+                    , TestSAT
     build-depends:    base
                     , SMT
                     , hedgehog

diff --git a/src/Algorithm/CDCL.hs b/src/Algorithm/CDCL.hs