liquid-fixpoint-0.2.2.0: external/fixpoint/smtLIB2.ml
(*
* Copyright © 2008 The Regents of the University of California. All rights reserved.
*
* Permission is hereby granted, without written agreement and without
* license or royalty fees, to use, copy, modify, and distribute this
* software and its documentation for any purpose, provided that the
* above copyright notice and the following two paragraphs appear in
* all copies of this software.
*
* IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY
* FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES
* ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN
* IF THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY
* OF SUCH DAMAGE.
*
* THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
* INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY
* AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS
* ON AN "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION
* TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.
*)
(********************************************************************************)
(*********** This module implements the binary interface with SMTLIB2 *********)
(*********** http://www.smt-lib.org/ *********)
(*********** http://www.grammatech.com/resource/smt/SMTLIBTutorial.pdf *********)
(********************************************************************************)
module H = Hashtbl
module F = Format
module Co = Constants
module BS = BNstats
module A = Ast
module Sy = A.Symbol
module So = A.Sort
module SM = Sy.SMap
module P = A.Predicate
module E = A.Expression
module Misc = FixMisc open Misc.Ops
module SSM = Misc.StringMap
module Th = Theories
module SMTLib2 : ProverArch.SMTSOLVER = struct
let spr = Printf.sprintf
let mydebug = false
let nb_unsat = ref 0
let nb_pop = ref 0
let nb_push = ref 0
(***************************************************************)
(********************** Types **********************************)
(***************************************************************)
type symbol = string (* Sy.t *)
type sort = string (* So.t *)
type ast = string (* E of A.expr | P of A.pred *)
type fun_decl = symbol
type cmd = Push
| Pop
| CheckSat
| Declare of symbol * sort list * sort
| AssertCnstr of ast
| Distinct of ast list (* {v: ast list | (len v) >= 2} *)
type resp = Ok
| Sat
| Unsat
| Unknown
| Error of string
type solver = Z3 | Mathsat | Cvc4
type context = { cin : in_channel
; cout : out_channel
; clog : out_channel }
let respString = function
| Ok -> "Ok"
| Sat -> "Sat"
| Unsat -> "Unsat"
| Unknown -> "Unknown"
| Error s -> "Error " ^ s
let solverString = function
| Z3 -> "z3"
| Mathsat -> "mathsat"
| Cvc4 -> "cvc4"
(*******************************************************************)
(*********************** Set Theory ********************************)
(*******************************************************************)
let elt = "SMT_Elt"
let set = "SMT_Set"
let emp = "smt_set_emp"
let add = "smt_set_add"
let cup = "smt_set_cup"
let cap = "smt_set_cap"
let mem = "smt_set_mem"
let dif = "smt_set_dif"
let sub = "smt_set_sub"
let com = "smt_set_com"
let map = "SMT_Map"
let sel = "smt_map_sel"
let sto = "smt_map_sto"
(*
(define-fun smt_set_emp () Set ((as const Set) false))
(define-fun smt_set_mem ((x Elt) (s Set)) Bool (select s x))
(define-fun smt_set_add ((s Set) (x Elt)) Set (store s x true))
(define-fun smt_set_cap ((s1 Set) (s2 Set)) Set ((_ map and) s1 s2))
(define-fun smt_set_cup ((s1 Set) (s2 Set)) Set ((_ map or) s1 s2))
(define-fun smt_set_com ((s Set)) Set ((_ map not) s))
(define-fun smt_set_dif ((s1 Set) (s2 Set)) Set (smt_set_cap s1 (smt_set_com s2)))
(define-fun smt_set_sub ((s1 Set) (s2 Set)) Bool (= smt_set_emp (smt_set_dif s1 s2)))
*)
let (++) = List.append
(* array preamble *)
let array_preamble _ =
if not !Co.map_theory then [] else
[ spr "(define-sort %s () (Array %s %s))"
map elt elt
; spr "(define-fun %s ((m %s) (k %s)) %s (select m k))"
sel map elt elt
; spr "(define-fun %s ((m %s) (k %s) (v %s)) %s (store m k v))"
sto map elt elt map
]
(* z3 specific *)
let z3_preamble _
= [ "(set-option :auto-config false)"
; "(set-option :model true)"
; "(set-option :model.partial false)"
; "(set-option :smt.mbqi false)"
] ++ if not !Co.set_theory then [] else
[ spr "(define-sort %s () Int)"
elt
; spr "(define-sort %s () (Array %s Bool))"
set elt
; spr "(define-fun %s () %s ((as const %s) false))"
emp set set
; spr "(define-fun %s ((x %s) (s %s)) Bool (select s x))"
mem elt set
; spr "(define-fun %s ((s %s) (x %s)) %s (store s x true))"
add set elt set
; spr "(define-fun %s ((s1 %s) (s2 %s)) %s ((_ map or) s1 s2))"
cup set set set
; spr "(define-fun %s ((s1 %s) (s2 %s)) %s ((_ map and) s1 s2))"
cap set set set
; spr "(define-fun %s ((s %s)) %s ((_ map not) s))"
com set set
; spr "(define-fun %s ((s1 %s) (s2 %s)) %s (%s s1 (%s s2)))"
dif set set set cap com
; spr "(define-fun %s ((s1 %s) (s2 %s)) Bool (= %s (%s s1 s2)))"
sub set set emp dif
] ++ array_preamble ()
(* cvc4 specific *)
let cvc4_preamble _
= if not !Co.set_theory then [] else
[ spr "(set-logic QF_AUFNIRAFS)"
; spr "(define-sort %s () Int)"
elt
; spr "(define-sort %s () (Set %s))"
set elt
; spr "(define-fun %s () %s (as emptyset (Set %s)))"
emp set elt
; spr "(define-fun %s ((x %s) (s %s)) Bool (member x s))"
mem elt set
; spr "(define-fun %s ((s %s) (x %s)) %s (insert x s))"
add set elt set
; spr "(define-fun %s ((s1 %s) (s2 %s)) %s (union s1 s2))"
cup set set set
; spr "(define-fun %s ((s1 %s) (s2 %s)) %s (intersection s1 s2))"
cap set set set
; spr "(declare-fun %s (%s) %s)"
com set set
; spr "(define-fun %s ((s1 %s) (s2 %s)) %s (setminus s1 s2))"
dif set set set
; spr "(define-fun %s ((s1 %s) (s2 %s)) Bool (subset s1 s2))"
sub set set
] ++ array_preamble ()
let smtlib_preamble
= [ spr "(set-logic QF_UFLIA)"
; spr "(define-sort %s () Int)" elt
; spr "(define-sort %s () Int)" set
; spr "(declare-fun %s () %s)" emp set
; spr "(declare-fun %s (%s %s) %s)" add set elt set
; spr "(declare-fun %s (%s %s) %s)" cup set set set
; spr "(declare-fun %s (%s %s) %s)" cap set set set
; spr "(declare-fun %s (%s %s) %s)" dif set set set
; spr "(declare-fun %s (%s %s) Bool)" sub set set
; spr "(declare-fun %s (%s %s) Bool)" mem elt set
; spr "(declare-fun %s (%s %s) %s)" sel map elt elt
; spr "(declare-fun %s (%s %s %s) %s)" sto map elt elt map
(* HIDE?
; spr "(assert (forall ((x %s)) (not (%s x %s))))"
elt mem emp
; spr "(assert (forall ((x %s) (s1 %s) (s2 %s))
(= (%s x (%s s1 s2)) (or (%s x s1) (%s x s2)))))"
elt set set mem cup mem mem
; spr "(assert (forall ((x %s) (s1 %s) (s2 %s))
(= (%s x (%s s1 s2)) (and (%s x s1) (%s x s2)))))"
elt set set mem cap mem mem
; spr "(assert (forall ((x %s) (s1 %s) (s2 %s))
(= (%s x (%s s1 s2)) (and (%s x s1) (not (%s x s2))))))"
elt set set mem dif mem mem
; spr "(assert (forall ((x %s) (s %s) (y %s))
(= (%s x (%s s y)) (or (%s x s) (= x y)))))"
elt set elt mem add mem
*)
]
let mkSetSort _ _ = set
let mkEmptySet _ _ = emp
let mkSetAdd _ s x = spr "(%s %s %s)" add s x
let mkSetMem _ x s = spr "(%s %s %s)" mem x s
let mkSetCup _ s t = spr "(%s %s %s)" cup s t
let mkSetCap _ s t = spr "(%s %s %s)" cap s t
let mkSetDif _ s t = spr "(%s %s %s)" dif s t
let mkSetSub _ s t = spr "(%s %s %s)" sub s t
let mkMapSort c k v = map
let mkMapSelect c m k = spr "(%s %s %s)" sel m k
let mkMapStore c m k v = spr "(%s %s %s %s)" sto m k v
let mkSizeSort _ n = spr "%d" n
let mkBitSort _ s = spr "(_ BitVec %s)" s
let mkBitAnd _ x y = spr "(bvand %s %s)" x y
let mkBitOr _ x y = spr "(bvor %s %s)" x y
(******************************************************************)
(**************** SMT IO ******************************************)
(** https://raw.github.com/ravichugh/djs/master/src/zzz.ml ********)
(******************************************************************)
(* "z3 -smt2 -in" *)
(* "z3 -smtc SOFT_TIMEOUT=1000 -in" *)
(* "z3 -smtc -in MBQI=false" *)
let smt_cmd = function
| Z3 -> "z3 -smt2 -in MODEL=false MODEL.PARTIAL=true smt.mbqi=false auto-config=false"
| Mathsat -> "mathsat -input=smt2"
| Cvc4 -> "cvc4 --incremental -L smtlib2"
let smt_preamble = function
| Z3 -> z3_preamble ()
| Cvc4 -> cvc4_preamble ()
| _ -> smtlib_preamble
let smt_write_raw me s =
output_now me.clog s;
output_now me.cout s
(* copied from String.trim in ocaml-4.0 since mingw-ocaml uses 3.x *)
let trim s =
let is_space = function
| ' ' | '\012' | '\n' | '\r' | '\t' -> true
| _ -> false in
let len = String.length s in
let i = ref 0 in
while !i < len && is_space (String.get s !i) do
incr i
done;
let j = ref (len - 1) in
while !j >= !i && is_space (String.get s !j) do
decr j
done;
if !i = 0 && !j = len - 1 then
s
else if !j >= !i then
String.sub s !i (!j - !i + 1)
else
""
(* strip off trailing whitespace, e.g. \r on windows.. *)
let smt_read_raw me =
trim (input_line me.cin)
let smt_write me ?nl:(nl=true) ?tab:(tab=false) s =
let pre = if tab then " " else "" in
let suf = if nl then "\n" else "" in
smt_write_raw me (pre^s^suf)
let rec smt_read me
= match smt_read_raw me with
| "sat" -> Sat
| "unsat" -> Unsat
| "success" -> smt_read me
| "unknown" -> Unknown
| s -> Error s
(* val interact : context -> cmd -> resp *)
let interact me = function
| Declare (x, ts, t) ->
let _ = smt_write me <| spr "(declare-fun %s (%s) %s)" x (String.concat " " ts) t in
Ok
| Push ->
let _ = smt_write me <| "(push 1)" in
Ok
| Pop ->
let _ = smt_write me <| "(pop 1)" in
Ok
| CheckSat ->
let _ = smt_write me <| "(check-sat)" in
smt_read me
| AssertCnstr a ->
let _ = smt_write me <| spr "(assert %s)" a in
Ok
| Distinct az ->
let _ = smt_write me <| spr "(assert (distinct %s))" (String.concat " " az) in
Ok
(* API *)
let smt_decl me x ts t
= match interact me (Declare (x, ts, t)) with
| Ok -> ()
| _ -> assertf "crash: SMTLIB2 smt_decl"
(* API *)
let smt_push me
= match interact me Push with
| Ok -> incr nb_push; ()
| _ -> assertf "crash: SMTLIB2 smt_push"
(* API *)
let smt_pop me
= match interact me Pop with
| Ok -> incr nb_pop; ()
| _ -> assertf "crash: SMTLIB2 smt_pop"
(* API *)
let smt_check_unsat me
= match interact me CheckSat with
| Unsat -> true
| Sat -> false
| Unknown -> false
| e -> assertf "crash: SMTLIB2 smt_check_unsat %s" (respString e)
(* API *)
let smt_assert_cnstr me p
= match interact me (AssertCnstr p) with
| Ok -> ()
| _ -> assertf "crash: SMTLIB2 smt_assert_cnstr"
(* API *)
let smt_assert_distinct me az
= match interact me (Distinct az) with
| Ok -> ()
| _ -> assertf "crash: SMTLIB2 smt_assert_distinct"
let solver () =
match !Co.smt_solver with
| Some "z3" -> Z3
| Some "mathsat" -> Mathsat
| Some "cvc4" -> Cvc4
| Some str -> assertf "ERROR: fixpoint does not yet support SMTSOLVER: %s" str
| None -> assertf "ERROR: undefined solver for smtLIB2"
let mkContext _ =
let s = solver () in
let ci, co = Unix.open_process <| smt_cmd s in
let cl = open_out <| Co.get_smt2_file () in
let pre = smt_preamble s in
let ctx = { cin = ci; cout = co; clog = cl } in
let _ = List.iter (smt_write ctx) pre in
ctx
(***********************************************************************)
(*********************** AST Constructors ******************************)
(***********************************************************************)
let stringSymbol _ s = s
let astString _ a = a
let sortString _ s = s
let isBool c a = failwith "TODO:SMTLib2.isBool"
let boundVar me i t = failwith "TODO:SMTLib2.boundVar"
let var me x t =
let _ = smt_decl me x [] t in
x
let funcDecl me s ta t =
let _ = smt_decl me s (Array.to_list ta) t in
s
let mkIntSort _ = "Int"
let mkRealSort _ = "Real"
let mkBoolSort _ = "Bool"
let mkInt _ i _ = if i >= 0 then string_of_int i
else spr "(- %d)" (abs i)
let mkReal _ i _ = if i >= 0. then string_of_float i ^ "0" (* add trailing 0 for floats like 1. *)
else spr "(- %s)" (string_of_float (i *. -1.0) ^ "0")
let mkLit _ l _ = l
let mkTrue _ = "true"
let mkFalse _ = "false"
let mkAll _ _ _ _ = failwith "TODO:SMTLib2.mkAll"
let mkRel _ r a1 a2
= match r with
| A.Eq
| A.Ueq -> spr "(= %s %s)" a1 a2
| A.Ne
| A.Une -> spr "(not (= %s %s))" a1 a2
| A.Gt -> spr "(> %s %s)" a1 a2
| A.Ge -> spr "(>= %s %s)" a1 a2
| A.Lt -> spr "(< %s %s)" a1 a2
| A.Le -> spr "(<= %s %s)" a1 a2
let mkApp _ f = function
| [] -> f
| az -> spr "(%s %s)" f (String.concat " " az)
let opStr = function
| A.Plus -> "+"
| A.Minus -> "-"
| A.Times -> "*"
| A.Div -> "/"
| A.Mod -> "mod"
let mkOp op a1 a2
= spr "(%s %s %s)" (opStr op) a1 a2
let mkMul _ = mkOp A.Times
let mkDiv _ = mkOp A.Div
let mkAdd _ = mkOp A.Plus
let mkSub _ = mkOp A.Minus
let mkMod _ = mkOp A.Mod
let mkIte _ a1 a2 a3
= spr "(ite %s %s %s)" a1 a2 a3
let mkNot _ a
= spr "(not %s)" a
let mkAnd _ az
= spr "(and %s)" (String.concat " " az)
let mkOr _ az
= spr "(or %s)" (String.concat " " az)
let mkImp _ a1 a2
= spr "(=> %s %s)" a1 a2
let mkIff _ a1 a2
= spr "(= %s %s)" a1 a2
(*******************************************************************)
(*********************** Queries ***********************************)
(*******************************************************************)
let us_ref = ref 0
(* API *)
let unsat me =
let _ = if mydebug then begin
Printf.printf "[%d] UNSAT 1 " (us_ref += 1);
flush stdout
end
in
let rv = BS.time "SMT.check_unsat" smt_check_unsat me in
let _ = if mydebug then (Printf.printf "UNSAT 2 \n"; flush stdout) in
let _ = if rv then ignore (nb_unsat += 1) in
rv
(* API *)
let assertAxiom me p
= (* Co.bprintf mydebug "@[Pushing axiom %s@]@." (astString me p); *)
BS.time "assertAxiom" (smt_assert_cnstr me) p;
asserts (not (unsat me)) "ERROR: Axiom makes background theory inconsistent!"
(* API *)
let assertDistinct me = function
| ((x1::x2::_) as az) -> smt_assert_distinct me az
| _ -> ()
(* API *)
let bracket me f
= Misc.bracket (fun _ -> smt_push me) (fun _ -> smt_pop me) f
(* API *)
let assertPreds me ps
= List.iter (fun p -> BS.time "assertPreds" (smt_assert_cnstr me) p) ps
(* API *)
let print_stats ppf () =
F.fprintf ppf "SMT stats: pushes=%d, pops=%d, unsats=%d \n"
!nb_push !nb_pop !nb_unsat
end