From 37ef3cbeb2cae5bc43f9a42bad91ba5ba3df099d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 20 Nov 2018 14:32:01 -0800
Subject: [PATCH] add rc2 sample

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 examples/python/rc2.py  | 84 +++++++++++++++++++++++++++++++++++++++++
 src/api/python/z3/z3.py |  8 +++-
 2 files changed, 91 insertions(+), 1 deletion(-)
 create mode 100644 examples/python/rc2.py

diff --git a/examples/python/rc2.py b/examples/python/rc2.py
new file mode 100644
index 000000000..a68e41b46
--- /dev/null
+++ b/examples/python/rc2.py
@@ -0,0 +1,84 @@
+# RC2 algorithm
+# basic version without optimizations
+# See also https://github.com/pysathq/pysat and papers in CP 2014, JSAT 2015.
+
+from z3 import *
+
+def tt(s, f):
+    return is_true(s.model().eval(f))
+
+
+def add(Ws, f, w):
+    Ws[f] = w + (Ws[f] if f in Ws else 0)
+
+def sub(Ws, f, w):
+    w1 = Ws[f]
+    if w1 > w:
+        Ws[f] = w1 - w
+    else:
+        del(Ws[f])
+
+class RC2:
+    def __init__(self, s):
+        self.bounds = {}
+        self.solver = s
+        self.solver.set("sat.cardinality.solver", True)
+        self.solver.set("sat.core.minimize", True)
+        self.solver.set("sat.core.minimize_partial", True)
+        
+    def at_most(self, S, k):
+        fml = AtMost(S + [k])
+        name = Bool("%s" % fml)
+        self.solver.add(Implies(name, fml))
+        self.bounds[name] = (S, k)
+        return name
+
+    # Ws are weighted soft constraints
+    # Whenever there is an unsatisfiable core over ws
+    # increase the limit of each soft constraint from a bound
+    # and create a soft constraint that limits the number of
+    # increased bounds to be at most one.
+    def maxsat(self, Ws):
+        cost = 0
+        Ws0 = Ws.copy()
+        while unsat == self.solver.check([f for f in Ws]):
+            core = list(self.solver.unsat_core())
+            print (self.solver.statistics())
+            print("Core", core)
+            if not core:
+                return unsat
+            w = min([Ws[c] for c in core])
+            cost += w
+            for f in core:
+                sub(Ws, f, w)
+            for f in core:
+                if f in self.bounds:
+                    S, k = self.bounds[f]
+                    if k + 1 < len(S):
+                        add(Ws, self.at_most(S, k + 1), w)                
+            add(Ws, self.at_most([mk_not(f) for f in core], 1), w)
+            
+        return cost, { f for f in Ws0 if tt(self.solver, f) }
+
+    def from_file(self, file):
+        opt = Optimize()
+        opt.from_file(file)
+        self.solver.add(opt.assertions())
+        obj = opt.objectives()[0]
+        Ws = {}        
+        for f in obj.children():
+            assert(f.arg(1).as_long() == 0)
+            add(Ws, f.arg(0), f.arg(2).as_long())
+        return self.maxsat(Ws)
+
+
+def main(file):
+    s = SolverFor("QF_FD")
+    rc2 = RC2(s)
+    set_param(verbose=0)
+    cost, trues = rc2.from_file(file)
+    print(cost)
+    print(s.statistics())
+
+# main(<myfile>)
+    
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 70dcb158e..ffd9c27a1 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -1645,6 +1645,12 @@ def Not(a, ctx=None):
         a = s.cast(a)
         return BoolRef(Z3_mk_not(ctx.ref(), a.as_ast()), ctx)
 
+def mk_not(a):
+    if is_not(a):
+        return a.arg(0)
+    else:
+        return Not(a)
+
 def _has_probe(args):
     """Return `True` if one of the elements of the given collection is a Z3 probe."""
     for arg in args:
@@ -2800,7 +2806,7 @@ class RatNumRef(ArithRef):
         return self.denominator().is_int() and self.denominator_as_long() == 1
 
     def as_long(self):
-        _z3_assert(self.is_int(), "Expected integer fraction")
+        _z3_assert(self.is_int_value(), "Expected integer fraction")
         return self.numerator_as_long()
 
     def as_decimal(self, prec):