logic: add yices_solution.py

logic/yices_solution.py

@@ -0,0 +1,62 @@
+# reads a solution from a SAT solver, given the original yices-generated CNF.
+
+import sys
+
+if len(sys.argv) == 0:
+    print("You've met with a terrible fate.", file=sys.stderr)
+    sys.exit(1)
+
+if len(sys.argv) != 3:
+    print(f'usage: {sys.argv[0]} {{problem file}} {{solution file}}', file=sys.stderr)
+    sys.exit(1)
+
+prob, sol = sys.argv[1:]
+
+if prob == '-':
+    prob = sys.stdin
+else:
+    prob = open(prob, 'r')
+
+if sol == '-':
+    sol = sys.stdin
+else:
+    sol = open(sol, 'r')
+
+pairs = dict()
+for line in prob:
+    tokens = line.split()
+    if tokens[0] == 'c' and len(tokens) > 4 and tokens[2] == '-->':
+        key = tokens[1]
+        ids = tokens[3:]
+        ids = [t.strip('[]') for t in ids]
+        ids = [int(t) for t in ids]
+        if -1 in ids:
+            continue
+        pairs[key] = ids
+    if tokens[0] == 's':
+        assert tokens[1] == 'SATISFIABLE', 'unsatisfiable'
+        break
+    assert tokens[0] != 'v', 'solution occurred too early to parse'
+
+if prob != sol and prob != sys.stdin:
+    prob.close()
+
+bools = dict()
+for line in sol:
+    tokens = line.split()
+    if tokens[0] == 'v':
+        for i in tokens[1:]:
+            i = int(i)
+            bools[abs(i)] = i > 0
+
+if sol != sys.stdin:
+    sol.close()
+
+bvs = dict((key, 0) for key in pairs.keys())
+for key, ids in pairs.items():
+    for i, id in enumerate(ids):
+        if bools[id]:
+            bvs[key] |= 1 << i
+
+for key, value in bvs.items():
+    print(key, value)