dual solver, exericse solution

Signed-off-by: Nikolaj Bjorner <[email protected]>

programmingz3/code/cdclTdual.py

@@ -0,0 +1,52 @@
+def simple_cdclT(clauses):
+    prop   = Solver()
+    dual   = Solver()
+    theory = Solver()
+    abs = {}
+    fml = abstract_clauses(abs, clauses)
+    prop.add(fml)
+    dual.add(Not(fml))
+    theory.add([p == abs[p] for p in abs])
+    while True:
+        is_sat = prop.check()
+        if sat == is_sat:
+            m = prop.model()            
+            lits = [mk_lit(m, abs[p]) for p in abs]
+            is_sat = dual.check(lits)
+            assert(is_sat == unsat)
+            lits = dual.unsat_core()
+            if unsat == theory.check(lits):
+                prop.add(Not(And(theory.unsat_core())))
+            else:
+                print(theory.model())
+                return
+        else:
+            print(is_sat)
+            return
+
+index = 0
+def abstract_atom(abs, atom):
+    global index
+    if atom in abs:
+        return abs[atom]
+    p = Bool("p%d" % index)
+    index += 1
+    abs[atom] = p
+    return p
+
+def abstract_lit(abs, lit):
+    if is_not(lit):
+        return Not(abstract_atom(abs, lit.arg(0)))
+    return abstract_atom(abs, lit)
+
+def abstract_clause(abs, clause):
+    return Or([abstract_lit(abs, lit) for lit in clause])
+
+def abstract_clauses(abs, clauses):
+    return [abstract_clause(abs, clause) for clause in clauses]
+
+def mk_lit(m, p):
+    if is_true(m.eval(p)):
+        return p
+    else:
+        return Not(p)