add pogo

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

programmingz3/code/interp.py

@@ -0,0 +1,26 @@
+from z3 import *
+
+def mk_lit(m, x):
+    if is_true(m.eval(x)):
+       return x
+    else:
+       return Not(x)
+
+def pogo(A, B, xs):   
+    while sat == A.check():
+       m = A.model()
+       L = [mk_lit(m, x) for x in xs]
+       if unsat == B.check(L):
+          notL = Not(And(B.unsat_core()))
+          yield notL
+          A.add(notL)
+       else:
+          print("expecting unsat")
+          break
+
+A = SolverFor("QF_FD")
+B = SolverFor("QF_FD")
+a1, a2, b1, b2, x1, x2 = Bools('a1 a2 b1 b2 x1 x2')
+A.add(a1 == x1, a2 == a1, a2 == x2)
+B.add(b1 == x1, b2 != b1, b2 == x2)
+print(list(pogo(A, B, [x1, x2])))

programmingz3/programmingz3.mdk

@@ -19,6 +19,9 @@ Package       : amssymb
 Package       : [curve]xypic
 Package       : tikz
 Package       : algorithm2e
+~Exercise     : @h1-exercise=lower-case @h1-exercise label="@h1@h1-exercise"
+                margin-left=0em
+                before="[**Exercise &label;: **]{margin-left=0em}&br;"
 
 ~ MathDefs
 \newcommand{\Mbp}{Mbp}
@@ -38,6 +41,8 @@ Package       : algorithm2e
 
 ~
 
+
+
 [TITLE]
 
 
