From 0b12ba0ca00f7cdfb50b614fb24b673fb7e4e322 Mon Sep 17 00:00:00 2001
From: Matthew Sotoudeh <matthew@masot.net>
Date: Fri, 14 Jul 2023 07:25:31 -0700
Subject: initial code

---
 example/symabs.py | 62 +++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 62 insertions(+)
 create mode 100644 example/symabs.py

(limited to 'example/symabs.py')

diff --git a/example/symabs.py b/example/symabs.py
new file mode 100644
index 0000000..a74db27
--- /dev/null
+++ b/example/symabs.py
@@ -0,0 +1,62 @@
+import sys
+import itertools
+from satispi import *
+
+def symabs(smtlib, exprs, types, cutoffs):
+    if len(exprs) == 0: return []
+
+    if Solver.singleton().model(smtlib) is None:
+        return [frozenset() for _ in exprs]
+
+    smtlib = smtlib.copy()
+
+    vars_ = [Variable(f"____symabs{i}", types[i]) for i in range(len(exprs))]
+    smtlib += [Term("=", var, expr) for var, expr in zip(vars_, exprs)]
+
+    possible = [frozenset() for _ in exprs]
+    aim_for = max(len(possible) // 8, 1)
+    for i in itertools.count():
+        distinction = [bvize(Term("distinct", v, *map(wordlit, sorted(p))))
+                       for v, p in zip(vars_, possible)
+                       if p and p is not True]
+
+        if i > 0 and not distinction:
+            # everything is Top
+            return possible
+
+        if len(distinction) == 1:
+            n_deltas = Term("bvadd", *distinction, wordlit(0))
+        else:
+            n_deltas = Term("bvadd", *distinction)
+
+        # aim_for <= n distincts.
+        # if aim_for = 1 and it's unsat, then impossible to get any distincts
+        goal = []
+        if distinction:
+            goal = [Term("bvult", wordlit(aim_for - 1), n_deltas)]
+
+        use_vars = [v for v, p in zip(vars_, possible) if p is not True]
+        model = Solver.singleton().model(smtlib + goal, use_vars)
+
+        if model is None:
+            assert aim_for >= 0
+            if aim_for > 1:
+                aim_for = max(aim_for // 2, 1)
+                continue
+            return possible
+
+        prior = possible.copy()
+        for i, (v, c) in enumerate(zip(vars_, cutoffs)):
+            if possible[i] is True: continue
+            if model[v.name] is None: continue
+            possible[i] = possible[i] | frozenset({model[v.name]})
+            if c is not None and len(possible[i]) > c:
+                possible[i] = True
+        assert possible != prior, \
+            "Solver did not return a complete enough model to make progress"
+
+def wordlit(val):
+    return Literal(f"(_ bv{val} 32)")
+
+def bvize(term):
+    return Term("ite", term, wordlit(1), wordlit(0))
-- 
cgit v1.2.3