ScalaZ3 Integrating SMT and Programming - LARA: Wiki

ScalaZ3 Integrating SMT and Programming - LARA: Wiki

Scala Z3 Integrating SMT and Programming Ali Sinan Kksal, Viktor Kuncak, Philippe Suter cole Polytechnique Fdrale de Lausanne Efficient SMT solver from Microsoft Research Supports many theories through DPLL(T) and NelsonOppen combination SMT-LIB standard input format, as well as C, .NET, OCaml, and Python bindings Scalable programming language

Blending of functional and object-oriented programming Runs on the Java Virtual Machine (and .NET) Rich type system (generics, type classes, implicit conversions, etc.) Now used by over 100000 developers (incl. Twitter, UBS, LinkedIn) ~$ ./demo C and Scala side-by-side #include "z3.h" Z3_config cfg = Z3_mk_config(); Z3_set_param_value(cfg, "MODEL", "true"); Z3_context z3 = Z3_mk_context(cfg); import z3.scala._

val cfg = new Z3Config cfg.setParamValue("MODEL", "true") val z3 = new Z3Context(cfg) Z3_sort intSort = Z3_mk_int_sort(z3); val intSort : Z3Sort = z3.mkIntSort Z3_func_decl f = Z3_mk_func_decl(z3, Z3_mk_string_symbol(z3,"f"), 1, &intSort, intSort); Z3_ast x = Z3_mk_const(z3, Z3_mk_string_symbol(z3,"x"), intSort); Z3_ast y = Z3_mk_const(z3, Z3_mk_string_symbol(z3,"y"), intSort); val f : Z3FuncDecl = z3.mkFuncDecl( z3.mkStringSymbol("f"),

List(intSort), intSort) val x : Z3AST = z3.mkConst( z3.mkStringSymbol("x"), intSort) val y : Z3AST = z3.mkConst( z3.mkStringSymbol("y"), intSort) Z3_ast ineq = Z3_mk_not(z3, Z3_mk_eq(z3, x, Z3_mk_app(z3, f, 1, &y))); val ineq : Z3AST = z3.mkNot( z3.mkEq(x, z3.mkApp(f, y))) Z3_assert_cnstr(z3, ineq); z3.assertCnstr(ineq)

Z3_model m; if(Z3_check_and_get_model(z3, &m)) { printf("%s", Z3_model_to_string(z3, m)); } z3.checkAndGetModel match { case (Some(true), m) println(m) case _ ; } def choose[A,B](p: (Val[A],Val[B])Tree[BoolSort]) : (A,B) def find[A,B](p: (Val[A],Val[B])Tree[BoolSort]) : Option[(A,B)] def findAll[A,B](p: (Val[A],Val[B])Tree[BoolSort]) : Iterator[(A,B)] Anatomy of an Inline Invocation import z3.scala._ import dsl._ ...

choose((y: Val[IntInt], x: Val[Int], y: Val[Int]) !(x === f(y))) imports and Val[_]s only manifestations of the library Desired return types (actual Scala types). Domain specific language of formulas resembles Scala expressions. Returned values are Scala values (including functions). for Comprehensions Can you find positive x, y, z such that 2x + 3y 40, xz = 3y2, and y is prime?

for((x,y) findAll((x: Val[Int], y: Val[Int]) x > 0 && y > x && x * 2 + y * 3 <= 40); if(isPrime(y)); z findAll((z: Val[Int]) z * x === 3 * y * y)) yield (x, y, z) Returned expression. Filter: arbitrary boolean expression. Generators: sequences, computed eagerly or lazily. (1,2,12), (1,3,27), (1,5,75), (1,7,147), (1,11,363), (3,11,121), (3,5,25), (3,7,49) Implementation Aspects Top

Basic representation: class Z3AST(ptr : Long) Tree hierarchy as part of the DSL: IntSort BoolSort SetSort Bottom abstract class Tree[+T >: Bottom <: Top] { ...

def <(other : Tree[_ <: IntSort]) : Tree[BoolSort] = ... ... } implicit def ast2Tree(ast : Z3AST) : Tree[Bottom] implicit def tree2AST(tree : Tree[_]) : Z3AST Automatic conversions between the two kinds. Soft typing for the DSL Trees. DSL in Action import z3.scala._ val cfg = new Z3Config cfg.setParamValue("MODEL", "true") val z3 = new Z3Context(cfg) import z3.scala._

val z3 = new Z3Context("MODEL -> true) val intSort : Z3Sort = z3.mkIntSort val intSort = z3.mkIntSort val f : Z3FuncDecl = z3.mkFuncDecl( z3.mkStringSymbol("f"), List(intSort), intSort) val x : Z3AST = z3.mkConst( z3.mkStringSymbol("x"), intSort) val y : Z3AST = z3.mkConst( z3.mkStringSymbol("y"), intSort) val f = z3.mkFuncDecl( "f", intSort, intSort) val ineq : Z3AST = z3.mkNot(

z3.mkEq(x, z3.mkApp(f, y))) val ineq : Z3AST = !(x === f(y)) val x = z3.mkConst("x", intSort) val y = z3.mkConst("y", intSort) Z3 Sorts Scala Types Array[A,B] Int Int Boolean

