From a943926fa31df288af676f73d51bcd1631fe5010 Mon Sep 17 00:00:00 2001 From: Connor Olding Date: Wed, 8 Jun 2022 05:18:48 +0200 Subject: [PATCH] logic: add yices_solution.py --- logic/yices_solution.py | 62 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 62 insertions(+) create mode 100644 logic/yices_solution.py diff --git a/logic/yices_solution.py b/logic/yices_solution.py new file mode 100644 index 0000000..0327154 --- /dev/null +++ b/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)