From 4bf3a8b67fcf54d6037dd0937aed57a0db555538 Mon Sep 17 00:00:00 2001
From: Thomas Leonard <talex5@gmail.com>
Date: Thu, 25 Mar 2010 22:10:11 +0000
Subject: [PATCH] Test SAT learning

---
 tests/testsat.py               | 28 +++++++++++++++++++++++++---
 zeroinstall/injector/sat.py    |  8 ++++----
 zeroinstall/injector/solver.py |  4 ----
 3 files changed, 29 insertions(+), 11 deletions(-)

diff --git a/tests/testsat.py b/tests/testsat.py
index 1bf8062..673313f 100755
--- a/tests/testsat.py
+++ b/tests/testsat.py
@@ -27,6 +27,7 @@ class Version:
 	def __init__(self, n):
 		self.n = n
 		self.requires = []
+		self.arch = None
 
 	def add_requires(self, lib, min_v, max_v):
 		self.requires.append((lib, min_v, max_v))
@@ -53,10 +54,13 @@ class Program:
 
 		i = 0
 		for version in self.versions.values():
-			impl = child(root, 'implementation', {
+			attrs = {
 				'id': str(i),
 				'version': str(version.n),
-			})
+			}
+			if version.arch:
+				attrs['arch'] = version.arch
+			impl = child(root, 'implementation', attrs)
 			child(impl, 'manifest-digest', {'sha1new': '1234'})
 			for lib, min_v, max_v in version.requires:
 				req = child(impl, 'requires', {'interface': uri_prefix + lib})
@@ -97,8 +101,12 @@ def assertSelection(expected, repo):
 		if ':' in line:
 			prog, versions = line.split(':')
 			prog = prog.strip()
+			if ' ' in prog:
+				prog, prog_arch = prog.split()
+			else:
+				prog_arch = None
 			for v in versions.split():
-				cache.get_prog(prog).get_version(v)
+				cache.get_prog(prog).get_version(v).arch = prog_arch
 		elif '=>' in line:
 			prog, requires = line.split('=>')
 			prog, version_range = prog.strip().split('[')
@@ -195,6 +203,20 @@ class TestSAT(BaseTest):
 			prog[1,2] => liba 1 2
 			""")
 
+	def testLearning(self):
+		# Prog-2 depends on libb and libz, but we can't have both
+		# at once. The learning means we don't have to explore every
+		# possible combination of liba and libb.
+		assertSelection("prog-1", """
+			prog: 1 2
+			liba: 1 2 3
+			libb Linux-i486: 1 2 3
+			libz Linux-x86_64: 1 2
+			prog[2] => liba 1 3
+			prog[2] => libz 1 2
+			liba[1,3] => libb 1 3
+			""")
+
 suite = unittest.makeSuite(TestSAT)
 if __name__ == '__main__':
 	sys.argv.append('-v')
diff --git a/zeroinstall/injector/sat.py b/zeroinstall/injector/sat.py
index 684a03d..f4904a6 100644
--- a/zeroinstall/injector/sat.py
+++ b/zeroinstall/injector/sat.py
@@ -63,7 +63,7 @@ def makeAtMostOneClause(solver):
 			assert solver.lit_value(lit) == True
 			assert lit >= 0
 
-			debug("%s: noticed %s has become True" % (self, solver.name_lit(lit)))
+			#debug("%s: noticed %s has become True" % (self, solver.name_lit(lit)))
 
 			# One is already selected
 			if self.current is not None:
@@ -99,7 +99,7 @@ def makeAtMostOneClause(solver):
 			return True
 
 		def undo(self, lit):
-			debug("backtracking: no longer selected %s" % solver.name_lit(lit))
+			debug("(backtracking: no longer selected %s)" % solver.name_lit(lit))
 			assert lit == self.current
 			self.current = None
 
@@ -171,7 +171,7 @@ def makeUnionClause(solver):
 		def propagate(self, lit):
 			# value[get(lit)] has just become False
 
-			debug("%s: noticed %s has become False" % (self, solver.name_lit(neg(lit))))
+			#debug("%s: noticed %s has become False" % (self, solver.name_lit(neg(lit))))
 
 			# For simplicity, only handle the case where self.lits[1]
 			# is the one that just got set to False, so that:
@@ -321,7 +321,7 @@ class Solver(object):
 	# Process the propQ.
 	# Returns None when done, or the clause that caused a conflict.
 	def propagate(self):
-		debug("propagate: queue length = %d", len(self.propQ))
+		#debug("propagate: queue length = %d", len(self.propQ))
 		while self.propQ:
 			lit = self.propQ[0]
 			del self.propQ[0]
diff --git a/zeroinstall/injector/solver.py b/zeroinstall/injector/solver.py
index 05d7cc2..cbbfaa3 100644
--- a/zeroinstall/injector/solver.py
+++ b/zeroinstall/injector/solver.py
@@ -371,14 +371,10 @@ class SATSolver(Solver):
 			m_group = 'm%d' % machine_group
 			var[m_group] = problem.add_variable(m_group)
 			if impls:
-				if comment_problem:
-					problem.append("* define machine group %d" % m_group)
 				for impl in impls:
 					problem.add_clause([var[m_group], sat.neg(var[impl])])
 			m_groups.append(var[m_group])
 		if m_groups:
-			if comment_problem:
-				problem.append("* select implementations from at most one machine group")
 			m_groups_clause = problem.at_most_one(m_groups)
 		else:
 			m_groups_clause = None
-- 
2.11.4.GIT