From 0232383191dab226f8ca0e993c31cbce039a2c2c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 15 Sep 2018 16:59:06 -0700
Subject: [PATCH] mini IC3 sample

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 examples/python/data/horn1.smt2 |  50 +++++
 examples/python/data/horn2.smt2 |  44 ++++
 examples/python/mini_ic3.py     | 363 ++++++++++++++++++++++++++++++++
 3 files changed, 457 insertions(+)
 create mode 100644 examples/python/data/horn1.smt2
 create mode 100644 examples/python/data/horn2.smt2
 create mode 100644 examples/python/mini_ic3.py

diff --git a/examples/python/data/horn1.smt2 b/examples/python/data/horn1.smt2
new file mode 100644
index 000000000..20d043534
--- /dev/null
+++ b/examples/python/data/horn1.smt2
@@ -0,0 +1,50 @@
+(declare-rel Goal (Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool))
+(declare-rel Invariant (Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool))
+(declare-var A Bool)
+(declare-var B Bool)
+(declare-var C Bool)
+(declare-var D Bool)
+(declare-var E Bool)
+(declare-var F Bool)
+(declare-var G Bool)
+(declare-var H Bool)
+(declare-var I Bool)
+(declare-var J Bool)
+(declare-var K Bool)
+(declare-var L Bool)
+(declare-var M Bool)
+(declare-var N Bool)
+(declare-var O Bool)
+(declare-var P Bool)
+(declare-var Q Bool)
+(declare-var R Bool)
+(declare-var S Bool)
+(declare-var T Bool)
+(declare-var U Bool)
+(declare-var V Bool)
+(declare-var W Bool)
+(declare-var X Bool)
+(rule (=> (not (or L K J I H G F E D C B A)) (Invariant L K J I H G F E D C B A)))
+(rule (let ((a!1 (and (Invariant X W V U T S R Q P O N M)
+                (=> (not (and true)) (not F))
+                (=> (not (and true)) (not E))
+                (=> (not (and W)) (not D))
+                (=> (not (and W)) (not C))
+                (=> (not (and U)) (not B))
+                (=> (not (and U)) (not A))
+                (= L (xor F X))
+                (= K (xor E W))
+                (= J (xor D V))
+                (= I (xor C U))
+                (= H (xor B T))
+                (= G (xor A S))
+                (=> D (not E))
+                (=> C (not E))
+                (=> B (not C))
+                (=> A (not C))
+                ((_ at-most 5) L K J I H G))))
+  (=> a!1 (Invariant L K J I H G F E D C B A))))
+(rule (=> (and (Invariant L K J I H G F E D C B A) L (not K) J (not I) H G)
+    (Goal L K J I H G F E D C B A)))
+
+(query Goal)
\ No newline at end of file
diff --git a/examples/python/data/horn2.smt2 b/examples/python/data/horn2.smt2
new file mode 100644
index 000000000..478c39d5f
--- /dev/null
+++ b/examples/python/data/horn2.smt2
@@ -0,0 +1,44 @@
+(declare-rel Invariant (Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool))
+(declare-rel Goal (Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool))
+(declare-var A Bool)
+(declare-var B Bool)
+(declare-var C Bool)
+(declare-var D Bool)
+(declare-var E Bool)
+(declare-var F Bool)
+(declare-var G Bool)
+(declare-var H Bool)
+(declare-var I Bool)
+(declare-var J Bool)
+(declare-var K Bool)
+(declare-var L Bool)
+(declare-var M Bool)
+(declare-var N Bool)
+(declare-var O Bool)
+(declare-var P Bool)
+(declare-var Q Bool)
+(declare-var R Bool)
+(declare-var S Bool)
+(declare-var T Bool)
+(rule (=> (not (or J I H G F E D C B A)) (Invariant J I H G F E D C B A)))
+(rule (let ((a!1 (and (Invariant T S R Q P O N M L K)
+                (=> (not (and true)) (not E))
+                (=> (not (and T)) (not D))
+                (=> (not (and S)) (not C))
+                (=> (not (and R)) (not B))
+                (=> (not (and Q)) (not A))
+                (= J (xor E T))
+                (= I (xor D S))
+                (= H (xor C R))
+                (= G (xor B Q))
+                (= F (xor A P))
+                (=> D (not E))
+                (=> C (not D))
+                (=> B (not C))
+                (=> A (not B))
+                ((_ at-most 3) J I H G F))))
+  (=> a!1 (Invariant J I H G F E D C B A))))
+(rule (=> (and (Invariant J I H G F E D C B A) (not J) (not I) (not H) (not G) F)
+    (Goal J I H G F E D C B A)))
+
+(query Goal)
diff --git a/examples/python/mini_ic3.py b/examples/python/mini_ic3.py
new file mode 100644
index 000000000..3ca126a2f
--- /dev/null
+++ b/examples/python/mini_ic3.py
@@ -0,0 +1,363 @@
+from z3 import *
+import heapq
+
+
+# Simplistic (and fragile) converter from
+# a class of Horn clauses corresponding to 
+# a transition system into a transition system
+# representation as <init, trans, goal>
+# It assumes it is given three Horn clauses
+# of the form:
+#  init(x) => Invariant(x)
+#  Invariant(x) and trans(x,x') => Invariant(x')
+#  Invariant(x) and goal(x) => Goal(x)
+# where Invariant and Goal are uninterpreted predicates
+    
+class Horn2Transitions:
+    def __init__(self):
+        self.trans = True
+        self.init = True
+        self.goal = True
+        self.index = 0
+        
+    def parse(self, file):
+        fp = Fixedpoint()
+        goals = fp.parse_file(file)
+        for r in fp.get_rules():
+            if not is_quantifier(r):
+                continue
+            b = r.body()
+            if not is_implies(b):
+                continue
+            f = b.arg(0)
+            g = b.arg(1)
+            if self.is_goal(f, g):
+                continue
+            if self.is_transition(f, g):
+                continue
+            if self.is_init(f, g):
+                continue
+
+    def is_pred(self, p, name):
+        return is_app(p) and p.decl().name() == name
+    
+    def is_goal(self, body, head):
+        if not self.is_pred(head, "Goal"):
+            return False
+        pred, inv = self.is_body(body)
+        if pred is None:
+            return False
+        self.goal = self.subst_vars("x", inv, pred)
+        return True
+
+    def is_body(self, body):
+        if not is_and(body):
+            return None, None
+        fmls = [f for f in body.children() if self.is_inv(f) is None]
+        inv = None
+        for f in body.children():
+            if self.is_inv(f) is not None:
+                inv = f;
+                break
+        return And(fmls), inv
+
+    def is_inv(self, f):
+        if self.is_pred(f, "Invariant"):
+            return f
+        return None
+
+    def is_transition(self, body, head):
+        pred, inv0 = self.is_body(body)
+        if pred is None:
+            return False
+        inv1 = self.is_inv(head)
+        if inv1 is None:
+            return False
+        pred = self.subst_vars("x",  inv0, pred)
+        self.xs = self.vars
+        pred = self.subst_vars("xn", inv1, pred)
+        self.xns = self.vars
+        self.trans = pred
+        return True
+
+    def is_init(self, body, head):
+        for f in body.children():
+            if self.is_inv(f) is not None:
+               return False
+        inv = self.is_inv(head)
+        if inv is None:
+            return False
+        self.init = self.subst_vars("x", inv, body)
+        return True
+    
+    def subst_vars(self, prefix, inv, fml):
+        subst = self.mk_subst(prefix, inv)
+        self.vars = [ v for (k,v) in subst ]
+        return substitute(fml, subst)
+
+    def mk_subst(self, prefix, inv):
+        self.index = 0
+        return [(f, self.mk_bool(prefix)) for f in inv.children()]
+
+    def mk_bool(self, prefix):
+        self.index += 1
+        return Bool("%s%d" % (prefix, self.index))
+
+# Produce a finite domain solver.
+# The theory QF_FD covers bit-vector formulas
+# and pseudo-Boolean constraints.
+# By default cardinality and pseudo-Boolean 
+# constraints are converted to clauses. To override
+# this default for cardinality constraints
+# we set sat.cardinality.solver to True
+
+def fd_solver():
+    s = SolverFor("QF_FD")
+    s.set("sat.cardinality.solver", True)
+    return s
+
+
+# negate, avoid double negation
+def negate(f):
+    if is_not(f):
+        return f.arg(0)
+    else:
+        return Not(f)
+
+def cube2clause(cube):
+    return Or([negate(f) for f in cube])
+
+class State:
+    def __init__(self, s):
+        self.R = set([])
+        self.solver = s
+
+    def add(self, clause):
+        self.R |= { clause }
+        self.solver.add(clause)
+    
+class Goal:
+    def __init__(self, cube, parent, level):
+        self.level = level
+        self.cube = cube
+        self.parent = parent
+
+# push a goal on a heap
+def push_heap(heap, goal):
+    heapq.heappush(heap, (goal.level, goal))
+                
+class MiniIC3:
+    def __init__(self, init, trans, goal, x0, xn):
+        self.x0 = x0
+        self.xn = xn
+        self.init = init
+        self.bad = goal
+        self.trans = trans
+        self.min_cube_solver = fd_solver()
+        self.min_cube_solver.add(Not(trans))
+        self.goals = []
+        s = State(fd_solver())
+        s.add(init)
+        s.solver.add(trans)
+        self.states = [s]
+        self.s_bad = fd_solver()
+        self.s_good = fd_solver()
+        self.s_bad.add(self.bad)
+        self.s_good.add(Not(self.bad))        
+        
+    def next(self, f):
+        if isinstance(f, list) or isinstance(f, tuple) or isinstance(f, AstVector):
+           return [self.next(f1) for f1 in f]
+        return substitute(f, zip(self.x0, self.xn))    
+    
+    def prev(self, f):
+        if isinstance(f, list) or isinstance(f, tuple) or isinstance(f, AstVector):
+           return [self.prev(f1) for f1 in f]
+        return substitute(f, zip(self.xn, self.x0))    
+    
+    def add_solver(self):
+        s = fd_solver()
+        s.add(self.trans)
+        self.states += [State(s)]
+        
+    # Check if the initial state is bad
+    def check_init(self):
+        s = fd_solver()
+        s.add(self.bad)
+        s.add(self.init)
+        return unsat == s.check()
+
+    # Remove clauses that are subsumed
+    def prune(self, i):
+        removed = set([])
+        s = fd_solver()
+        for f1 in self.states[i].R:
+            s.push()
+            for f2 in self.states[i].R:
+                if f2 not in removed:
+                    s.add(Not(f2) if f1.eq(f2) else f2)
+            if s.check() == unsat:
+                removed |= { f1 }
+            s.pop()
+        self.states[i].R = self.states[i].R - removed
+
+    def R(self, i):
+        return And(self.states[i].R)
+
+    # Check if there are two states next to each other that have the same clauses.
+    def is_valid(self):
+        i = 1
+        while i + 1 < len(self.states):
+            if not (self.states[i].R - self.states[i+1].R):
+               self.prune(i)
+               return self.R(i)
+            i += 1
+        return None
+
+    def value2literal(self, m, x):
+        value = m.eval(x)
+        if is_true(value):
+            return x
+        if is_false(value):
+            return Not(x)
+        return None
+
+    def values2literals(self, m, xs):
+        p = [self.value2literal(m, x) for x in xs]
+        return [x for x in p if x is not None]
+
+    def project0(self, m):
+        return self.values2literals(m, self.x0)
+
+    def projectN(self, m):
+        return self.values2literals(m, self.xn)
+
+    # Determine if there is a cube for the current state 
+    # that is potentially reachable.
+    def unfold(self):
+        core = []
+        self.s_bad.push()
+        R = self.R(len(self.states)-1)
+        self.s_bad.add(R)
+        is_sat = self.s_bad.check()
+        if is_sat == sat:
+           m = self.s_bad.model()
+           props = self.project0(m)
+           self.s_good.push()
+           self.s_good.add(R)
+           is_sat2 = self.s_good.check(props)
+           assert is_sat2 == unsat
+           core = self.s_good.unsat_core()
+           self.s_good.pop()
+        self.s_bad.pop()
+        return is_sat, core
+
+    # Block a cube by asserting the clause corresponding to its negation
+    def block_cube(self, i, cube):
+        self.assert_clause(i, cube2clause(cube))
+
+    # Add a clause to levels 0 until i
+    def assert_clause(self, i, clause):
+        for j in range(i + 1):
+            if clause not in self.states[j].R:
+                self.states[j].add(clause)
+
+    # minimize cube that is core of Dual solver.
+    # this assumes that props & cube => Trans    
+    def minimize_cube(self, cube, lits):
+        is_sat = self.min_cube_solver.check(lits + [c for c in cube])
+        assert is_sat == unsat
+        core = self.min_cube_solver.unsat_core()
+        assert core
+        return [c for c in core if c in set(cube)]
+
+    # A state s0 and level f0 such that
+    # not(s0) is f0-1 inductive
+    def ic3_blocked(self, s0, f0):
+        push_heap(self.goals, Goal(self.next(s0), None, f0))
+        while self.goals:
+            f, g = heapq.heappop(self.goals)
+            sys.stdout.write("%d." % f)
+            sys.stdout.flush()
+            # Not(g.cube) is f-1 invariant
+            if f == 0:
+               print("")
+               return g
+            cube, f, is_sat = self.is_inductive(f, g.cube)
+            if is_sat == unsat:
+               self.block_cube(f, self.prev(cube))
+               if f < f0:
+                  push_heap(self.goals, Goal(g.cube, g.parent, f + 1))
+            elif is_sat == sat:
+               push_heap(self.goals, Goal(cube, g, f - 1))
+               push_heap(self.goals, g)
+            else:
+               return is_sat
+        print("")
+        return None
+
+    # Rudimentary generalization:
+    # If the cube is already unsat with respect to transition relation
+    # extract a core (not necessarily minimal)
+    # otherwise, just return the cube.
+    def generalize(self, cube, f):
+        s = self.states[f - 1].solver
+        if unsat == s.check(cube):
+            return s.unsat_core(), f
+        return cube, f
+
+    # Check if the negation of cube is inductive at level f
+    def is_inductive(self, f, cube):
+        s = self.states[f - 1].solver
+        s.push()
+        s.add(self.prev(Not(And(cube))))
+        is_sat = s.check(cube)
+        if is_sat == sat:
+           m = s.model()
+        s.pop()
+        if is_sat == sat:
+           cube = self.next(self.minimize_cube(self.project0(m), self.projectN(m)))
+        elif is_sat == unsat:
+           cube, f = self.generalize(cube, f)
+        return cube, f, is_sat
+                        
+    def run(self):
+        if not self.check_init():
+           return "goal is reached in initial state"
+        level = 0
+        while True:
+            inv = self.is_valid()
+            if inv is not None:
+                return inv
+            is_sat, cube = self.unfold()
+            if is_sat == unsat:
+               level += 1
+               print("Unfold %d" % level)
+               sys.stdout.flush()
+               self.add_solver()
+            elif is_sat == sat:
+               cex = self.ic3_blocked(cube, level)
+               if cex is not None:
+                  return cex
+            else:
+               return is_sat  
+
+def test(file):
+    h2t = Horn2Transitions()
+    h2t.parse(file)
+    mp = MiniIC3(h2t.init, h2t.trans, h2t.goal, h2t.xs, h2t.xns)
+    result = mp.run()    
+    if isinstance(result, Goal):
+       g = result
+       print("Trace")
+       while g:
+          print(g.level, g.cube)
+          g = g.parent
+       return
+    if isinstance(result, ExprRef):
+       print("Invariant:\n%s " % result)
+       return
+    print(result)
+
+test("data/horn1.smt2")
+test("data/horn2.smt2")