Embed 0install SAT solver to avoid fetching the entire ZI disribution

3 files changed, 105 insertions, 4 deletions

diff --git a/tests/__init__.py b/tests/__init__.py
index b93e388..81c8b4e 100644
--- a/tests/__init__.py
+++ b/tests/__init__.py
@@ -24,7 +24,6 @@ from sugar_network.db import files
 from sugar_network.client import IPCConnection, journal, routes as client_routes
 from sugar_network.client.routes import ClientRoutes, _Auth
 from sugar_network import db, client, node, toolkit, model
-from sugar_network.client import solver
 from sugar_network.model.user import User
 from sugar_network.model.context import Context
 from sugar_network.model.post import Post
@@ -116,9 +115,6 @@ class Test(unittest.TestCase):
         http._RECONNECTION_NUMBER = 0
         toolkit.cachedir.value = tmpdir + '/tmp'
         journal._ds_root = tmpdir + '/datastore'
-        solver.nodeps = False
-        solver._stability = None
-        solver._conn = None
         downloads._POOL_SIZE = 256
         gbus.join()
 
diff --git a/tests/units/toolkit/__main__.py b/tests/units/toolkit/__main__.py
index 68cb254..0e33682 100644
--- a/tests/units/toolkit/__main__.py
+++ b/tests/units/toolkit/__main__.py
@@ -13,6 +13,7 @@ from spec import *
 from router import *
 from gbus import *
 from i18n import *
+from sat import *
 
 if __name__ == '__main__':
     tests.main()
diff --git a/tests/units/toolkit/sat.py b/tests/units/toolkit/sat.py
new file mode 100755
index 0000000..4202789
--- /dev/null
+++ b/tests/units/toolkit/sat.py
@@ -0,0 +1,104 @@
+#!/usr/bin/env python
+# sugar-lint: disable
+
+from __init__ import tests
+
+from sugar_network.toolkit import sat
+
+
+class SAT(tests.Test):
+
+    def test_AtMostOne(self):
+        self.assertEqual(
+                {'c': 1},
+                sat.solve([[1]], {'c': [1]}, decide))
+        self.assertEqual(
+                {'c': 1},
+                sat.solve([[1, 2]], {'c': [1, 2]}, decide))
+        self.assertEqual(
+                {'c': 1},
+                sat.solve([[1, 2, 3]], {'c': [1, 2, 3]}, decide))
+
+    def test_DeepSolve(self):
+        self.assertEqual({
+            'c1': 1,
+            'c2': 2,
+            'c3': 3,
+            'c4': 5,
+            },
+            sat.solve(
+                [
+                    [1, 6], [-1, 2],
+                    [-2, 3],
+                    [-3, 5],
+                    ],
+                {
+                    'c1': [1, 6],
+                    'c2': [2],
+                    'c3': [3],
+                    'c4': [4, 5],
+                    },
+                decide))
+
+    def test_SwitchToAnotherBranch(self):
+        self.assertEqual({
+            'c1': 6,
+            'c4': 4,
+            },
+            sat.solve(
+                [
+                    [1, 6], [-1, 2], [-6, 4],
+                    [-2, 3], [-2, 4],
+                    [-3, 5],
+                    ],
+                {
+                    'c1': [1, 6],
+                    'c2': [2],
+                    'c3': [3],
+                    'c4': [4, 5],
+                    },
+                decide))
+
+    def __test_zi(self):
+        from zeroinstall.injector import sat
+
+        problem = sat.Problem()
+
+        v1 = problem.add_variable(1)
+        v2 = problem.add_variable(2)
+        v3 = problem.add_variable(3)
+        v4 = problem.add_variable(4)
+        v5 = problem.add_variable(5)
+        v6 = problem.add_variable(6)
+
+        c1 = problem.at_most_one([v1, v6])
+        problem.add_clause([v1, v6])
+        problem.add_clause([sat.neg(v1), v2])
+        problem.add_clause([sat.neg(v6), v4])
+
+        c2 = problem.at_most_one([v2])
+        problem.add_clause([sat.neg(v2), v3])
+        problem.add_clause([sat.neg(v2), v4])
+
+        c3 = problem.at_most_one([v3])
+        problem.add_clause([sat.neg(v3), v5])
+
+        c4 = problem.at_most_one([v4, v5])
+
+        assert problem.run_solver(lambda: decide({'c1': c1, 'c2': c2, 'c3': c3, 'c4': c4}))
+        self.assertEqual(v6, c1.current)
+        self.assertEqual(None, c2.current)
+        self.assertEqual(None, c3.current)
+        self.assertEqual(v4, c4.current)
+
+
+def decide(clauses):
+    for i in clauses.values():
+        if i.current is None:
+            r = i.best_undecided()
+            if r is not None:
+                return r
+
+
+if __name__ == '__main__':
+    tests.main()