(declare-sortT)
(declare-fun subtype (TT) Bool)
;; subtype is reflexive
(assert (forall ((x T)) (subtype x x)))
;; subtype is antisymmetric
(assert (forall ((x T) (y T)) (=> (and (subtype x y) (subtype y x)) (= x y))))
;; subtype is transitive; ...;; subtype has the tree-property
(assert (forall ((x T) (y T) (z T))
(=> (and (subtype x z) (subtype y z)) (or (subtype x y) (subtype y x)))))
;; we have an additional axiom: every type is a subtype of obj-type
(declare-const obj-type T) ....
(assert (forall ((x T)) (subtype x obj-type)))
(assert (subtype int-type real-type))
(assert (subtype real-type complex-type))
(assert (not (subtype string-type real-type)))
EPR Example - online
EPR decidability
Skolemize
, the are free constants
Instantiate
where ranges over all bindings of to .
Check ground SAT
Ground SAT implies finite model of size at most .
EPR using MBQI
Skolemize
, the are free constants
Models for bind variables to free constants
The number of possible such models is bounded by .
Synthesize generalized instantiation sets using grammar rules.
Applies to winder range of formulas than the syntactic array property fragment.
list property fragment by McPeak and Necula
several locally finite theories - Stokkermans et. al.
Essentially Uninterpreted Example
(set-option:smt.mbqi true)
;; f an g are "streams"
(declare-fun f (Int) Int)
(declare-fun g (Int) Int)
;; the segment [a, n + a] of stream f is equal to the segment [0, n] of stream g.
(declare-const n Int)
(declare-const a Int)
(assert (forall ((x Int)) (=> (and (<= 0 x) (<= x n))
(= (f (+ x a)) (g x)))))
;; adding some constraints to a
(assert (> a 10))
(assert (>= (f a) 2))
(assert (<= (g 3) (- 10)))
(check-sat)
(get-model)
fixes value of , but can change again it at round ,
can guess values of of to satisfy .
Some player loses at round .
Create succinct no-good to strengthen resp. .
Backjump to round (or below).
Main ingredients: Projection and Strategies
Projections are added to learn from mistakes.
Player avoids repeating same losing moves.
Strategies prune moves from opponent.
Prevent opponent player from moves.
Finding small good no-goods
Player has lost at round
Player found a model at round , .
induces an evaluation on a subset of literals in , such that
.
is an unsatisfiable core for .
Model Based Projection
Find a , such that .
should be weak, so is a strong blocker.
should be cheap to find and avoid space overhead.
Then can block .
Idea: Use to find a sufficient .
Initialization
def level(j,a):return max level of bound variable in atom a of parity j
QSAT Algorithm
def strategy(M,j):returndef tailv(j):return
j =1M= null
whileTrue:if strategy(M, j) is unsat:if j == 1:returnFis unsat
if j == 2:returnFis sat
C=Core(, strategy(M, j))
J=Mbp(tailv(j), C)
j = index of max variable inJ of same parity as j
=JM= null
else:M= current model
j = j + 1
Projection and Strategies
Projections learn from mistakes, avoids similar mistakes in future rounds.
Strategies prune moves from opponent.
Model-based projection - Example
Want to compute small .
Note
Say
So
Model-based Projection for LRA
Eliminate from conjunction of literals :
Trick: Use to turn into .
Model-based Projection for LRA - resolution
Can now assume occurs only as upper or lower bounds:
Model-based Projection on formulas
def sign(M,a):ifM(a) return a elsereturn a
Model-based Projection for LIA
For LIA, cannot just assume equalities are of the form or .
Generally, has a coefficient, that we cannot remove.
Example: .
What could go wrong if we just reduce to ?
Suppose , . So .
Cross-multiplying gives , which is feasible, but is infeasible.
Model-based Projection for LIA - integer resolution
Claim: (Roughly) The same projection operator can be used in both cases if occurs in all literals and the operator is stable under changes to the value of .
Finding strategies
Other main ingredient of QSAT is option for players to narrow options of opponents by revealing a strategy
at round :
value of is already fixed,
fixes value of ,
can make a function of .
Developing practical strategies is work in progress
[1]Nikolaj Bjørner. “Linear Quantifier-Elimination as an Abstract Decision Procedure.” In IJCAR. 2010. 🔎
[2]Nikolaj Bjørner, and Mikolás Janota. “Playing with Alternating Quantifier Satisfaction.” In LPAR Short Presentation Papers. 2015. 🔎
[3]Nikolaj Bjørner, Mikolás Janota, and William Klieber. “On Conflicts and Strategies in QBF.” In 20th International Conferences on Logic for Programming, Artificial
Intelligence and Reasoning - Short Presentations, LPAR 2015, Suva,
Fiji, November 24-28, 2015., 28â€“41. 2015. http://www.easychair.org/publications/paper/On_Conflicts_and_Strategies_in_QBF. 🔎
[4]Nikolaj Bjørner, Kenneth L. McMillan, and Andrey Rybalchenko. “On Solving Universally Quantified Horn Clauses.” In SAS, 105â€“125. 2013. 🔎
[5]Maria Paola Bonacina, Christopher Lynch, and Leonardo Mendonça de Moura. “On Deciding Satisfiability by Theorem Proving with Speculative
Inferences.” J. Autom. Reasoning 47 (2): 161â€“189. 2011. 🔎
[6]Aaron R. Bradley. “SAT-Based Model Checking without Unrolling.” In VMCAI, 70â€“87. 2011. 🔎
[7]Aaron R. Bradley, Zohar Manna, and Henny B. Sipma. “Whatâ€™s Decidable About Arrays?” In Verification, Model Checking, and Abstract Interpretation, 7th International
Conference, VMCAI 2006, Charleston, SC, USA, January 8-10, 2006,
Proceedings, 427â€“442. 2006. doi:10.1007/11609773_28. 🔎
[8]Alessandro Cimatti, and Alberto Griggio. “Software Model Checking via IC3.” In CAV, 277â€“293. 2012. 🔎
[9]Alessandro Cimatti, Alberto Griggio, Sergio Mover, and Stefano Tonetta. “IC3 Modulo Theories via Implicit Predicate Abstraction.” In TACAS, 46â€“61. 2014. 🔎
[10]Niklas Eén, Alan Mishchenko, and Robert K. Brayton. “Efficient Implementation of Property Directed Reachability.” In FMCAD, 125â€“134. 2011. 🔎
[11]Yeting Ge, and Leonardo Mendonça de Moura. “Complete Instantiation for Quantified Formulas in Satisfiabiliby
Modulo Theories.” In CAV, 306â€“320. 2009. 🔎
[12]Sergey Grebenshchikov, Nuno P. Lopes, Corneliu Popeea, and Andrey Rybalchenko. “Synthesizing Software Verifiers from Proof Rules.” In ACM SIGPLAN Conference on Programming Language Design and Implementation,
PLDI â€™12, Beijing, China - June 11 - 16, 2012, 405â€“416. 2012. doi:10.1145/2254064.2254112. 🔎
[13]Krystof Hoder, and Nikolaj Bjørner. “Generalized Property Directed Reachability.” In Theory and Applications of Satisfiability Testing - SAT 2012 - 15th
International Conference, Trento, Italy, June 17-20, 2012. Proceedings, 157â€“171. 2012. doi:10.1007/978-3-642-31612-8_13. 🔎
[14]Krystof Hoder, Nikolaj Bjørner, and Leonardo Mendonça de Moura. “μZ- An Efficient Engine for Fixed Points with Constraints.” In Computer Aided Verification - 23rd International Conference, CAV
2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, 457â€“462. 2011. doi:10.1007/978-3-642-22110-1_36. 🔎
[15]Shachar Itzhaky, Nikolaj Bjørner, Thomas W. Reps, Mooly Sagiv, and Aditya V. Thakur. “Property-Directed Shape Analysis.” In CAV, 35â€“51. 2014. 🔎
[16]Mikolás Janota, and Joao Marques-Silva. “Solving QBF by Clause Selection.” In Proceedings of the Twenty-Fourth International Joint Conference on
Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, July
25-31, 2015, 325â€“331. 2015. http://ijcai.org/Abstract/15/052. 🔎
[17]Ajith K. John, and Supratik Chakraborty. “A Quantifier Elimination Algorithm for Linear Modular Equations and
Disequations.” In Computer Aided Verification - 23rd International Conference, CAV
2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, 486â€“503. 2011. doi:10.1007/978-3-642-22110-1_39. 🔎
[18]Ajith K. John, and Supratik Chakraborty. “Extending Quantifier Elimination to Linear Inequalities on Bit-Vectors.” In Tools and Algorithms for the Construction and Analysis of Systems
- 19th International Conference, TACAS 2013, Held as Part of the
European Joint Conferences on Theory and Practice of Software, ETAPS
2013, Rome, Italy, March 16-24, 2013. Proceedings, 78â€“92. 2013. doi:10.1007/978-3-642-36742-7_6. 🔎
[19]Ajith K. John, and Supratik Chakraborty. “A Layered Algorithm for Quantifier Elimination from Linear Modular
Constraints.” Formal Methods in System Design 49 (3): 272â€“323. 2016. doi:10.1007/s10703-016-0260-9. 🔎
[20]Dejan Jovanovic, and Leonardo Mendonça de Moura. “Solving Non-Linear Arithmetic.” In Automated Reasoning - 6th International Joint Conference, IJCAR
2012, Manchester, UK, June 26-29, 2012. Proceedings, 339â€“354. 2012. doi:10.1007/978-3-642-31365-3_27. 🔎
[21]Roland Kindermann, Tommi A. Junttila, and Ilkka Niemelä “SMT-Based Induction Methods for Timed Systems.” In FORMATS, 171â€“187. 2012. 🔎
[22]Anvesh Komuravelli, Arie Gurfinkel, and Sagar Chaki. “SMT-Based Model Checking for Recursive Programs.” In CAV, 17â€“34. 2014. 🔎
[23]Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki, and Edmund M. Clarke. “Automatic Abstraction in SMT-Based Unbounded Software Model
Checking.” In CAV, 846â€“862. 2013. 🔎
[24]Kenneth L. McMillan. “Lazy Annotation Revisited.” In Computer Aided Verification - 26th International Conference, CAV
2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna,
Austria, July 18-22, 2014. Proceedings, 243â€“259. 2014. doi:10.1007/978-3-319-08867-9_16. 🔎
[25]David Monniaux. “A Quantifier Elimination Algorithm for Linear Real Arithmetic.” In LPAR (Logic for Programming Artificial Intelligence and Reasoning), 243â€“257. Lecture Notes in Computer ScienceÂ 5330. Springer Verlag. 2008. doi:10.1007/978-3-540-89439-1_18. 🔎
[26]David Monniaux. “Quantifier Elimination by Lazy Model Enumeration.” In Computer-Aided Verification (CAV), 585â€“599. Lecture Notes in Computer ScienceÂ 6174. Springer Verlag. 2010. doi:10.1007/978-3-642-14295-6_51. 🔎
[27]Leonardo Mendonça de Moura, and Nikolaj Bjørner. “Efficient E-Matching for SMT Solvers.” In CADE, 183â€“198. 2007. 🔎
[28]Leonardo Mendonça de Moura, and Nikolaj Bjørner. “Engineering DPLL(T) + Saturation.” In IJCAR, 475â€“490. 2008. 🔎
[29]Leonardo Mendonça de Moura, and Nikolaj Bjørner. “Bugs, Moles and Skeletons: Symbolic Reasoning for Software
Development.” In IJCAR, 400â€“411. 2010. 🔎
[30]Leonardo Mendonça de Moura, and Dejan Jovanovic. “A Model-Constructing Satisfiability Calculus.” In Verification, Model Checking, and Abstract Interpretation, 14th International
Conference, VMCAI 2013, Rome, Italy, January 20-22, 2013. Proceedings, 1â€“12. 2013. doi:10.1007/978-3-642-35873-9_1. 🔎
[31]Anh-Dung Phan, Nikolaj Bjørner, and David Monniaux. “Anatomy of Alternating Quantifier Satisfiability (Work in
Progress).” In SMT-IJCAR, 120â€“130. 2012. 🔎
[32]Ruzica Piskac, Leonardo Mendonça de Moura, and Nikolaj Bjørner. “Deciding Effectively Propositional Logic Using DPLL and
Substitution Sets.” J. Autom. Reasoning 44 (4): 401â€“424. 2010. 🔎
[33]William Pugh. “The Omega Test: A Fast and Practical Integer Programming Algorithm
for Dependence Analysis.” In Proceedings Supercomputing â€™91, Albuquerque, NM, USA, November 18-22,
1991, 4â€“13. 1991. doi:10.1145/125826.125848. 🔎
[34]Andrew Reynolds, Tim King, and Viktor Kuncak. “Solving Quantified Linear Arithmetic by Counterexample-Guided Instantiation.” Formal Methods in System Design 51 (3): 500â€“532. 2017. doi:10.1007/s10703-017-0290-y. 🔎
[35]Martina Seidl, Florian Lonsing, and Armin Biere. “qbf2epr: A Tool for Generating EPR Formulas from QBF.” In Third Workshop on Practical Aspects of Automated Reasoning, PAAR-2012,
Manchester, UK, June 30 - July 1, 2012, 139â€“148. 2012. http://www.easychair.org/publications/paper/145184. 🔎
[36]Christoph M. Wintersteiger, Youssef Hamadi, and Leonardo Mendonça de Moura. “Efficiently Solving Quantified Bit-Vector Formulas.” Formal Methods in System Design 42 (1): 3â€“23. 2013. 🔎