BV[32] Bool AB Different function calls to create constants and to retrieve the models: ctx.getBool(m.eval(tree)) ctx.getNumeralInt(m.eval(tree)) m.getArrayValue(tree)... Set[A] Users should be able to ignore the underlying representation:

m.evalAs[Boolean](tree) m.evalAs[Int](tree) m.evalAs[IntInt](tree) def evalAs[T](tree : Z3AST) : T def evalAs[T : Evaluator](tree : Z3AST) : T def evalAs[T](tree : Z3AST)(implicit e : Evaluator[T]) : T @implicitNotFound(No known model evaluator for type ${T}.) trait Evaluator[T] { def eval(model : Z3Model, tree : Z3AST) : T } implicit object IntEvaluator extends Evaluator[Int] { def eval(model : Z3Model, tree : Z3AST) : Int = ... } implicit def lift2Set[T : Evaluator] = new Evaluator[Set[T]] { def eval(model : Z3Model, tree : Z3AST) : Set[T] = ... }

m.evalAs[Int](t) m.evalAs[Int](t)(IntEvaluator) m.evalAs[Set[Set[Int]]](t) m.evalAs[...](t)(lift2Set(lift2Set(IntEvaluator))) Procedural Attachments val z3 = new Z3Context(MODEL -> true) val stringTheory = new ProceduralAttachment[String](z3) { val concat = function((s1,s2) s1 + s2) val substr = predicate((s1,s2) s2.contains(s1)) val evenLength = predicate(_.length % 2 == 0) } import stringTheory._ val s = z3.mkConst(s, stringTheory.sort) z3.assertCnstr(s === world || s === moon) z3.assertCnstr(evenLength(s))

z3.check > Some(true) z3.assertCnstr(substr(concat(hello, s), low)) z3.check > Some(false) Applications MUNCH: Decision procedure for multisets and sets R. Piskac, V. Kuncak, IJCAR 2010 Z3 extension for sets with cardinality constraints P. Suter, R. Steiger, V. Kuncak, VMCAI 2011 Leon: Verifier for functional programs P. Suter, A.S. Kksal, V. Kuncak, SAS 2011, http://lara.epfl.ch/leon/ Kaplan: Constraint programming in Scala Ali Sinan Kksals Master Thesis

Other users at ETH Zrich, KU Leuven Availability http://lara.epfl.ch/w/ScalaZ3 https://github.com/psuter/ScalaZ3 (Tested on Windows and Linux, on 32 and 64 bit architectures.) Thank you.

Recently Viewed Presentations

  • Fire Blocking For All Buildings, Including Houses

    Fire Blocking For All Buildings, Including Houses

    Fire Blocking Requirements For All Buildings; BC Building Code . Fire Block Requirements . Including Houses. Fire blocking has been specified within the National Building Code for over 47 years or longer, under the former name of "fire stopping".
  • Using Data to Advance Health Equity - Lessons from Community ...

    Using Data to Advance Health Equity - Lessons from Community ...

    Health equity indicators in this webinar also include health status indicators and stratifiers, which are sets of quantitative data that provide information on the health status of individuals, groups or populations. An indicator is "a thing that indicates the state...
  • An Introduction to Communicate in Print

    An Introduction to Communicate in Print

    Colourful semantics! These can be adapted to any structure/topic or theme and extended/reduced to meet the needs of the child. * Don't differentiate by the amount of support given. If a child 'always' has support then they are learning to...
  • Social Bond Theory Self-Control Theory - Numbers 1-30

    Social Bond Theory Self-Control Theory - Numbers 1-30

    Social Bond Theory Developed by Travis Hirschi The Theory: Assumes that all people have the capacity to be delinquent Preventing most people from engaging in delinquency is a "bonding" to conventional society Hirschi identifies 4 elements to the social bond...
  • Chapter 7 Section 3 Confucianism and Government

    Chapter 7 Section 3 Confucianism and Government

    During the Period of Disunion, which followed the Han dynasty, Confucianism was overshadowed by Buddhism as the major tradition in China. As you recall, many Chinese people turned to Buddhism for comfort during these troubled times. In doing so, they...
  • Evolution

    Evolution

    The group of flightless birds, known as ratites, occur in Australia (emu), New Zealand (kiwi), South America (rhea), Pupua New Guinea (cassowary) and Africa (ostrich). ... Convergent Evolution When two or more unrelated species adopt similar adaptations in response to...
  • CSC 341 Human-Computer Interaction

    CSC 341 Human-Computer Interaction

    Why usability? "A central concern of interaction design is to develop interactive products that are usable." "By . this is generally . meant: easy. to . learn, effective. to use, and . providing an enjoyable . user experience." A ....
  • A dairy calf DNA biobank for the discovery

    A dairy calf DNA biobank for the discovery

    John B. Cole. Animal Genomics & Improvement Laboratory, Agricultural Research Service, USDA, Beltsville, MD 20705-2350. INTRODUCTION. A number of recessive mutations that adversely affect dairy cow fertility have been identified using high-density SNP genotypes (VanRaden et al., 2011; Cole et...