@@ -1144,7 +1149,13 @@ def cube_and_conquer(s):
 When the underlying solver is based on the SAT Core, see Section [#sec-sat-core], it uses
 a lookahead solver to select cubes [@HeuleKWB11]. By default, the cuber produces two branches,
 corresponding to a case split on a single literal. The SAT Core based cuber can be configured
-to produce cubes that represent several branches. Each branch is represented as a conjunction
+to produce cubes that represent several branches. An empty cube indicates a failure, such
+as, the solver does not support cubing (only the SMT and SAT cores support cubing, and generic
+solvers based on tactics do not), or a timeout or resource bound was encountered during cubing.
+A cube comprising of the Boolean constant `true` indicates that the state of the solver is
+satisfiable. Finally, it is possible for the `s.cube()` method to return an empty set of cubes.
+This happens when the state of `s` is unsatisfiable.
+Each branch is represented as a conjunction
 of literals. The cut-off for branches is configured using
 
 * `sat.lookahead.cube.cutoff`{language:python} 
@@ -1187,12 +1198,13 @@ def block_model(s):
     s.add(Or([ f() != m[f] for f in m.decls() if f.arity() == 0]))           
 ```
 
-## Maximizing Satisfying Assignments [@MenciaPM15]
+## Maximizing Satisfying Assignments
 Another use of models is to use them as a guide to a notion of optimal model.
 A _maximal satisfying solution_, in short _mss_, for a set of formulas `ps`
 is a subset of `ps` that is consistent with respect to the solver state `s`
 and cannot be extended to a bigger subset of `ps` without becoming inconsistent
-relative to `s`. We provide a procedure for finding a maximal satisfying subset below.
+relative to `s`. We provide a procedure, from [@MenciaPM15], 
+for finding a maximal satisfying subset below.
 It extends a set `mss` greedily by adding as many satisfied predicates from `ps` 
 in each round as possible. If it finds some predicate `p` that it cannot add, it notes that it
 is a backbone with respect to the current `mss`. As a friendly hint, 
@@ -1226,15 +1238,14 @@ def get_mss(s, mss, ps):
 
 
 ~ Exercise
-__Exercise__:
 Suppose `ps` is a list corresponding to digits in a binary number
 and `ps` is ordered by most significant digit down. The goal is to
 find an mss with the largest value as a binary number. Modify `get_mss` 
 to produce such a number.
 ~
 
-## All Cores and Correction Sets [@liffiton2016fast]
-The Marco procedure combines models and cores in a process
+## All Cores and Correction Sets 
+The Marco procedure [@liffiton2016fast] combines models and cores in a process
 that enumerates all unsatisfiable cores and all maximal
 satisfying subsets of a set of formulas `ps` with
 respect to solver `s`. It maintains a `map` solver
@@ -1267,8 +1278,8 @@ Efficiently enumerating cores and correction sets is an active area of research.
 Many significant improvements have been developed over the above basic 
 implementation [@BacchusK15;@MenciaPM15;@BacchusK16;@PrevitiMJM17;@Alviano17;@NarodytskaBMS18].
 
-## Bounded Model Checking [@Biere09]
-Figure [#fig-bmc] illustrates a bounded model checker
+## Bounded Model Checking 
+Figure [#fig-bmc] illustrates a bounded model checking procedure [@Biere09]
  that takes a transition system as input and checks if a goal is reachable.
 Transition systems are described as
 
@@ -1332,7 +1343,59 @@ You can find a simplistic implementation of IC3 using the Python API online
 <https://github.com/Z3Prover/z3/blob/master/examples/python/mini_ic3.py>
 ~
 
-## Monadic Decomposition [@VeanesBNB17]
+## Propositional Interpolation
+
+It is possible to compute interpolants using models and cores [@ChocklerIM12].
+A procedure that computes an interpolant $I$ for formulas $A$, $B$, where
+$A \land B$ is unsatisfiable proceeds by initializing $I = \true$ and 
+saturating $\lceil A, B, \true \rceil$ with respect to the rules:
+
+
+~ MathPre
+ \lceil A, B, I \rceil & \Longrightarrow & \lceil A, B, I \land \neg L\rceil & \mbox{if} & B \vdash \neg L, A \land I\not\vdash \neg L \\
+                       &                 & I & \mbox{if} & A \vdash \neg I %\\
+~
+
+The partial interpolant $I$ produced by pogo satisfies $B \vdash I$. It terminates when $A \vdash \neg I$.
+The condition $A \land I \not\vdash \neg L$ ensures that the algorithm makes progress and suggests using an implicant $L' \supseteq L$ of $A \land I$ in each iteration.
+
+~ Figure { #fig-interpolate; caption : "Propositional interpolation" }
+```python
+def mk_lit(m, x):
+    if is_true(m.eval(x)):
+       return x
+    else:
+       return Not(x)
+
+def pogo(A, B, xs):   
+    while sat == A.check():
+       m = A.model()
+       L = [mk_lit(m, x) for x in xs]
+       if unsat == B.check(L):
+          notL = Not(And(B.unsat_core()))
+          yield notL
+          A.add(notL)
+       else:
+          print("expecting unsat")
+          break
+```
+~
+
+~ Example
+The (reverse) interpolant between $A: x_1 = a_1 = a_2 = a_2$ and $B: x_1 = b_1 \neq b_2 = x_2$
+using vocabulary $x_1, x_2$ is $x_1 \neq x_2$. It is implied by $B$ and inconsistent with $A$.
+```python
+A = SolverFor("QF_FD")
+B = SolverFor("QF_FD")
+a1, a2, b1, b2, x1, x2 = Bools('a1 a2 b1 b2 x1 x2')
+A.add(a1 == x1, a2 == a1, a2 == x2)
+B.add(b1 == x1, b2 != b1, b2 == x2)
+print(list(pogo(A, B, [x1, x2])))
+```
+
+~
+
+## Monadic Decomposition 
 
 Suppose we are given a formula $\varphi[x,y]$ using variables $x$ and $y$.
 When is it possible to rewrite it as a Boolean combination of formulas
@@ -2038,11 +2101,14 @@ SPACER Horn clause solver by Arie Gurfinkel to solve Horn clauses over arithmeti
 A Constrained Horn Clause is a disjunction of literals over a set of uninterpreted 
 predicates and interpreted functions and interpreted predicates (such as arithmetical 
 operations `+` and relations `<=`). The uninterpreted predicates, 
-may occur negatively without restrictions, but only occur positively in at most one literal.
+may occur negatively without restrictions, but only occur positively in at most one place.
 
 The solver also contains a Datalog engine that can be used to solve Datalog queries
 (with stratified negation) over finite domains and "header spaces" that are large finite
-domains, but can be encoded succinctly using ternary bit-vectors. Additional
+domains, but can be encoded succinctly using ternary bit-vectors. The `Fixedpoint`{language:python}
+context contains facilities for building Horn clauses, and generally a set of stratified Datalog rules, 
+and for querying the resulting set of rules and facts.
+Additional
 information on the Fixedpoint engine can be found on <https://rise4fun.com/z3/tutorial/fixedpoints>.
 
 We provide a very simple illustration of Horn clause usage here. McCarthy's 91 function illustrates

programmingz3/refs.bib

@@ -1,3 +1,4 @@
+
 @article{VeanesBNB17,
   author    = {Margus Veanes and
                Nikolaj Bj{\o}rner and
@@ -510,18 +511,6 @@ @inproceedings{DBLP:conf/hvc/MorgadoLM12
   pages     = {86--101},
   year      = {2012},
 }
-@proceedings{DBLP:conf/hvc/2012,
-  editor    = {Armin Biere and
-               Amir Nahir and
-               Tanja E. J. Vos},
-  title     = {Hardware and Software: Verification and Testing - 8th International
-               Haifa Verification Conference, {HVC} 2012, Haifa, Israel, November
-               6-8, 2012. Revised Selected Papers},
-
-  volume    = {7857},
-  publisher = {Springer},
-  year      = {2013},
-}
 
 @inproceedings{IhlemannJS08,
   author    = {Carsten Ihlemann and
@@ -1355,23 +1344,6 @@ @inproceedings{BjornerGKL13
   bibsource = {dblp computer science bibliography, http://dblp.org}
 }
 
-@inproceedings{ChocklerIM12,
-  author    = {Hana Chockler and
-               Alexander Ivrii and
-               Arie Matsliah},
-  title     = {Computing Interpolants without Proofs},
-  booktitle = {Hardware and Software: Verification and Testing - 8th International
-               Haifa Verification Conference, {HVC} 2012, Haifa, Israel, November
-               6-8, 2012. Revised Selected Papers},
-  pages     = {72--85},
-  year      = {2012},
-  crossref  = {DBLP:conf/hvc/2012},
-  url       = {http://dx.doi.org/10.1007/978-3-642-39611-3_12},
-  doi       = {10.1007/978-3-642-39611-3_12},
-  timestamp = {Tue, 09 Jul 2013 14:14:21 +0200},
-  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/hvc/ChocklerIM12},
-  bibsource = {dblp computer science bibliography, http://dblp.org}
-}
 
 @inproceedings{PhanBM12,
   author    = {Anh-Dung Phan and
@@ -2293,6 +2265,19 @@ @inproceedings{ChocklerIM12
   bibsource = {dblp computer science bibliography, http://dblp.org}
 }
 
+@proceedings{DBLP:conf/hvc/2012,
+  editor    = {Armin Biere and
+               Amir Nahir and
+               Tanja E. J. Vos},
+  title     = {Hardware and Software: Verification and Testing - 8th International
+               Haifa Verification Conference, {HVC} 2012, Haifa, Israel, November
+               6-8, 2012. Revised Selected Papers},
+  volume    = {7857},
+  publisher = {Springer},
+  year      = {2013},
+}
+
+
 @article{LopesMNR18,
   author    = {Nuno P. Lopes and
                David Menendez and