From 15e5a4224d4834b6c9d82160511728bdbc1af4bf Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 25 Nov 2015 10:04:01 +0100 Subject: [PATCH] ocp-indent all the files, for the greater good! --- smt/cc.ml | 154 ++++++------- smt/cc.mli | 14 +- smt/expr.ml | 18 +- smt/expr.mli | 26 +-- smt/mcsat.ml | 88 ++++---- smt/sig.mli | 6 +- smt/smt.ml | 40 ++-- smt/unionfind.ml | 126 +++++------ smt/unionfind.mli | 12 +- solver/internal.ml | 116 +++++----- solver/log_intf.ml | 4 +- solver/res.ml | 8 +- solver/res_intf.ml | 2 +- solver/tseitin.ml | 40 ++-- util/either.ml | 8 +- util/either.mli | 6 +- util/sat_solve.ml | 72 +++--- util/smtlib/lexsmtlib.mll | 4 +- util/smtlib/parsesmtlib.mly | 404 +++++++++++++++++----------------- util/smtlib/smtlib.ml | 130 +++++------ util/smtlib/smtlib_syntax.mli | 16 +- 21 files changed, 647 insertions(+), 647 deletions(-) diff --git a/smt/cc.ml b/smt/cc.ml index d71621c1..cbfa7d97 100644 --- a/smt/cc.ml +++ b/smt/cc.ml @@ -6,94 +6,94 @@ Copyright 2014 Simon Cruanes module Make(T : Sig.OrderedType) = struct - module M = Map.Make(T) - module U = Unionfind.Make(T) + module M = Map.Make(T) + module U = Unionfind.Make(T) - exception Unsat of (T.t * T.t * (T.t list)) + exception Unsat of (T.t * T.t * (T.t list)) - type t = { - repr : U.t; - expl : T.t M.t; - size : int M.t; - } + type t = { + repr : U.t; + expl : T.t M.t; + size : int M.t; + } - let empty = { - repr = U.empty; - expl = M.empty; - size = M.empty; - } + let empty = { + repr = U.empty; + expl = M.empty; + size = M.empty; + } - let repr t a = U.find t.repr a + let repr t a = U.find t.repr a - let map_find m v default = try M.find v m with Not_found -> default - let find_parent v m = map_find m v v + let map_find m v default = try M.find v m with Not_found -> default + let find_parent v m = map_find m v v - let rev_root m root = - let rec aux m curr next = - if T.compare curr next = 0 then - m, curr - else - let parent = find_parent next m in - let m' = M.add next curr (M.remove curr m) in - aux m' next parent - in - aux m root (find_parent root m) + let rev_root m root = + let rec aux m curr next = + if T.compare curr next = 0 then + m, curr + else + let parent = find_parent next m in + let m' = M.add next curr (M.remove curr m) in + aux m' next parent + in + aux m root (find_parent root m) - let rec root m acc curr = - let parent = find_parent curr m in - if T.compare curr parent = 0 then - curr :: acc - else - root m (curr :: acc) parent + let rec root m acc curr = + let parent = find_parent curr m in + if T.compare curr parent = 0 then + curr :: acc + else + root m (curr :: acc) parent - let expl t a b = - let rec aux last = function - | x :: r, y :: r' when T.compare x y = 0 -> - aux (Some x) (r, r') - | l, l' -> begin match last with - | Some z -> List.rev_append (z :: l) l' - | None -> List.rev_append l l' - end - in - aux None (root t.expl [] a, root t.expl [] b) + let expl t a b = + let rec aux last = function + | x :: r, y :: r' when T.compare x y = 0 -> + aux (Some x) (r, r') + | l, l' -> begin match last with + | Some z -> List.rev_append (z :: l) l' + | None -> List.rev_append l l' + end + in + aux None (root t.expl [] a, root t.expl [] b) - let add_eq_aux t i j = - if T.compare (U.find t.repr i) (U.find t.repr j) = 0 then - t - else - let m, old_root_i = rev_root t.expl i in - let m, old_root_j = rev_root m j in - let nb_i = map_find t.size old_root_i 0 in - let nb_j = map_find t.size old_root_j 0 in - if nb_i < nb_j then { - repr = t.repr; - expl = M.add i j m; - size = M.add j (nb_i + nb_j + 1) t.size; } - else { - repr = t.repr; - expl = M.add j i m; - size = M.add i (nb_i + nb_j + 1) t.size; } + let add_eq_aux t i j = + if T.compare (U.find t.repr i) (U.find t.repr j) = 0 then + t + else + let m, old_root_i = rev_root t.expl i in + let m, old_root_j = rev_root m j in + let nb_i = map_find t.size old_root_i 0 in + let nb_j = map_find t.size old_root_j 0 in + if nb_i < nb_j then { + repr = t.repr; + expl = M.add i j m; + size = M.add j (nb_i + nb_j + 1) t.size; } + else { + repr = t.repr; + expl = M.add j i m; + size = M.add i (nb_i + nb_j + 1) t.size; } - let add_eq t i j = - let t' = add_eq_aux t i j in - try - let u' = U.union t.repr i j in - { t' with repr = u' } - with U.Unsat (a, b) -> - raise (Unsat (a, b, expl t' a b)) + let add_eq t i j = + let t' = add_eq_aux t i j in + try + let u' = U.union t.repr i j in + { t' with repr = u' } + with U.Unsat (a, b) -> + raise (Unsat (a, b, expl t' a b)) - let add_neq t i j = - try - let u' = U.forbid t.repr i j in - { t with repr = u' } - with U.Unsat (a, b) -> - raise (Unsat (a, b, expl t a b)) + let add_neq t i j = + try + let u' = U.forbid t.repr i j in + { t with repr = u' } + with U.Unsat (a, b) -> + raise (Unsat (a, b, expl t a b)) - let are_neq t a b = - try - ignore (U.union t.repr a b); - false - with U.Unsat _ -> - true + let are_neq t a b = + try + ignore (U.union t.repr a b); + false + with U.Unsat _ -> + true end diff --git a/smt/cc.mli b/smt/cc.mli index 2f92550d..005264d8 100644 --- a/smt/cc.mli +++ b/smt/cc.mli @@ -5,14 +5,14 @@ Copyright 2014 Simon Cruanes *) module Make(T : Sig.OrderedType) : sig - type t + type t - exception Unsat of (T.t * T.t * (T.t list)) + exception Unsat of (T.t * T.t * (T.t list)) - val empty : t - val add_eq : t -> T.t -> T.t -> t - val add_neq : t -> T.t -> T.t -> t + val empty : t + val add_eq : t -> T.t -> T.t -> t + val add_neq : t -> T.t -> T.t -> t - val repr : t -> T.t -> T.t - val are_neq : t -> T.t -> T.t -> bool + val repr : t -> T.t -> T.t + val are_neq : t -> T.t -> T.t -> bool end diff --git a/smt/expr.ml b/smt/expr.ml index 9e13da2d..b6d868cc 100644 --- a/smt/expr.ml +++ b/smt/expr.ml @@ -8,9 +8,9 @@ exception Invalid_var type var = string type formula = - | Prop of int - | Equal of var * var - | Distinct of var * var + | Prop of int + | Equal of var * var + | Distinct of var * var type t = formula type proof = unit @@ -18,16 +18,16 @@ let dummy = Prop 0 let max_fresh = ref 0 let fresh () = - incr max_fresh; + incr max_fresh; Prop (2 * !max_fresh + 1) let mk_prop i = - if i <> 0 && i < max_int / 2 then Prop (2 * i) - else raise Invalid_var + if i <> 0 && i < max_int / 2 then Prop (2 * i) + else raise Invalid_var let mk_var i = - if i <> "" then i - else raise Invalid_var + if i <> "" then i + else raise Invalid_var let mk_eq i j = Equal (mk_var (min i j), mk_var (max i j)) let mk_neq i j = Distinct (mk_var (min i j), mk_var (max i j)) @@ -42,7 +42,7 @@ let norm = function | Equal (a, b) -> Equal (a, b), false | Distinct (a, b) -> Equal (a, b), true - (* Only used after normalisation, so usual functions should work *) +(* Only used after normalisation, so usual functions should work *) let hash = Hashtbl.hash let equal = (=) let compare = Pervasives.compare diff --git a/smt/expr.mli b/smt/expr.mli index a62cf5ea..46fc5f2f 100644 --- a/smt/expr.mli +++ b/smt/expr.mli @@ -6,9 +6,9 @@ Copyright 2014 Simon Cruanes type var = string type formula = private - | Prop of int - | Equal of var * var - | Distinct of var * var + | Prop of int + | Equal of var * var + | Distinct of var * var type t = formula type proof = unit @@ -34,16 +34,16 @@ val add_label : Hstring.t -> t -> unit val print : Format.formatter -> t -> unit module Term : sig - type t = var - val hash : t -> int - val equal : t -> t -> bool - val compare : t -> t -> int - val print : Format.formatter -> t -> unit + type t = var + val hash : t -> int + val equal : t -> t -> bool + val compare : t -> t -> int + val print : Format.formatter -> t -> unit end module Formula : sig - type t = formula - val hash : t -> int - val equal : t -> t -> bool - val compare : t -> t -> int - val print : Format.formatter -> t -> unit + type t = formula + val hash : t -> int + val equal : t -> t -> bool + val compare : t -> t -> int + val print : Format.formatter -> t -> unit end diff --git a/smt/mcsat.ml b/smt/mcsat.ml index 47edf2c5..6514ea08 100644 --- a/smt/mcsat.ml +++ b/smt/mcsat.ml @@ -29,8 +29,8 @@ module Tsmt = struct } type level = { - cc : CC.t; - assign : (term * int) M.t; + cc : CC.t; + assign : (term * int) M.t; } type res = @@ -49,60 +49,60 @@ module Tsmt = struct let current_level () = !env let to_clause (a, b, l) = - Log.debug 10 "Expl : %s; %s" a b; - List.iter (fun s -> Log.debug 10 " |- %s" s) l; - let rec aux acc = function - | [] | [_] -> acc - | x :: ((y :: _) as r) -> - aux (Fsmt.mk_eq x y :: acc) r - in - (Fsmt.mk_eq a b) :: (List.rev_map Fsmt.neg (aux [] l)) + Log.debug 10 "Expl : %s; %s" a b; + List.iter (fun s -> Log.debug 10 " |- %s" s) l; + let rec aux acc = function + | [] | [_] -> acc + | x :: ((y :: _) as r) -> + aux (Fsmt.mk_eq x y :: acc) r + in + (Fsmt.mk_eq a b) :: (List.rev_map Fsmt.neg (aux [] l)) let assume s = - try - for i = s.start to s.start + s.length - 1 do - match s.get i with - | (Assign (x, v)), lvl -> - env := { !env with assign = M.add x (v, lvl) !env.assign } - | Lit f, _ -> - Log.debug 10 "Propagating in th : %s" (Log.on_fmt Fsmt.print f); - match f with - | Fsmt.Prop _ -> () - | Fsmt.Equal (i, j) -> - env := { !env with cc = CC.add_eq !env.cc i j } - | Fsmt.Distinct (i, j) -> - env := { !env with cc = CC.add_neq !env.cc i j } - done; - Sat - with CC.Unsat x -> - Log.debug 8 "Making explanation clause..."; - Unsat (to_clause x, ()) + try + for i = s.start to s.start + s.length - 1 do + match s.get i with + | (Assign (x, v)), lvl -> + env := { !env with assign = M.add x (v, lvl) !env.assign } + | Lit f, _ -> + Log.debug 10 "Propagating in th : %s" (Log.on_fmt Fsmt.print f); + match f with + | Fsmt.Prop _ -> () + | Fsmt.Equal (i, j) -> + env := { !env with cc = CC.add_eq !env.cc i j } + | Fsmt.Distinct (i, j) -> + env := { !env with cc = CC.add_neq !env.cc i j } + done; + Sat + with CC.Unsat x -> + Log.debug 8 "Making explanation clause..."; + Unsat (to_clause x, ()) let backtrack l = env := l let assign t = CC.repr !env.cc t let iter_assignable f = function - | Fsmt.Prop _ -> () - | Fsmt.Equal(a, b) - | Fsmt.Distinct (a, b) -> f a; f b + | Fsmt.Prop _ -> () + | Fsmt.Equal(a, b) + | Fsmt.Distinct (a, b) -> f a; f b let max (a: int) (b: int) = if a < b then b else a let eval = function - | Fsmt.Prop _ -> Unknown - | Fsmt.Equal (a, b) -> - begin try - let a', lvl_a = M.find a !env.assign in - let b', lvl_b = M.find b !env.assign in - Valued (Fsmt.Term.equal a' b', max lvl_a lvl_b) - with Not_found -> Unknown end - | Fsmt.Distinct (a, b) -> - begin try - let a', lvl_a = M.find a !env.assign in - let b', lvl_b = M.find b !env.assign in - Valued (not (Fsmt.Term.equal a' b'), max lvl_a lvl_b) - with Not_found -> Unknown end + | Fsmt.Prop _ -> Unknown + | Fsmt.Equal (a, b) -> + begin try + let a', lvl_a = M.find a !env.assign in + let b', lvl_b = M.find b !env.assign in + Valued (Fsmt.Term.equal a' b', max lvl_a lvl_b) + with Not_found -> Unknown end + | Fsmt.Distinct (a, b) -> + begin try + let a', lvl_a = M.find a !env.assign in + let b', lvl_b = M.find b !env.assign in + Valued (not (Fsmt.Term.equal a' b'), max lvl_a lvl_b) + with Not_found -> Unknown end let if_sat _ = () diff --git a/smt/sig.mli b/smt/sig.mli index d75d565b..1441de22 100644 --- a/smt/sig.mli +++ b/smt/sig.mli @@ -6,8 +6,8 @@ Copyright 2014 Simon Cruanes module type OrderedType = sig - (** Signature for ordered types (mainly for use in Map.Make) *) + (** Signature for ordered types (mainly for use in Map.Make) *) - type t - val compare : t -> t -> int + type t + val compare : t -> t -> int end diff --git a/smt/smt.ml b/smt/smt.ml index 85733eee..fc630713 100644 --- a/smt/smt.ml +++ b/smt/smt.ml @@ -31,28 +31,28 @@ module Tsmt = struct let current_level () = !env let to_clause (a, b, l) = - Log.debug 10 "Expl : %s; %s" a b; - List.iter (fun s -> Log.debug 10 " |- %s" s) l; - let rec aux acc = function - | [] | [_] -> acc - | x :: ((y :: _) as r) -> - aux (Fsmt.mk_eq x y :: acc) r - in - (Fsmt.mk_eq a b) :: (List.rev_map Fsmt.neg (aux [] l)) + Log.debug 10 "Expl : %s; %s" a b; + List.iter (fun s -> Log.debug 10 " |- %s" s) l; + let rec aux acc = function + | [] | [_] -> acc + | x :: ((y :: _) as r) -> + aux (Fsmt.mk_eq x y :: acc) r + in + (Fsmt.mk_eq a b) :: (List.rev_map Fsmt.neg (aux [] l)) let assume s = - try - for i = s.start to s.start + s.length - 1 do - Log.debug 10 "Propagating in th : %s" (Log.on_fmt Fsmt.print (s.get i)); - match s.get i with - | Fsmt.Prop _ -> () - | Fsmt.Equal (i, j) -> env := CC.add_eq !env i j - | Fsmt.Distinct (i, j) -> env := CC.add_neq !env i j - done; - Sat (current_level ()) - with CC.Unsat x -> - Log.debug 8 "Making explanation clause..."; - Unsat (to_clause x, ()) + try + for i = s.start to s.start + s.length - 1 do + Log.debug 10 "Propagating in th : %s" (Log.on_fmt Fsmt.print (s.get i)); + match s.get i with + | Fsmt.Prop _ -> () + | Fsmt.Equal (i, j) -> env := CC.add_eq !env i j + | Fsmt.Distinct (i, j) -> env := CC.add_neq !env i j + done; + Sat (current_level ()) + with CC.Unsat x -> + Log.debug 8 "Making explanation clause..."; + Unsat (to_clause x, ()) let backtrack l = env := l diff --git a/smt/unionfind.ml b/smt/unionfind.ml index f77c440c..7211fbe0 100644 --- a/smt/unionfind.ml +++ b/smt/unionfind.ml @@ -6,78 +6,78 @@ Copyright 2014 Simon Cruanes (* Union-find Module *) module Make(T : Sig.OrderedType) = struct - exception Unsat of T.t * T.t + exception Unsat of T.t * T.t - type var = T.t - module M = Map.Make(T) + type var = T.t + module M = Map.Make(T) -type t = { - rank : int M.t; - forbid : ((var * var) list); - mutable parent : var M.t; -} + type t = { + rank : int M.t; + forbid : ((var * var) list); + mutable parent : var M.t; + } -let empty = { - rank = M.empty; - forbid = []; - parent = M.empty; -} + let empty = { + rank = M.empty; + forbid = []; + parent = M.empty; + } -let find_map m i default = + let find_map m i default = try - M.find i m + M.find i m with Not_found -> - default + default -let rec find_aux f i = - let fi = find_map f i i in - if fi = i then - (f, i) - else - let f, r = find_aux f fi in - let f = M.add i r f in - (f, r) - -let find h x = - let f, cx = find_aux h.parent x in - h.parent <- f; - cx - -(* Highly ineficient treatment of inequalities *) -let possible h = - let aux (a, b) = - let ca = find h a in - let cb = find h b in - if T.compare ca cb = 0 then - raise (Unsat (a, b)) - in - List.iter aux h.forbid; - h - -let union_aux h x y = - let cx = find h x in - let cy = find h y in - if cx != cy then begin - let rx = find_map h.rank cx 0 in - let ry = find_map h.rank cy 0 in - if rx > ry then - { h with parent = M.add cy cx h.parent } - else if ry > rx then - { h with parent = M.add cx cy h.parent } + let rec find_aux f i = + let fi = find_map f i i in + if fi = i then + (f, i) else - { rank = M.add cx (rx + 1) h.rank; - parent = M.add cy cx h.parent; - forbid = h.forbid; } - end else + let f, r = find_aux f fi in + let f = M.add i r f in + (f, r) + + let find h x = + let f, cx = find_aux h.parent x in + h.parent <- f; + cx + + (* Highly ineficient treatment of inequalities *) + let possible h = + let aux (a, b) = + let ca = find h a in + let cb = find h b in + if T.compare ca cb = 0 then + raise (Unsat (a, b)) + in + List.iter aux h.forbid; h -let union h x y = possible (union_aux h x y) + let union_aux h x y = + let cx = find h x in + let cy = find h y in + if cx != cy then begin + let rx = find_map h.rank cx 0 in + let ry = find_map h.rank cy 0 in + if rx > ry then + { h with parent = M.add cy cx h.parent } + else if ry > rx then + { h with parent = M.add cx cy h.parent } + else + { rank = M.add cx (rx + 1) h.rank; + parent = M.add cy cx h.parent; + forbid = h.forbid; } + end else + h -let forbid h x y = - let cx = find h x in - let cy = find h y in - if cx = cy then - raise (Unsat (x, y)) - else - { h with forbid = (x, y) :: h.forbid } + let union h x y = possible (union_aux h x y) + + let forbid h x y = + let cx = find h x in + let cy = find h y in + if cx = cy then + raise (Unsat (x, y)) + else + { h with forbid = (x, y) :: h.forbid } end diff --git a/smt/unionfind.mli b/smt/unionfind.mli index 29df1f71..4d559ced 100644 --- a/smt/unionfind.mli +++ b/smt/unionfind.mli @@ -5,11 +5,11 @@ Copyright 2014 Simon Cruanes *) module Make(T : Sig.OrderedType) : sig - type t - exception Unsat of T.t * T.t - val empty : t - val find : t -> T.t -> T.t - val union : t -> T.t -> T.t -> t - val forbid : t -> T.t -> T.t -> t + type t + exception Unsat of T.t * T.t + val empty : t + val find : t -> T.t -> T.t + val union : t -> T.t -> T.t -> t + val forbid : t -> T.t -> T.t -> t end diff --git a/solver/internal.ml b/solver/internal.ml index ccdb3f32..a3a32ada 100644 --- a/solver/internal.ml +++ b/solver/internal.ml @@ -178,8 +178,8 @@ module Make (L : Log_intf.S)(St : Solver_types.S) let insert_var_order e = destruct_elt e (fun v -> Iheap.insert f_weight env.order v.lid) (fun v -> - Iheap.insert f_weight env.order v.vid; - iter_sub (fun t -> Iheap.insert f_weight env.order t.lid) v + Iheap.insert f_weight env.order v.vid; + iter_sub (fun t -> Iheap.insert f_weight env.order t.lid) v ) let var_decay_activity () = @@ -273,22 +273,22 @@ module Make (L : Log_intf.S)(St : Solver_types.S) env.tatoms_qhead <- env.qhead; for c = env.qhead to Vec.size env.trail - 1 do destruct (Vec.get env.trail c) - (fun v -> - v.assigned <- None; - v.level <- -1; - insert_var_order (elt_of_lit v) - ) - (fun a -> - if a.var.level <= lvl then begin - Vec.set env.trail env.qhead (of_atom a); - env.qhead <- env.qhead + 1 - end else begin - a.is_true <- false; - a.neg.is_true <- false; - a.var.level <- -1; - a.var.reason <- Bcp None; - insert_var_order (elt_of_var a.var) - end) + (fun v -> + v.assigned <- None; + v.level <- -1; + insert_var_order (elt_of_lit v) + ) + (fun a -> + if a.var.level <= lvl then begin + Vec.set env.trail env.qhead (of_atom a); + env.qhead <- env.qhead + 1 + end else begin + a.is_true <- false; + a.neg.is_true <- false; + a.var.level <- -1; + a.var.reason <- Bcp None; + insert_var_order (elt_of_var a.var) + end) done; Th.backtrack (Vec.get env.tenv_queue lvl); (* recover the right tenv *) Vec.shrink env.trail ((Vec.size env.trail) - env.qhead); @@ -325,18 +325,18 @@ module Make (L : Log_intf.S)(St : Solver_types.S) let th_eval a = if a.is_true || a.neg.is_true then None else match Th.eval a.lit with - | Th.Unknown -> None - | Th.Valued (b, lvl) -> - let atom = if b then a else a.neg in - enqueue_bool atom lvl (Semantic lvl); - Some b + | Th.Unknown -> None + | Th.Valued (b, lvl) -> + let atom = if b then a else a.neg in + enqueue_bool atom lvl (Semantic lvl); + Some b (* conflict analysis *) let max_lvl_atoms l = - List.fold_left (fun (max_lvl, acc) a -> - if a.var.level = max_lvl then (max_lvl, a :: acc) - else if a.var.level > max_lvl then (a.var.level, [a]) - else (max_lvl, acc)) (0, []) l + List.fold_left (fun (max_lvl, acc) a -> + if a.var.level = max_lvl then (max_lvl, a :: acc) + else if a.var.level > max_lvl then (a.var.level, [a]) + else (max_lvl, acc)) (0, []) l let backtrack_lvl is_uip = function | [] -> 0 @@ -351,8 +351,8 @@ module Make (L : Log_intf.S)(St : Solver_types.S) let history = ref [c_clause] in clause_bump_activity c_clause; let is_semantic a = match a.var.reason with - | Semantic _ -> true - | _ -> false + | Semantic _ -> true + | _ -> false in try while true do let lvl, atoms = max_lvl_atoms !c in @@ -361,34 +361,34 @@ module Make (L : Log_intf.S)(St : Solver_types.S) if lvl = 0 then raise Exit; match atoms with | [] | _ :: [] -> - L.debug 15 "Found UIP clause"; - is_uip := true; - raise Exit + L.debug 15 "Found UIP clause"; + is_uip := true; + raise Exit | _ when List.for_all is_semantic atoms -> - L.debug 15 "Found Semantic backtrack clause"; - raise Exit + L.debug 15 "Found Semantic backtrack clause"; + raise Exit | _ -> - decr tr_ind; - L.debug 20 "Looking at trail element %d" !tr_ind; - destruct (Vec.get env.trail !tr_ind) - (fun v -> L.debug 15 "%a" St.pp_lit v) - (fun a -> match a.var.reason with - | Bcp (Some d) -> - L.debug 15 "Propagation : %a" St.pp_atom a; - L.debug 15 " |- %a" St.pp_clause d; - let tmp, res = Proof.resolve (Proof.merge !c (Proof.to_list d)) in - begin match tmp with - | [] -> L.debug 15 "No lit to resolve over." - | [b] when b == a.var.pa -> - clause_bump_activity d; - var_bump_activity a.var; - history := d :: !history; - c := res - | _ -> assert false - end - | Bcp None -> L.debug 15 "Decision : %a" St.pp_atom a - | Semantic _ -> L.debug 15 "Semantic propagation : %a" St.pp_atom a) - done; assert false + decr tr_ind; + L.debug 20 "Looking at trail element %d" !tr_ind; + destruct (Vec.get env.trail !tr_ind) + (fun v -> L.debug 15 "%a" St.pp_lit v) + (fun a -> match a.var.reason with + | Bcp (Some d) -> + L.debug 15 "Propagation : %a" St.pp_atom a; + L.debug 15 " |- %a" St.pp_clause d; + let tmp, res = Proof.resolve (Proof.merge !c (Proof.to_list d)) in + begin match tmp with + | [] -> L.debug 15 "No lit to resolve over." + | [b] when b == a.var.pa -> + clause_bump_activity d; + var_bump_activity a.var; + history := d :: !history; + c := res + | _ -> assert false + end + | Bcp None -> L.debug 15 "Decision : %a" St.pp_atom a + | Semantic _ -> L.debug 15 "Semantic propagation : %a" St.pp_atom a) + done; assert false with Exit -> let learnt = List.sort (fun a b -> Pervasives.compare b.var.level a.var.level) !c in let blevel = backtrack_lvl !is_uip learnt in @@ -890,9 +890,9 @@ module Make (L : Log_intf.S)(St : Solver_types.S) Vec.grow_to_by_double env.learnts nbc; env.nb_init_clauses <- nbc; St.iter_elt (fun e -> destruct_elt e - (fun v -> L.debug 50 " -- %a" St.pp_lit v) - (fun a -> L.debug 50 " -- %a" St.pp_atom a.pa) - ); + (fun v -> L.debug 50 " -- %a" St.pp_lit v) + (fun a -> L.debug 50 " -- %a" St.pp_atom a.pa) + ); add_clauses ?tag cnf let assume ?tag cnf = diff --git a/solver/log_intf.ml b/solver/log_intf.ml index 35384dc4..5636255b 100644 --- a/solver/log_intf.ml +++ b/solver/log_intf.ml @@ -1,6 +1,6 @@ module type S = sig - val debug : int -> ('a, Buffer.t, unit, unit) format4 -> 'a - (** debug message *) + val debug : int -> ('a, Buffer.t, unit, unit) format4 -> 'a + (** debug message *) end diff --git a/solver/res.ml b/solver/res.ml index 6688a81e..d478ea84 100644 --- a/solver/res.ml +++ b/solver/res.ml @@ -282,10 +282,10 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct Stack.push (Leaving p) s; let node = expand p in begin match node.step with - | Resolution (p1, p2, _) -> - Stack.push (Enter p2) s; - Stack.push (Enter p1) s - | _ -> () + | Resolution (p1, p2, _) -> + Stack.push (Enter p2) s; + Stack.push (Enter p1) s + | _ -> () end end; fold_aux s h f acc diff --git a/solver/res_intf.ml b/solver/res_intf.ml index 419c433e..8dfce476 100644 --- a/solver/res_intf.ml +++ b/solver/res_intf.ml @@ -29,7 +29,7 @@ module type S = sig | Hypothesis | Lemma of lemma | Resolution of proof * proof * atom - (** Lazy type for proof trees. Proofs can be extended to proof nodes using functions defined later. *) + (** Lazy type for proof trees. Proofs can be extended to proof nodes using functions defined later. *) (** {3 Resolution helpers} *) val to_list : clause -> atom list diff --git a/solver/tseitin.ml b/solver/tseitin.ml index 4b00354f..b4ea0dbb 100644 --- a/solver/tseitin.ml +++ b/solver/tseitin.ml @@ -61,33 +61,33 @@ module Make (F : Formula_intf.S) = struct end let remove_true l = - let aux = function - | True -> None - | f -> Some f - in - opt_rev_map aux [] l + let aux = function + | True -> None + | f -> Some f + in + opt_rev_map aux [] l let remove_false l = - let aux = function - | Comb(Not, [True]) -> None - | f -> Some f - in - opt_rev_map aux [] l + let aux = function + | Comb(Not, [True]) -> None + | f -> Some f + in + opt_rev_map aux [] l let make_not f = make Not [f] let make_and l = - let l' = remove_true (flatten And [] l) in - if List.exists ((=) f_false) l' then - f_false - else - make And l' + let l' = remove_true (flatten And [] l) in + if List.exists ((=) f_false) l' then + f_false + else + make And l' let make_or l = let l' = remove_false (flatten Or [] l) in if List.exists ((=) f_true) l' then - f_true + f_true else match l' with | [] -> raise Empty_Or | [a] -> a @@ -110,19 +110,19 @@ module Make (F : Formula_intf.S) = struct | Comb (And, l) -> sform_list [] l (k %% make_and) | Comb (Or, l) -> sform_list [] l (k %% make_or) | Comb (Imp, [f1; f2]) -> - sform (make_not f1) (fun f1' -> sform f2 (fun f2' -> k (make_or [f1'; f2']))) + sform (make_not f1) (fun f1' -> sform f2 (fun f2' -> k (make_or [f1'; f2']))) | Comb (Not, [Comb (Imp, [f1; f2])]) -> - sform f1 (fun f1' -> sform (make_not f2) (fun f2' -> k (make_and [f1';f2']))) + sform f1 (fun f1' -> sform (make_not f2) (fun f2' -> k (make_and [f1';f2']))) | Comb ((Imp | Not), _) -> assert false | Lit _ -> k f and sform_list acc l k = match l with | [] -> k acc | f :: tail -> - sform f (fun f' -> sform_list (f'::acc) tail k) + sform f (fun f' -> sform_list (f'::acc) tail k) and sform_list_not acc l k = match l with | [] -> k acc | f :: tail -> - sform (make_not f) (fun f' -> sform_list_not (f'::acc) tail k) + sform (make_not f) (fun f' -> sform_list_not (f'::acc) tail k) let ( @@ ) l1 l2 = List.rev_append l1 l2 let ( @ ) = `Use_rev_append_instead (* prevent use of non-tailrec append *) diff --git a/util/either.ml b/util/either.ml index be411cd2..c48c6dda 100644 --- a/util/either.ml +++ b/util/either.ml @@ -5,12 +5,12 @@ Copyright 2014 Simon Cruanes *) type ('a, 'b) t = - | Left of 'a - | Right of 'b + | Left of 'a + | Right of 'b let mk_left a = Left a let mk_right b = Right b let destruct e f_left f_right = match e with - | Left a -> f_left a - | Right b -> f_right b + | Left a -> f_left a + | Right b -> f_right b diff --git a/util/either.mli b/util/either.mli index 7fde7015..3a90b9cf 100644 --- a/util/either.mli +++ b/util/either.mli @@ -5,11 +5,11 @@ Copyright 2014 Simon Cruanes *) type ('a, 'b) t = - | Left of 'a - | Right of 'b + | Left of 'a + | Right of 'b val mk_left : 'a -> ('a, 'b) t val mk_right : 'b -> ('a, 'b) t val destruct : ('a, 'b) t -> - ('a -> 'c) -> ('b -> 'c) -> 'c + ('a -> 'c) -> ('b -> 'c) -> 'c diff --git a/util/sat_solve.ml b/util/sat_solve.ml index afabf93e..9aedda8e 100644 --- a/util/sat_solve.ml +++ b/util/sat_solve.ml @@ -223,43 +223,43 @@ let main () = print_cnf cnf; match !solver with | Smt -> - Smt.assume cnf; - let res = Smt.solve () in - Gc.delete_alarm al; - begin match res with - | Smt.Sat -> - print "Sat (%f)" (Sys.time ()); - if !p_check then - if not (List.for_all (List.exists Smt.eval) cnf) then - raise Incorrect_model - | Smt.Unsat -> - print "Unsat (%f)" (Sys.time ()); - if !p_check then begin - let p = Smt.get_proof () in - print_proof p; - if !p_unsat_core then - print_unsat_core (Smt.unsat_core p) - end - end + Smt.assume cnf; + let res = Smt.solve () in + Gc.delete_alarm al; + begin match res with + | Smt.Sat -> + print "Sat (%f)" (Sys.time ()); + if !p_check then + if not (List.for_all (List.exists Smt.eval) cnf) then + raise Incorrect_model + | Smt.Unsat -> + print "Unsat (%f)" (Sys.time ()); + if !p_check then begin + let p = Smt.get_proof () in + print_proof p; + if !p_unsat_core then + print_unsat_core (Smt.unsat_core p) + end + end | Mcsat -> - Mcsat.assume cnf; - let res = Mcsat.solve () in - Gc.delete_alarm al; - begin match res with - | Mcsat.Sat -> - print "Sat (%f)" (Sys.time ()); - if !p_check then - if not (List.for_all (List.exists Mcsat.eval) cnf) then - raise Incorrect_model - | Mcsat.Unsat -> - print "Unsat (%f)" (Sys.time ()); - if !p_check then begin - let p = Mcsat.get_proof () in - print_mcproof p; - if !p_unsat_core then - print_mc_unsat_core (Mcsat.unsat_core p) - end - end + Mcsat.assume cnf; + let res = Mcsat.solve () in + Gc.delete_alarm al; + begin match res with + | Mcsat.Sat -> + print "Sat (%f)" (Sys.time ()); + if !p_check then + if not (List.for_all (List.exists Mcsat.eval) cnf) then + raise Incorrect_model + | Mcsat.Unsat -> + print "Unsat (%f)" (Sys.time ()); + if !p_check then begin + let p = Mcsat.get_proof () in + print_mcproof p; + if !p_unsat_core then + print_mc_unsat_core (Mcsat.unsat_core p) + end + end let () = try diff --git a/util/smtlib/lexsmtlib.mll b/util/smtlib/lexsmtlib.mll index e02e09df..b192c3f3 100644 --- a/util/smtlib/lexsmtlib.mll +++ b/util/smtlib/lexsmtlib.mll @@ -1,5 +1,5 @@ { - (* auto-generated by gt *) + (* auto-generated by gt *) open Parsesmtlib;; } @@ -45,4 +45,4 @@ rule token = parse | ( '0' | ['1'-'9'] ['0'-'9']* ) '.' ['0'-'9']+ as str { DECIMAL(str) } | eof { EOF } | _ {failwith((Lexing.lexeme lexbuf) ^ -": lexing error on line "^(string_of_int !Smtlib_util.line))}{} + ": lexing error on line "^(string_of_int !Smtlib_util.line))}{} diff --git a/util/smtlib/parsesmtlib.mly b/util/smtlib/parsesmtlib.mly index 343ccb27..65a14660 100644 --- a/util/smtlib/parsesmtlib.mly +++ b/util/smtlib/parsesmtlib.mly @@ -1,9 +1,9 @@ %{ -(* auto-generated by gt *) + (* auto-generated by gt *) - open Smtlib_syntax;; +open Smtlib_syntax;; let parse_error s = - print_string s; + print_string s; print_string " on line "; print_int !Smtlib_util.line; print_string "\n";; @@ -15,316 +15,316 @@ let parse_error s = %token EOF AS ASSERT CHECKSAT DECLAREFUN DECLARESORT DEFINEFUN DEFINESORT EXCLIMATIONPT EXISTS EXIT FORALL GETASSERT GETASSIGN GETINFO GETOPTION GETPROOF GETUNSATCORE GETVALUE LET LPAREN POP PUSH RPAREN SETINFO SETLOGIC SETOPTION UNDERSCORE %token ASCIIWOR BINARY DECIMAL HEXADECIMAL KEYWORD NUMERAL STRINGLIT SYMBOL -%type main + %type main -%type an_option + %type an_option -%type attribute + %type attribute -%type attributevalsexpr_attributevalue_sexpr5 + %type attributevalsexpr_attributevalue_sexpr5 -%type attributevalue + %type attributevalue -%type command + %type command -%type commanddeclarefun_command_sort13 + %type commanddeclarefun_command_sort13 -%type commanddefinefun_command_sortedvar15 + %type commanddefinefun_command_sortedvar15 -%type commanddefinesort_command_symbol11 + %type commanddefinesort_command_symbol11 -%type commandgetvalue_command_term24 + %type commandgetvalue_command_term24 -%type commands + %type commands -%type commands_commands_command30 + %type commands_commands_command30 -%type identifier + %type identifier -%type idunderscoresymnum_identifier_numeral33 + %type idunderscoresymnum_identifier_numeral33 -%type infoflag + %type infoflag -%type qualidentifier + %type qualidentifier -%type sexpr + %type sexpr -%type sexprinparen_sexpr_sexpr41 + %type sexprinparen_sexpr_sexpr41 -%type sort + %type sort -%type sortedvar + %type sortedvar -%type sortidsortmulti_sort_sort44 + %type sortidsortmulti_sort_sort44 -%type specconstant + %type specconstant -%type symbol + %type symbol -%type term + %type term -%type termexclimationpt_term_attribute64 + %type termexclimationpt_term_attribute64 -%type termexiststerm_term_sortedvar62 + %type termexiststerm_term_sortedvar62 -%type termforallterm_term_sortedvar60 + %type termforallterm_term_sortedvar60 -%type termletterm_term_varbinding58 + %type termletterm_term_varbinding58 -%type termqualidterm_term_term56 + %type termqualidterm_term_term56 -%type varbinding + %type varbinding -%type cur_position + %type cur_position -%% + %% -main: -| commands { Some($1) } -| EOF { None } + main: + | commands { Some($1) } + | EOF { None } -cur_position: -| { Smtlib_util.cur_pd() } + cur_position: + | { Smtlib_util.cur_pd() } -an_option: -| attribute { AnOptionAttribute(pd_attribute $1, $1) } + an_option: + | attribute { AnOptionAttribute(pd_attribute $1, $1) } -attribute: -| cur_position KEYWORD { AttributeKeyword($1, $2) } + attribute: + | cur_position KEYWORD { AttributeKeyword($1, $2) } -attribute: -| cur_position KEYWORD attributevalue { AttributeKeywordValue($1, $2, $3) } + attribute: + | cur_position KEYWORD attributevalue { AttributeKeywordValue($1, $2, $3) } -attributevalue: -| specconstant { AttributeValSpecConst(pd_specconstant $1, $1) } + attributevalue: + | specconstant { AttributeValSpecConst(pd_specconstant $1, $1) } -attributevalue: -| symbol { AttributeValSymbol(pd_symbol $1, $1) } + attributevalue: + | symbol { AttributeValSymbol(pd_symbol $1, $1) } -attributevalue: -| cur_position LPAREN attributevalsexpr_attributevalue_sexpr5 RPAREN { AttributeValSexpr($1, $3) } + attributevalue: + | cur_position LPAREN attributevalsexpr_attributevalue_sexpr5 RPAREN { AttributeValSexpr($1, $3) } -command: -| cur_position LPAREN SETLOGIC symbol RPAREN { CommandSetLogic($1, $4) } + command: + | cur_position LPAREN SETLOGIC symbol RPAREN { CommandSetLogic($1, $4) } -command: -| cur_position LPAREN SETOPTION an_option RPAREN { CommandSetOption($1, $4) } + command: + | cur_position LPAREN SETOPTION an_option RPAREN { CommandSetOption($1, $4) } -command: -| cur_position LPAREN SETINFO attribute RPAREN { CommandSetInfo($1, $4) } + command: + | cur_position LPAREN SETINFO attribute RPAREN { CommandSetInfo($1, $4) } -command: -| cur_position LPAREN DECLARESORT symbol NUMERAL RPAREN { CommandDeclareSort($1, $4, $5) } + command: + | cur_position LPAREN DECLARESORT symbol NUMERAL RPAREN { CommandDeclareSort($1, $4, $5) } -command: -| cur_position LPAREN DEFINESORT symbol LPAREN commanddefinesort_command_symbol11 RPAREN sort RPAREN { CommandDefineSort($1, $4, $6, $8) } + command: + | cur_position LPAREN DEFINESORT symbol LPAREN commanddefinesort_command_symbol11 RPAREN sort RPAREN { CommandDefineSort($1, $4, $6, $8) } -command: -| cur_position LPAREN DECLAREFUN symbol LPAREN commanddeclarefun_command_sort13 RPAREN sort RPAREN { CommandDeclareFun($1, $4, $6, $8) } + command: + | cur_position LPAREN DECLAREFUN symbol LPAREN commanddeclarefun_command_sort13 RPAREN sort RPAREN { CommandDeclareFun($1, $4, $6, $8) } -command: -| cur_position LPAREN DEFINEFUN symbol LPAREN commanddefinefun_command_sortedvar15 RPAREN sort term RPAREN { CommandDefineFun($1, $4, $6, $8, $9) } + command: + | cur_position LPAREN DEFINEFUN symbol LPAREN commanddefinefun_command_sortedvar15 RPAREN sort term RPAREN { CommandDefineFun($1, $4, $6, $8, $9) } -command: -| cur_position LPAREN PUSH NUMERAL RPAREN { CommandPush($1, $4) } + command: + | cur_position LPAREN PUSH NUMERAL RPAREN { CommandPush($1, $4) } -command: -| cur_position LPAREN POP NUMERAL RPAREN { CommandPop($1, $4) } + command: + | cur_position LPAREN POP NUMERAL RPAREN { CommandPop($1, $4) } -command: -| cur_position LPAREN ASSERT term RPAREN { CommandAssert($1, $4) } + command: + | cur_position LPAREN ASSERT term RPAREN { CommandAssert($1, $4) } -command: -| cur_position LPAREN CHECKSAT RPAREN { CommandCheckSat($1) } + command: + | cur_position LPAREN CHECKSAT RPAREN { CommandCheckSat($1) } -command: -| cur_position LPAREN GETASSERT RPAREN { CommandGetAssert($1) } + command: + | cur_position LPAREN GETASSERT RPAREN { CommandGetAssert($1) } -command: -| cur_position LPAREN GETPROOF RPAREN { CommandGetProof($1) } + command: + | cur_position LPAREN GETPROOF RPAREN { CommandGetProof($1) } -command: -| cur_position LPAREN GETUNSATCORE RPAREN { CommandGetUnsatCore($1) } + command: + | cur_position LPAREN GETUNSATCORE RPAREN { CommandGetUnsatCore($1) } -command: -| cur_position LPAREN GETVALUE LPAREN commandgetvalue_command_term24 RPAREN RPAREN { CommandGetValue($1, $5) } + command: + | cur_position LPAREN GETVALUE LPAREN commandgetvalue_command_term24 RPAREN RPAREN { CommandGetValue($1, $5) } -command: -| cur_position LPAREN GETASSIGN RPAREN { CommandGetAssign($1) } + command: + | cur_position LPAREN GETASSIGN RPAREN { CommandGetAssign($1) } -command: -| cur_position LPAREN GETOPTION KEYWORD RPAREN { CommandGetOption($1, $4) } + command: + | cur_position LPAREN GETOPTION KEYWORD RPAREN { CommandGetOption($1, $4) } -command: -| cur_position LPAREN GETINFO infoflag RPAREN { CommandGetInfo($1, $4) } + command: + | cur_position LPAREN GETINFO infoflag RPAREN { CommandGetInfo($1, $4) } -command: -| cur_position LPAREN EXIT RPAREN { CommandExit($1) } + command: + | cur_position LPAREN EXIT RPAREN { CommandExit($1) } -commands: -| commands_commands_command30 { Commands(pd_commands_commands_command30 $1, $1) } + commands: + | commands_commands_command30 { Commands(pd_commands_commands_command30 $1, $1) } -identifier: -| symbol { IdSymbol(pd_symbol $1, $1) } + identifier: + | symbol { IdSymbol(pd_symbol $1, $1) } -identifier: -| cur_position LPAREN UNDERSCORE symbol idunderscoresymnum_identifier_numeral33 RPAREN { IdUnderscoreSymNum($1, $4, $5) } + identifier: + | cur_position LPAREN UNDERSCORE symbol idunderscoresymnum_identifier_numeral33 RPAREN { IdUnderscoreSymNum($1, $4, $5) } -infoflag: -| cur_position KEYWORD { InfoFlagKeyword($1, $2) } + infoflag: + | cur_position KEYWORD { InfoFlagKeyword($1, $2) } -qualidentifier: -| identifier { QualIdentifierId(pd_identifier $1, $1) } + qualidentifier: + | identifier { QualIdentifierId(pd_identifier $1, $1) } -qualidentifier: -| cur_position LPAREN AS identifier sort RPAREN { QualIdentifierAs($1, $4, $5) } + qualidentifier: + | cur_position LPAREN AS identifier sort RPAREN { QualIdentifierAs($1, $4, $5) } -sexpr: -| specconstant { SexprSpecConst(pd_specconstant $1, $1) } + sexpr: + | specconstant { SexprSpecConst(pd_specconstant $1, $1) } -sexpr: -| symbol { SexprSymbol(pd_symbol $1, $1) } + sexpr: + | symbol { SexprSymbol(pd_symbol $1, $1) } -sexpr: -| cur_position KEYWORD { SexprKeyword($1, $2) } + sexpr: + | cur_position KEYWORD { SexprKeyword($1, $2) } -sexpr: -| cur_position LPAREN sexprinparen_sexpr_sexpr41 RPAREN { SexprInParen($1, $3) } + sexpr: + | cur_position LPAREN sexprinparen_sexpr_sexpr41 RPAREN { SexprInParen($1, $3) } -sort: -| identifier { SortIdentifier(pd_identifier $1, $1) } + sort: + | identifier { SortIdentifier(pd_identifier $1, $1) } -sort: -| cur_position LPAREN identifier sortidsortmulti_sort_sort44 RPAREN { SortIdSortMulti($1, $3, $4) } + sort: + | cur_position LPAREN identifier sortidsortmulti_sort_sort44 RPAREN { SortIdSortMulti($1, $3, $4) } -sortedvar: -| cur_position LPAREN symbol sort RPAREN { SortedVarSymSort($1, $3, $4) } + sortedvar: + | cur_position LPAREN symbol sort RPAREN { SortedVarSymSort($1, $3, $4) } -specconstant: -| cur_position DECIMAL { SpecConstsDec($1, $2) } + specconstant: + | cur_position DECIMAL { SpecConstsDec($1, $2) } -specconstant: -| cur_position NUMERAL { SpecConstNum($1, $2) } + specconstant: + | cur_position NUMERAL { SpecConstNum($1, $2) } -specconstant: -| cur_position STRINGLIT { SpecConstString($1, $2) } + specconstant: + | cur_position STRINGLIT { SpecConstString($1, $2) } -specconstant: -| cur_position HEXADECIMAL { SpecConstsHex($1, $2) } + specconstant: + | cur_position HEXADECIMAL { SpecConstsHex($1, $2) } -specconstant: -| cur_position BINARY { SpecConstsBinary($1, $2) } + specconstant: + | cur_position BINARY { SpecConstsBinary($1, $2) } -symbol: -| cur_position SYMBOL { Symbol($1, $2) } + symbol: + | cur_position SYMBOL { Symbol($1, $2) } -symbol: -| cur_position ASCIIWOR { SymbolWithOr($1, $2) } + symbol: + | cur_position ASCIIWOR { SymbolWithOr($1, $2) } -term: -| specconstant { TermSpecConst(pd_specconstant $1, $1) } + term: + | specconstant { TermSpecConst(pd_specconstant $1, $1) } -term: -| qualidentifier { TermQualIdentifier(pd_qualidentifier $1, $1) } + term: + | qualidentifier { TermQualIdentifier(pd_qualidentifier $1, $1) } -term: -| cur_position LPAREN qualidentifier termqualidterm_term_term56 RPAREN { TermQualIdTerm($1, $3, $4) } + term: + | cur_position LPAREN qualidentifier termqualidterm_term_term56 RPAREN { TermQualIdTerm($1, $3, $4) } -term: -| cur_position LPAREN LET LPAREN termletterm_term_varbinding58 RPAREN term RPAREN { TermLetTerm($1, $5, $7) } + term: + | cur_position LPAREN LET LPAREN termletterm_term_varbinding58 RPAREN term RPAREN { TermLetTerm($1, $5, $7) } -term: -| cur_position LPAREN FORALL LPAREN termforallterm_term_sortedvar60 RPAREN term RPAREN { TermForAllTerm($1, $5, $7) } + term: + | cur_position LPAREN FORALL LPAREN termforallterm_term_sortedvar60 RPAREN term RPAREN { TermForAllTerm($1, $5, $7) } -term: -| cur_position LPAREN EXISTS LPAREN termexiststerm_term_sortedvar62 RPAREN term RPAREN { TermExistsTerm($1, $5, $7) } + term: + | cur_position LPAREN EXISTS LPAREN termexiststerm_term_sortedvar62 RPAREN term RPAREN { TermExistsTerm($1, $5, $7) } -term: -| cur_position LPAREN EXCLIMATIONPT term termexclimationpt_term_attribute64 RPAREN { TermExclimationPt($1, $4, $5) } + term: + | cur_position LPAREN EXCLIMATIONPT term termexclimationpt_term_attribute64 RPAREN { TermExclimationPt($1, $4, $5) } -varbinding: -| cur_position LPAREN symbol term RPAREN { VarBindingSymTerm($1, $3, $4) } + varbinding: + | cur_position LPAREN symbol term RPAREN { VarBindingSymTerm($1, $3, $4) } -termexclimationpt_term_attribute64: -| attribute { (pd_attribute $1, ($1)::[]) } + termexclimationpt_term_attribute64: + | attribute { (pd_attribute $1, ($1)::[]) } -termexclimationpt_term_attribute64: -| attribute termexclimationpt_term_attribute64 { let (p, ( l1 )) = $2 in (pd_attribute $1, ($1)::(l1)) } + termexclimationpt_term_attribute64: + | attribute termexclimationpt_term_attribute64 { let (p, ( l1 )) = $2 in (pd_attribute $1, ($1)::(l1)) } -termexiststerm_term_sortedvar62: -| sortedvar { (pd_sortedvar $1, ($1)::[]) } + termexiststerm_term_sortedvar62: + | sortedvar { (pd_sortedvar $1, ($1)::[]) } -termexiststerm_term_sortedvar62: -| sortedvar termexiststerm_term_sortedvar62 { let (p, ( l1 )) = $2 in (pd_sortedvar $1, ($1)::(l1)) } + termexiststerm_term_sortedvar62: + | sortedvar termexiststerm_term_sortedvar62 { let (p, ( l1 )) = $2 in (pd_sortedvar $1, ($1)::(l1)) } -termforallterm_term_sortedvar60: -| sortedvar { (pd_sortedvar $1, ($1)::[]) } + termforallterm_term_sortedvar60: + | sortedvar { (pd_sortedvar $1, ($1)::[]) } -termforallterm_term_sortedvar60: -| sortedvar termforallterm_term_sortedvar60 { let (p, ( l1 )) = $2 in (pd_sortedvar $1, ($1)::(l1)) } + termforallterm_term_sortedvar60: + | sortedvar termforallterm_term_sortedvar60 { let (p, ( l1 )) = $2 in (pd_sortedvar $1, ($1)::(l1)) } -termletterm_term_varbinding58: -| varbinding { (pd_varbinding $1, ($1)::[]) } + termletterm_term_varbinding58: + | varbinding { (pd_varbinding $1, ($1)::[]) } -termletterm_term_varbinding58: -| varbinding termletterm_term_varbinding58 { let (p, ( l1 )) = $2 in (pd_varbinding $1, ($1)::(l1)) } + termletterm_term_varbinding58: + | varbinding termletterm_term_varbinding58 { let (p, ( l1 )) = $2 in (pd_varbinding $1, ($1)::(l1)) } -termqualidterm_term_term56: -| term { (pd_term $1, ($1)::[]) } + termqualidterm_term_term56: + | term { (pd_term $1, ($1)::[]) } -termqualidterm_term_term56: -| term termqualidterm_term_term56 { let (p, ( l1 )) = $2 in (pd_term $1, ($1)::(l1)) } + termqualidterm_term_term56: + | term termqualidterm_term_term56 { let (p, ( l1 )) = $2 in (pd_term $1, ($1)::(l1)) } -sortidsortmulti_sort_sort44: -| sort { (pd_sort $1, ($1)::[]) } + sortidsortmulti_sort_sort44: + | sort { (pd_sort $1, ($1)::[]) } -sortidsortmulti_sort_sort44: -| sort sortidsortmulti_sort_sort44 { let (p, ( l1 )) = $2 in (pd_sort $1, ($1)::(l1)) } + sortidsortmulti_sort_sort44: + | sort sortidsortmulti_sort_sort44 { let (p, ( l1 )) = $2 in (pd_sort $1, ($1)::(l1)) } -sexprinparen_sexpr_sexpr41: -| cur_position { ($1, []) } + sexprinparen_sexpr_sexpr41: + | cur_position { ($1, []) } -sexprinparen_sexpr_sexpr41: -| sexpr sexprinparen_sexpr_sexpr41 { let (p, ( l1 )) = $2 in (pd_sexpr $1, ($1)::(l1)) } + sexprinparen_sexpr_sexpr41: + | sexpr sexprinparen_sexpr_sexpr41 { let (p, ( l1 )) = $2 in (pd_sexpr $1, ($1)::(l1)) } -idunderscoresymnum_identifier_numeral33: -| cur_position NUMERAL { ($1, ($2)::[]) } + idunderscoresymnum_identifier_numeral33: + | cur_position NUMERAL { ($1, ($2)::[]) } -idunderscoresymnum_identifier_numeral33: -| cur_position NUMERAL idunderscoresymnum_identifier_numeral33 { let (p, ( l1 )) = $3 in ($1, ($2)::(l1)) } + idunderscoresymnum_identifier_numeral33: + | cur_position NUMERAL idunderscoresymnum_identifier_numeral33 { let (p, ( l1 )) = $3 in ($1, ($2)::(l1)) } -commands_commands_command30: -| cur_position { ($1, []) } + commands_commands_command30: + | cur_position { ($1, []) } -commands_commands_command30: -| command commands_commands_command30 { let (p, ( l1 )) = $2 in (pd_command $1, ($1)::(l1)) } + commands_commands_command30: + | command commands_commands_command30 { let (p, ( l1 )) = $2 in (pd_command $1, ($1)::(l1)) } -commandgetvalue_command_term24: -| term { (pd_term $1, ($1)::[]) } + commandgetvalue_command_term24: + | term { (pd_term $1, ($1)::[]) } -commandgetvalue_command_term24: -| term commandgetvalue_command_term24 { let (p, ( l1 )) = $2 in (pd_term $1, ($1)::(l1)) } + commandgetvalue_command_term24: + | term commandgetvalue_command_term24 { let (p, ( l1 )) = $2 in (pd_term $1, ($1)::(l1)) } -commanddefinefun_command_sortedvar15: -| cur_position { ($1, []) } + commanddefinefun_command_sortedvar15: + | cur_position { ($1, []) } -commanddefinefun_command_sortedvar15: -| sortedvar commanddefinefun_command_sortedvar15 { let (p, ( l1 )) = $2 in (pd_sortedvar $1, ($1)::(l1)) } + commanddefinefun_command_sortedvar15: + | sortedvar commanddefinefun_command_sortedvar15 { let (p, ( l1 )) = $2 in (pd_sortedvar $1, ($1)::(l1)) } -commanddeclarefun_command_sort13: -| cur_position { ($1, []) } + commanddeclarefun_command_sort13: + | cur_position { ($1, []) } -commanddeclarefun_command_sort13: -| sort commanddeclarefun_command_sort13 { let (p, ( l1 )) = $2 in (pd_sort $1, ($1)::(l1)) } + commanddeclarefun_command_sort13: + | sort commanddeclarefun_command_sort13 { let (p, ( l1 )) = $2 in (pd_sort $1, ($1)::(l1)) } -commanddefinesort_command_symbol11: -| cur_position { ($1, []) } + commanddefinesort_command_symbol11: + | cur_position { ($1, []) } -commanddefinesort_command_symbol11: -| symbol commanddefinesort_command_symbol11 { let (p, ( l1 )) = $2 in (pd_symbol $1, ($1)::(l1)) } + commanddefinesort_command_symbol11: + | symbol commanddefinesort_command_symbol11 { let (p, ( l1 )) = $2 in (pd_symbol $1, ($1)::(l1)) } -attributevalsexpr_attributevalue_sexpr5: -| cur_position { ($1, []) } + attributevalsexpr_attributevalue_sexpr5: + | cur_position { ($1, []) } -attributevalsexpr_attributevalue_sexpr5: -| sexpr attributevalsexpr_attributevalue_sexpr5 { let (p, ( l1 )) = $2 in (pd_sexpr $1, ($1)::(l1)) } + attributevalsexpr_attributevalue_sexpr5: + | sexpr attributevalsexpr_attributevalue_sexpr5 { let (p, ( l1 )) = $2 in (pd_sexpr $1, ($1)::(l1)) } diff --git a/util/smtlib/smtlib.ml b/util/smtlib/smtlib.ml index 2a1719b5..49057058 100644 --- a/util/smtlib/smtlib.ml +++ b/util/smtlib/smtlib.ml @@ -19,94 +19,94 @@ Hashtbl.add env "true" T.f_true;; Hashtbl.add env "false" T.f_false;; let get_atom s = - try - Hashtbl.find env s - with Not_found -> - let f = T.make_atom (F.fresh ()) in - Hashtbl.add env s f; - f + try + Hashtbl.find env s + with Not_found -> + let f = T.make_atom (F.fresh ()) in + Hashtbl.add env s f; + f (* Term translation *) let translate_const = function - | SpecConstsDec(_, s) - | SpecConstNum(_, s) - | SpecConstString(_, s) - | SpecConstsHex(_, s) - | SpecConstsBinary(_, s) -> s + | SpecConstsDec(_, s) + | SpecConstNum(_, s) + | SpecConstString(_, s) + | SpecConstsHex(_, s) + | SpecConstsBinary(_, s) -> s let translate_symbol = function - | Symbol(_, s) - | SymbolWithOr(_, s) -> s + | Symbol(_, s) + | SymbolWithOr(_, s) -> s let translate_id = function - | IdSymbol(_, s) -> translate_symbol s - | IdUnderscoreSymNum(_, s, n) -> raise Incomplete_translation + | IdSymbol(_, s) -> translate_symbol s + | IdUnderscoreSymNum(_, s, n) -> raise Incomplete_translation let translate_qualid = function - | QualIdentifierId(_, id) -> translate_id id - | QualIdentifierAs(_, id, s) -> raise Incomplete_translation + | QualIdentifierId(_, id) -> translate_id id + | QualIdentifierAs(_, id, s) -> raise Incomplete_translation let left_assoc s f = function - | x :: r -> List.fold_left f x r - | _ -> raise (Bad_arity s) + | x :: r -> List.fold_left f x r + | _ -> raise (Bad_arity s) let rec right_assoc s f = function - | [] -> raise (Bad_arity s) - | [x] -> x - | x :: r -> f x (right_assoc s f r) + | [] -> raise (Bad_arity s) + | [x] -> x + | x :: r -> f x (right_assoc s f r) let translate_atom = function - | TermSpecConst(_, const) -> translate_const const - | TermQualIdentifier(_, id) -> translate_qualid id - | _ -> raise Incomplete_translation + | TermSpecConst(_, const) -> translate_const const + | TermQualIdentifier(_, id) -> translate_qualid id + | _ -> raise Incomplete_translation let rec translate_term = function - | TermQualIdTerm(_, f, (_, l)) -> - begin match (translate_qualid f) with - | "=" -> - begin match (List.map translate_atom l) with - | [a; b] -> T.make_atom (F.mk_eq a b) - | _ -> assert false - end - | s -> - begin match s, (List.map translate_term l) with - (* CORE theory translation - 'distinct','ite' not yet implemented *) - | "not", [e] -> T.make_not e - | "not", _ -> raise (Bad_arity "not") - | "and", l -> T.make_and l - | "or", l -> T.make_or l - | "xor" as s, l -> left_assoc s T.make_xor l - | "=>" as s, l -> right_assoc s T.make_imply l - | _ -> - Format.printf "unknown : %s@." s; - raise Unknown_command - end - end - | e -> (get_atom (translate_atom e)) + | TermQualIdTerm(_, f, (_, l)) -> + begin match (translate_qualid f) with + | "=" -> + begin match (List.map translate_atom l) with + | [a; b] -> T.make_atom (F.mk_eq a b) + | _ -> assert false + end + | s -> + begin match s, (List.map translate_term l) with + (* CORE theory translation - 'distinct','ite' not yet implemented *) + | "not", [e] -> T.make_not e + | "not", _ -> raise (Bad_arity "not") + | "and", l -> T.make_and l + | "or", l -> T.make_or l + | "xor" as s, l -> left_assoc s T.make_xor l + | "=>" as s, l -> right_assoc s T.make_imply l + | _ -> + Format.printf "unknown : %s@." s; + raise Unknown_command + end + end + | e -> (get_atom (translate_atom e)) (* Command Translation *) let translate_command = function - | CommandDeclareFun(_, s, (_, []), _) -> - None - | CommandAssert(_, t) -> - Some (translate_term t) - | _ -> None + | CommandDeclareFun(_, s, (_, []), _) -> + None + | CommandAssert(_, t) -> + Some (translate_term t) + | _ -> None let rec translate_command_list acc = function - | [] -> acc - | c :: r -> - begin match translate_command c with - | None -> translate_command_list acc r - | Some t -> translate_command_list (t :: acc) r - end + | [] -> acc + | c :: r -> + begin match translate_command c with + | None -> translate_command_list acc r + | Some t -> translate_command_list (t :: acc) r + end let translate = function - | Some Commands (_, (_, l)) -> List.rev (translate_command_list [] l) - | None -> [] + | Some Commands (_, (_, l)) -> List.rev (translate_command_list [] l) + | None -> [] let parse file = - let f = open_in file in - let lexbuf = Lexing.from_channel f in - let commands = Parsesmtlib.main Lexsmtlib.token lexbuf in - close_in f; - translate commands + let f = open_in file in + let lexbuf = Lexing.from_channel f in + let commands = Parsesmtlib.main Lexsmtlib.token lexbuf in + close_in f; + translate commands diff --git a/util/smtlib/smtlib_syntax.mli b/util/smtlib/smtlib_syntax.mli index 491d229c..05ad8cc7 100644 --- a/util/smtlib/smtlib_syntax.mli +++ b/util/smtlib/smtlib_syntax.mli @@ -13,18 +13,18 @@ and attributevalue = AttributeValSpecConst of Smtlib_util.pd * specconstant | AttributeValSymbol of Smtlib_util.pd * symbol | AttributeValSexpr of Smtlib_util.pd * - attributevalsexpr_attributevalue_sexpr5 + attributevalsexpr_attributevalue_sexpr5 and command = CommandSetLogic of Smtlib_util.pd * symbol | CommandSetOption of Smtlib_util.pd * an_option | CommandSetInfo of Smtlib_util.pd * attribute | CommandDeclareSort of Smtlib_util.pd * symbol * string | CommandDefineSort of Smtlib_util.pd * symbol * - commanddefinesort_command_symbol11 * sort + commanddefinesort_command_symbol11 * sort | CommandDeclareFun of Smtlib_util.pd * symbol * - commanddeclarefun_command_sort13 * sort + commanddeclarefun_command_sort13 * sort | CommandDefineFun of Smtlib_util.pd * symbol * - commanddefinefun_command_sortedvar15 * sort * term + commanddefinefun_command_sortedvar15 * sort * term | CommandPush of Smtlib_util.pd * string | CommandPop of Smtlib_util.pd * string | CommandAssert of Smtlib_util.pd * term @@ -41,7 +41,7 @@ and commands = Commands of Smtlib_util.pd * commands_commands_command30 and identifier = IdSymbol of Smtlib_util.pd * symbol | IdUnderscoreSymNum of Smtlib_util.pd * symbol * - idunderscoresymnum_identifier_numeral33 + idunderscoresymnum_identifier_numeral33 and infoflag = InfoFlagKeyword of Smtlib_util.pd * string and qualidentifier = QualIdentifierId of Smtlib_util.pd * identifier @@ -54,7 +54,7 @@ and sexpr = and sort = SortIdentifier of Smtlib_util.pd * identifier | SortIdSortMulti of Smtlib_util.pd * identifier * - sortidsortmulti_sort_sort44 + sortidsortmulti_sort_sort44 and sortedvar = SortedVarSymSort of Smtlib_util.pd * symbol * sort and specconstant = SpecConstsDec of Smtlib_util.pd * string @@ -69,12 +69,12 @@ and term = TermSpecConst of Smtlib_util.pd * specconstant | TermQualIdentifier of Smtlib_util.pd * qualidentifier | TermQualIdTerm of Smtlib_util.pd * qualidentifier * - termqualidterm_term_term56 + termqualidterm_term_term56 | TermLetTerm of Smtlib_util.pd * termletterm_term_varbinding58 * term | TermForAllTerm of Smtlib_util.pd * termforallterm_term_sortedvar60 * term | TermExistsTerm of Smtlib_util.pd * termexiststerm_term_sortedvar62 * term | TermExclimationPt of Smtlib_util.pd * term * - termexclimationpt_term_attribute64 + termexclimationpt_term_attribute64 and varbinding = VarBindingSymTerm of Smtlib_util.pd * symbol * term and termexclimationpt_term_attribute64 = Smtlib_util.pd * attribute list and termexiststerm_term_sortedvar62 = Smtlib_util.pd * sortedvar list