refactor uninterpreted functions

* implement mini eDSL for writing constraints in ghci * compute minimial infeasible constraint subsets when solver finds a conflict * communicate conflicts to SAT solver * also clean-up some unused files
gruhn · Jul 30, 2023 · 6e6732d · 6e6732d
1 parent 6728683
commit 6e6732d
Show file tree

Hide file tree

Showing 27 changed files with 471 additions and 3,434 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
diff --git a/README.md b/README.md
@@ -0,0 +1 @@
+
diff --git a/SMT.cabal b/SMT.cabal
@@ -14,8 +14,8 @@ library
                     , Theory
                     , Theory.Propositions
                     , Theory.BitVectors
-                    , Theory.UninterpretedFunctions.Lazy
-                    , Theory.UninterpretedFunctions.Eager
+                    , Theory.UninterpretedFunctions
+                    , Theory.UninterpretedFunctions.EDSL
                     , Theory.LinearArithmatic.Constraint
                     , Theory.LinearArithmatic.FourierMotzkin
                     , Theory.LinearArithmatic.Simplex
@@ -38,6 +38,7 @@ library
                     , mtl
                     , extra
                     , vector
+                    , search-algorithms
     hs-source-dirs:   src
     default-language: Haskell2010
     default-extensions: 
@@ -51,7 +52,7 @@ library
 test-suite test
     type:             exitcode-stdio-1.0 
     main-is:          Test.hs
-    other-modules:    GameUnequal
+    other-modules:    TestUninterpretedFunctions
                     , TestNonLinearRealArithmatic
                     , TestLinearArithmatic
                     , TestSAT

diff --git a/minisat/Dockerfile b/minisat/Dockerfile
diff --git a/minisat/dimacs/game-unequal.cnf b/minisat/dimacs/game-unequal.cnf