simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-08 04:05:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

ocp-indent all the files, for the greater good!

Browse source
This commit is contained in:
Simon Cruanes 2015-11-25 10:04:01 +01:00
parent a729d2dafb
commit 15e5a4224d
21 changed files with 647 additions and 647 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

154
smt/cc.ml
View file

@ -6,94 +6,94 @@ Copyright 2014 Simon Cruanes
module Make(T : Sig.OrderedType) = struct module Make(T : Sig.OrderedType) = struct
module M = Map.Make(T) module M = Map.Make(T)
module U = Unionfind.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 = { type t = {
repr : U.t; repr : U.t;
expl : T.t M.t; expl : T.t M.t;
size : int M.t; size : int M.t;
} }
let empty = { let empty = {
repr = U.empty; repr = U.empty;
expl = M.empty; expl = M.empty;
size = 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 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 find_parent v m = map_find m v v
let rev_root m root = let rev_root m root =
let rec aux m curr next = let rec aux m curr next =
if T.compare curr next = 0 then if T.compare curr next = 0 then
m, curr m, curr
else else
let parent = find_parent next m in let parent = find_parent next m in
let m' = M.add next curr (M.remove curr m) in let m' = M.add next curr (M.remove curr m) in
aux m' next parent aux m' next parent
in in
aux m root (find_parent root m) aux m root (find_parent root m)
let rec root m acc curr = let rec root m acc curr =
let parent = find_parent curr m in let parent = find_parent curr m in
if T.compare curr parent = 0 then if T.compare curr parent = 0 then
curr :: acc curr :: acc
else else
root m (curr :: acc) parent root m (curr :: acc) parent
let expl t a b = let expl t a b =
let rec aux last = function let rec aux last = function
| x :: r, y :: r' when T.compare x y = 0 -> | x :: r, y :: r' when T.compare x y = 0 ->
aux (Some x) (r, r') aux (Some x) (r, r')
| l, l' -> begin match last with | l, l' -> begin match last with
| Some z -> List.rev_append (z :: l) l' | Some z -> List.rev_append (z :: l) l'
| None -> List.rev_append l l' | None -> List.rev_append l l'
end end
in in
aux None (root t.expl [] a, root t.expl [] b) aux None (root t.expl [] a, root t.expl [] b)
let add_eq_aux t i j = let add_eq_aux t i j =
if T.compare (U.find t.repr i) (U.find t.repr j) = 0 then if T.compare (U.find t.repr i) (U.find t.repr j) = 0 then
t t
else else
let m, old_root_i = rev_root t.expl i in let m, old_root_i = rev_root t.expl i in
let m, old_root_j = rev_root m j 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_i = map_find t.size old_root_i 0 in
let nb_j = map_find t.size old_root_j 0 in let nb_j = map_find t.size old_root_j 0 in
if nb_i < nb_j then { if nb_i < nb_j then {
repr = t.repr; repr = t.repr;
expl = M.add i j m; expl = M.add i j m;
size = M.add j (nb_i + nb_j + 1) t.size; } size = M.add j (nb_i + nb_j + 1) t.size; }
else { else {
repr = t.repr; repr = t.repr;
expl = M.add j i m; expl = M.add j i m;
size = M.add i (nb_i + nb_j + 1) t.size; } size = M.add i (nb_i + nb_j + 1) t.size; }
let add_eq t i j = let add_eq t i j =
let t' = add_eq_aux t i j in let t' = add_eq_aux t i j in
try try
let u' = U.union t.repr i j in let u' = U.union t.repr i j in
{ t' with repr = u' } { t' with repr = u' }
with U.Unsat (a, b) -> with U.Unsat (a, b) ->
raise (Unsat (a, b, expl t' a b)) raise (Unsat (a, b, expl t' a b))
let add_neq t i j = let add_neq t i j =
try try
let u' = U.forbid t.repr i j in let u' = U.forbid t.repr i j in
{ t with repr = u' } { t with repr = u' }
with U.Unsat (a, b) -> with U.Unsat (a, b) ->
raise (Unsat (a, b, expl t a b)) raise (Unsat (a, b, expl t a b))
let are_neq t a b = let are_neq t a b =
try try
ignore (U.union t.repr a b); ignore (U.union t.repr a b);
false false
with U.Unsat _ -> with U.Unsat _ ->
true true
end end

14
smt/cc.mli
View file

@ -5,14 +5,14 @@ Copyright 2014 Simon Cruanes
*) *)
module Make(T : Sig.OrderedType) : sig 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 empty : t
val add_eq : t -> T.t -> T.t -> t val add_eq : t -> T.t -> T.t -> t
val add_neq : t -> T.t -> T.t -> t val add_neq : t -> T.t -> T.t -> t
val repr : t -> T.t -> T.t val repr : t -> T.t -> T.t
val are_neq : t -> T.t -> T.t -> bool val are_neq : t -> T.t -> T.t -> bool
end end

18
smt/expr.ml
View file

@ -8,9 +8,9 @@ exception Invalid_var
type var = string type var = string
type formula = type formula =
| Prop of int | Prop of int
| Equal of var * var | Equal of var * var
| Distinct of var * var | Distinct of var * var
type t = formula type t = formula
type proof = unit type proof = unit
@ -18,16 +18,16 @@ let dummy = Prop 0
let max_fresh = ref 0 let max_fresh = ref 0
let fresh () = let fresh () =
incr max_fresh; incr max_fresh;
Prop (2 * !max_fresh + 1) Prop (2 * !max_fresh + 1)
let mk_prop i = let mk_prop i =
if i <> 0 && i < max_int / 2 then Prop (2 * i) if i <> 0 && i < max_int / 2 then Prop (2 * i)
else raise Invalid_var else raise Invalid_var
let mk_var i = let mk_var i =
if i <> "" then i if i <> "" then i
else raise Invalid_var else raise Invalid_var
let mk_eq i j = Equal (mk_var (min i j), mk_var (max i j)) 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)) 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 | Equal (a, b) -> Equal (a, b), false
| Distinct (a, b) -> Equal (a, b), true | 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 hash = Hashtbl.hash
let equal = (=) let equal = (=)
let compare = Pervasives.compare let compare = Pervasives.compare

26
smt/expr.mli
View file

@ -6,9 +6,9 @@ Copyright 2014 Simon Cruanes
type var = string type var = string
type formula = private type formula = private
| Prop of int | Prop of int
| Equal of var * var | Equal of var * var
| Distinct of var * var | Distinct of var * var
type t = formula type t = formula
type proof = unit type proof = unit
@ -34,16 +34,16 @@ val add_label : Hstring.t -> t -> unit
val print : Format.formatter -> t -> unit val print : Format.formatter -> t -> unit
module Term : sig module Term : sig
type t = var type t = var
val hash : t -> int val hash : t -> int
val equal : t -> t -> bool val equal : t -> t -> bool
val compare : t -> t -> int val compare : t -> t -> int
val print : Format.formatter -> t -> unit val print : Format.formatter -> t -> unit
end end
module Formula : sig module Formula : sig
type t = formula type t = formula
val hash : t -> int val hash : t -> int
val equal : t -> t -> bool val equal : t -> t -> bool
val compare : t -> t -> int val compare : t -> t -> int
val print : Format.formatter -> t -> unit val print : Format.formatter -> t -> unit
end end

88
smt/mcsat.ml
View file

@ -29,8 +29,8 @@ module Tsmt = struct
} }
type level = { type level = {
cc : CC.t; cc : CC.t;
assign : (term * int) M.t; assign : (term * int) M.t;
} }
type res = type res =
@ -49,60 +49,60 @@ module Tsmt = struct
let current_level () = !env let current_level () = !env
let to_clause (a, b, l) = let to_clause (a, b, l) =
Log.debug 10 "Expl : %s; %s" a b; Log.debug 10 "Expl : %s; %s" a b;
List.iter (fun s -> Log.debug 10 " |- %s" s) l; List.iter (fun s -> Log.debug 10 " |- %s" s) l;
let rec aux acc = function let rec aux acc = function
| [] | [_] -> acc | [] | [_] -> acc
| x :: ((y :: _) as r) -> | x :: ((y :: _) as r) ->
aux (Fsmt.mk_eq x y :: acc) r aux (Fsmt.mk_eq x y :: acc) r
in in
(Fsmt.mk_eq a b) :: (List.rev_map Fsmt.neg (aux [] l)) (Fsmt.mk_eq a b) :: (List.rev_map Fsmt.neg (aux [] l))
let assume s = let assume s =
try try
for i = s.start to s.start + s.length - 1 do for i = s.start to s.start + s.length - 1 do
match s.get i with match s.get i with
| (Assign (x, v)), lvl -> | (Assign (x, v)), lvl ->
env := { !env with assign = M.add x (v, lvl) !env.assign } env := { !env with assign = M.add x (v, lvl) !env.assign }
| Lit f, _ -> | Lit f, _ ->
Log.debug 10 "Propagating in th : %s" (Log.on_fmt Fsmt.print f); Log.debug 10 "Propagating in th : %s" (Log.on_fmt Fsmt.print f);
match f with match f with
| Fsmt.Prop _ -> () | Fsmt.Prop _ -> ()
| Fsmt.Equal (i, j) -> | Fsmt.Equal (i, j) ->
env := { !env with cc = CC.add_eq !env.cc i j } env := { !env with cc = CC.add_eq !env.cc i j }
| Fsmt.Distinct (i, j) -> | Fsmt.Distinct (i, j) ->
env := { !env with cc = CC.add_neq !env.cc i j } env := { !env with cc = CC.add_neq !env.cc i j }
done; done;
Sat Sat
with CC.Unsat x -> with CC.Unsat x ->
Log.debug 8 "Making explanation clause..."; Log.debug 8 "Making explanation clause...";
Unsat (to_clause x, ()) Unsat (to_clause x, ())
let backtrack l = env := l let backtrack l = env := l
let assign t = CC.repr !env.cc t let assign t = CC.repr !env.cc t
let iter_assignable f = function let iter_assignable f = function
| Fsmt.Prop _ -> () | Fsmt.Prop _ -> ()
| Fsmt.Equal(a, b) | Fsmt.Equal(a, b)
| Fsmt.Distinct (a, b) -> f a; f b | Fsmt.Distinct (a, b) -> f a; f b
let max (a: int) (b: int) = if a < b then b else a let max (a: int) (b: int) = if a < b then b else a
let eval = function let eval = function
| Fsmt.Prop _ -> Unknown | Fsmt.Prop _ -> Unknown
| Fsmt.Equal (a, b) -> | Fsmt.Equal (a, b) ->
begin try begin try
let a', lvl_a = M.find a !env.assign in let a', lvl_a = M.find a !env.assign in
let b', lvl_b = M.find b !env.assign in let b', lvl_b = M.find b !env.assign in
Valued (Fsmt.Term.equal a' b', max lvl_a lvl_b) Valued (Fsmt.Term.equal a' b', max lvl_a lvl_b)
with Not_found -> Unknown end with Not_found -> Unknown end
| Fsmt.Distinct (a, b) -> | Fsmt.Distinct (a, b) ->
begin try begin try
let a', lvl_a = M.find a !env.assign in let a', lvl_a = M.find a !env.assign in
let b', lvl_b = M.find b !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) Valued (not (Fsmt.Term.equal a' b'), max lvl_a lvl_b)
with Not_found -> Unknown end with Not_found -> Unknown end
let if_sat _ = () let if_sat _ = ()

6
smt/sig.mli
View file

@ -6,8 +6,8 @@ Copyright 2014 Simon Cruanes
module type OrderedType = sig 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 type t
val compare : t -> t -> int val compare : t -> t -> int
end end

40
smt/smt.ml
View file

@ -31,28 +31,28 @@ module Tsmt = struct
let current_level () = !env let current_level () = !env
let to_clause (a, b, l) = let to_clause (a, b, l) =
Log.debug 10 "Expl : %s; %s" a b; Log.debug 10 "Expl : %s; %s" a b;
List.iter (fun s -> Log.debug 10 " |- %s" s) l; List.iter (fun s -> Log.debug 10 " |- %s" s) l;
let rec aux acc = function let rec aux acc = function
| [] | [_] -> acc | [] | [_] -> acc
| x :: ((y :: _) as r) -> | x :: ((y :: _) as r) ->
aux (Fsmt.mk_eq x y :: acc) r aux (Fsmt.mk_eq x y :: acc) r
in in
(Fsmt.mk_eq a b) :: (List.rev_map Fsmt.neg (aux [] l)) (Fsmt.mk_eq a b) :: (List.rev_map Fsmt.neg (aux [] l))
let assume s = let assume s =
try try
for i = s.start to s.start + s.length - 1 do 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)); Log.debug 10 "Propagating in th : %s" (Log.on_fmt Fsmt.print (s.get i));
match s.get i with match s.get i with
| Fsmt.Prop _ -> () | Fsmt.Prop _ -> ()
| Fsmt.Equal (i, j) -> env := CC.add_eq !env i j | Fsmt.Equal (i, j) -> env := CC.add_eq !env i j
| Fsmt.Distinct (i, j) -> env := CC.add_neq !env i j | Fsmt.Distinct (i, j) -> env := CC.add_neq !env i j
done; done;
Sat (current_level ()) Sat (current_level ())
with CC.Unsat x -> with CC.Unsat x ->
Log.debug 8 "Making explanation clause..."; Log.debug 8 "Making explanation clause...";
Unsat (to_clause x, ()) Unsat (to_clause x, ())
let backtrack l = env := l let backtrack l = env := l

126
smt/unionfind.ml
View file

@ -6,78 +6,78 @@ Copyright 2014 Simon Cruanes
(* Union-find Module *) (* Union-find Module *)
module Make(T : Sig.OrderedType) = struct module Make(T : Sig.OrderedType) = struct
exception Unsat of T.t * T.t exception Unsat of T.t * T.t
type var = T.t type var = T.t
module M = Map.Make(T) module M = Map.Make(T)
type t = { type t = {
rank : int M.t; rank : int M.t;
forbid : ((var * var) list); forbid : ((var * var) list);
mutable parent : var M.t; mutable parent : var M.t;
} }
let empty = { let empty = {
rank = M.empty; rank = M.empty;
forbid = []; forbid = [];
parent = M.empty; parent = M.empty;
} }
let find_map m i default = let find_map m i default =
try try
M.find i m M.find i m
with Not_found -> with Not_found ->
default default
let rec find_aux f i = let rec find_aux f i =
let fi = find_map f i i in let fi = find_map f i i in
if fi = i then if fi = i then
(f, i) (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 }
else else
{ rank = M.add cx (rx + 1) h.rank; let f, r = find_aux f fi in
parent = M.add cy cx h.parent; let f = M.add i r f in
forbid = h.forbid; } (f, r)
end else
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 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 union h x y = possible (union_aux h x y)
let cx = find h x in
let cy = find h y in let forbid h x y =
if cx = cy then let cx = find h x in
raise (Unsat (x, y)) let cy = find h y in
else if cx = cy then
{ h with forbid = (x, y) :: h.forbid } raise (Unsat (x, y))
else
{ h with forbid = (x, y) :: h.forbid }
end end

12
smt/unionfind.mli
View file

@ -5,11 +5,11 @@ Copyright 2014 Simon Cruanes
*) *)
module Make(T : Sig.OrderedType) : sig module Make(T : Sig.OrderedType) : sig
type t type t
exception Unsat of T.t * T.t exception Unsat of T.t * T.t
val empty : t val empty : t
val find : t -> T.t -> T.t val find : t -> T.t -> T.t
val union : t -> T.t -> T.t -> t val union : t -> T.t -> T.t -> t
val forbid : t -> T.t -> T.t -> t val forbid : t -> T.t -> T.t -> t
end end

116
solver/internal.ml
View file

@ -178,8 +178,8 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
let insert_var_order e = destruct_elt e 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.lid)
(fun v -> (fun v ->
Iheap.insert f_weight env.order v.vid; Iheap.insert f_weight env.order v.vid;
iter_sub (fun t -> Iheap.insert f_weight env.order t.lid) v iter_sub (fun t -> Iheap.insert f_weight env.order t.lid) v
) )
let var_decay_activity () = let var_decay_activity () =
@ -273,22 +273,22 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
env.tatoms_qhead <- env.qhead; env.tatoms_qhead <- env.qhead;
for c = env.qhead to Vec.size env.trail - 1 do for c = env.qhead to Vec.size env.trail - 1 do
destruct (Vec.get env.trail c) destruct (Vec.get env.trail c)
(fun v -> (fun v ->
v.assigned <- None; v.assigned <- None;
v.level <- -1; v.level <- -1;
insert_var_order (elt_of_lit v) insert_var_order (elt_of_lit v)
) )
(fun a -> (fun a ->
if a.var.level <= lvl then begin if a.var.level <= lvl then begin
Vec.set env.trail env.qhead (of_atom a); Vec.set env.trail env.qhead (of_atom a);
env.qhead <- env.qhead + 1 env.qhead <- env.qhead + 1
end else begin end else begin
a.is_true <- false; a.is_true <- false;
a.neg.is_true <- false; a.neg.is_true <- false;
a.var.level <- -1; a.var.level <- -1;
a.var.reason <- Bcp None; a.var.reason <- Bcp None;
insert_var_order (elt_of_var a.var) insert_var_order (elt_of_var a.var)
end) end)
done; done;
Th.backtrack (Vec.get env.tenv_queue lvl); (* recover the right tenv *) Th.backtrack (Vec.get env.tenv_queue lvl); (* recover the right tenv *)
Vec.shrink env.trail ((Vec.size env.trail) - env.qhead); 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 = let th_eval a =
if a.is_true || a.neg.is_true then None if a.is_true || a.neg.is_true then None
else match Th.eval a.lit with else match Th.eval a.lit with
| Th.Unknown -> None | Th.Unknown -> None
| Th.Valued (b, lvl) -> | Th.Valued (b, lvl) ->
let atom = if b then a else a.neg in let atom = if b then a else a.neg in
enqueue_bool atom lvl (Semantic lvl); enqueue_bool atom lvl (Semantic lvl);
Some b Some b
(* conflict analysis *) (* conflict analysis *)
let max_lvl_atoms l = let max_lvl_atoms l =
List.fold_left (fun (max_lvl, acc) a -> List.fold_left (fun (max_lvl, acc) a ->
if a.var.level = max_lvl then (max_lvl, a :: acc) if a.var.level = max_lvl then (max_lvl, a :: acc)
else if a.var.level > max_lvl then (a.var.level, [a]) else if a.var.level > max_lvl then (a.var.level, [a])
else (max_lvl, acc)) (0, []) l else (max_lvl, acc)) (0, []) l
let backtrack_lvl is_uip = function let backtrack_lvl is_uip = function
| [] -> 0 | [] -> 0
@ -351,8 +351,8 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
let history = ref [c_clause] in let history = ref [c_clause] in
clause_bump_activity c_clause; clause_bump_activity c_clause;
let is_semantic a = match a.var.reason with let is_semantic a = match a.var.reason with
| Semantic _ -> true | Semantic _ -> true
| _ -> false | _ -> false
in in
try while true do try while true do
let lvl, atoms = max_lvl_atoms !c in 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; if lvl = 0 then raise Exit;
match atoms with match atoms with
| [] | _ :: [] -> | [] | _ :: [] ->
L.debug 15 "Found UIP clause"; L.debug 15 "Found UIP clause";
is_uip := true; is_uip := true;
raise Exit raise Exit
| _ when List.for_all is_semantic atoms -> | _ when List.for_all is_semantic atoms ->
L.debug 15 "Found Semantic backtrack clause"; L.debug 15 "Found Semantic backtrack clause";
raise Exit raise Exit
| _ -> | _ ->
decr tr_ind; decr tr_ind;
L.debug 20 "Looking at trail element %d" !tr_ind; L.debug 20 "Looking at trail element %d" !tr_ind;
destruct (Vec.get env.trail !tr_ind) destruct (Vec.get env.trail !tr_ind)
(fun v -> L.debug 15 "%a" St.pp_lit v) (fun v -> L.debug 15 "%a" St.pp_lit v)
(fun a -> match a.var.reason with (fun a -> match a.var.reason with
| Bcp (Some d) -> | Bcp (Some d) ->
L.debug 15 "Propagation : %a" St.pp_atom a; L.debug 15 "Propagation : %a" St.pp_atom a;
L.debug 15 " |- %a" St.pp_clause d; L.debug 15 " |- %a" St.pp_clause d;
let tmp, res = Proof.resolve (Proof.merge !c (Proof.to_list d)) in let tmp, res = Proof.resolve (Proof.merge !c (Proof.to_list d)) in
begin match tmp with begin match tmp with
| [] -> L.debug 15 "No lit to resolve over." | [] -> L.debug 15 "No lit to resolve over."
| [b] when b == a.var.pa -> | [b] when b == a.var.pa ->
clause_bump_activity d; clause_bump_activity d;
var_bump_activity a.var; var_bump_activity a.var;
history := d :: !history; history := d :: !history;
c := res c := res
| _ -> assert false | _ -> assert false
end end
| Bcp None -> L.debug 15 "Decision : %a" St.pp_atom a | Bcp None -> L.debug 15 "Decision : %a" St.pp_atom a
| Semantic _ -> L.debug 15 "Semantic propagation : %a" St.pp_atom a) | Semantic _ -> L.debug 15 "Semantic propagation : %a" St.pp_atom a)
done; assert false done; assert false
with Exit -> with Exit ->
let learnt = List.sort (fun a b -> Pervasives.compare b.var.level a.var.level) !c in 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 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; Vec.grow_to_by_double env.learnts nbc;
env.nb_init_clauses <- nbc; env.nb_init_clauses <- nbc;
St.iter_elt (fun e -> destruct_elt e St.iter_elt (fun e -> destruct_elt e
(fun v -> L.debug 50 " -- %a" St.pp_lit v) (fun v -> L.debug 50 " -- %a" St.pp_lit v)
(fun a -> L.debug 50 " -- %a" St.pp_atom a.pa) (fun a -> L.debug 50 " -- %a" St.pp_atom a.pa)
); );
add_clauses ?tag cnf add_clauses ?tag cnf
let assume ?tag cnf = let assume ?tag cnf =

4
solver/log_intf.ml
View file

@ -1,6 +1,6 @@
module type S = sig module type S = sig
val debug : int -> ('a, Buffer.t, unit, unit) format4 -> 'a val debug : int -> ('a, Buffer.t, unit, unit) format4 -> 'a
(** debug message *) (** debug message *)
end end

8
solver/res.ml
View file

@ -282,10 +282,10 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct
Stack.push (Leaving p) s; Stack.push (Leaving p) s;
let node = expand p in let node = expand p in
begin match node.step with begin match node.step with
| Resolution (p1, p2, _) -> | Resolution (p1, p2, _) ->
Stack.push (Enter p2) s; Stack.push (Enter p2) s;
Stack.push (Enter p1) s Stack.push (Enter p1) s
| _ -> () | _ -> ()
end end
end; end;
fold_aux s h f acc fold_aux s h f acc

2
solver/res_intf.ml
View file

@ -29,7 +29,7 @@ module type S = sig
| Hypothesis | Hypothesis
| Lemma of lemma | Lemma of lemma
| Resolution of proof * proof * atom | 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} *) (** {3 Resolution helpers} *)
val to_list : clause -> atom list val to_list : clause -> atom list

40
solver/tseitin.ml
View file

@ -61,33 +61,33 @@ module Make (F : Formula_intf.S) = struct
end end
let remove_true l = let remove_true l =
let aux = function let aux = function
| True -> None | True -> None
| f -> Some f | f -> Some f
in in
opt_rev_map aux [] l opt_rev_map aux [] l
let remove_false l = let remove_false l =
let aux = function let aux = function
| Comb(Not, [True]) -> None | Comb(Not, [True]) -> None
| f -> Some f | f -> Some f
in in
opt_rev_map aux [] l opt_rev_map aux [] l
let make_not f = make Not [f] let make_not f = make Not [f]
let make_and l = let make_and l =
let l' = remove_true (flatten And [] l) in let l' = remove_true (flatten And [] l) in
if List.exists ((=) f_false) l' then if List.exists ((=) f_false) l' then
f_false f_false
else else
make And l' make And l'
let make_or l = let make_or l =
let l' = remove_false (flatten Or [] l) in let l' = remove_false (flatten Or [] l) in
if List.exists ((=) f_true) l' then if List.exists ((=) f_true) l' then
f_true f_true
else match l' with else match l' with
| [] -> raise Empty_Or | [] -> raise Empty_Or
| [a] -> a | [a] -> a
@ -110,19 +110,19 @@ module Make (F : Formula_intf.S) = struct
| Comb (And, l) -> sform_list [] l (k %% make_and) | Comb (And, l) -> sform_list [] l (k %% make_and)
| Comb (Or, l) -> sform_list [] l (k %% make_or) | Comb (Or, l) -> sform_list [] l (k %% make_or)
| Comb (Imp, [f1; f2]) -> | 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])]) -> | 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 | Comb ((Imp | Not), _) -> assert false
| Lit _ -> k f | Lit _ -> k f
and sform_list acc l k = match l with and sform_list acc l k = match l with
| [] -> k acc | [] -> k acc
| f :: tail -> | 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 and sform_list_not acc l k = match l with
| [] -> k acc | [] -> k acc
| f :: tail -> | 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 ( @@ ) l1 l2 = List.rev_append l1 l2
let ( @ ) = `Use_rev_append_instead (* prevent use of non-tailrec append *) let ( @ ) = `Use_rev_append_instead (* prevent use of non-tailrec append *)

8
util/either.ml
View file

@ -5,12 +5,12 @@ Copyright 2014 Simon Cruanes
*) *)
type ('a, 'b) t = type ('a, 'b) t =
| Left of 'a | Left of 'a
| Right of 'b | Right of 'b
let mk_left a = Left a let mk_left a = Left a
let mk_right b = Right b let mk_right b = Right b
let destruct e f_left f_right = match e with let destruct e f_left f_right = match e with
| Left a -> f_left a | Left a -> f_left a
| Right b -> f_right b | Right b -> f_right b

6
util/either.mli
View file

@ -5,11 +5,11 @@ Copyright 2014 Simon Cruanes
*) *)
type ('a, 'b) t = type ('a, 'b) t =
| Left of 'a | Left of 'a
| Right of 'b | Right of 'b
val mk_left : 'a -> ('a, 'b) t val mk_left : 'a -> ('a, 'b) t
val mk_right : 'b -> ('a, 'b) t val mk_right : 'b -> ('a, 'b) t
val destruct : ('a, 'b) t -> val destruct : ('a, 'b) t ->
('a -> 'c) -> ('b -> 'c) -> 'c ('a -> 'c) -> ('b -> 'c) -> 'c

72
util/sat_solve.ml
View file

@ -223,43 +223,43 @@ let main () =
print_cnf cnf; print_cnf cnf;
match !solver with match !solver with
| Smt -> | Smt ->
Smt.assume cnf; Smt.assume cnf;
let res = Smt.solve () in let res = Smt.solve () in
Gc.delete_alarm al; Gc.delete_alarm al;
begin match res with begin match res with
| Smt.Sat -> | Smt.Sat ->
print "Sat (%f)" (Sys.time ()); print "Sat (%f)" (Sys.time ());
if !p_check then if !p_check then
if not (List.for_all (List.exists Smt.eval) cnf) then if not (List.for_all (List.exists Smt.eval) cnf) then
raise Incorrect_model raise Incorrect_model
| Smt.Unsat -> | Smt.Unsat ->
print "Unsat (%f)" (Sys.time ()); print "Unsat (%f)" (Sys.time ());
if !p_check then begin if !p_check then begin
let p = Smt.get_proof () in let p = Smt.get_proof () in
print_proof p; print_proof p;
if !p_unsat_core then if !p_unsat_core then
print_unsat_core (Smt.unsat_core p) print_unsat_core (Smt.unsat_core p)
end end
end end
| Mcsat -> | Mcsat ->
Mcsat.assume cnf; Mcsat.assume cnf;
let res = Mcsat.solve () in let res = Mcsat.solve () in
Gc.delete_alarm al; Gc.delete_alarm al;
begin match res with begin match res with
| Mcsat.Sat -> | Mcsat.Sat ->
print "Sat (%f)" (Sys.time ()); print "Sat (%f)" (Sys.time ());
if !p_check then if !p_check then
if not (List.for_all (List.exists Mcsat.eval) cnf) then if not (List.for_all (List.exists Mcsat.eval) cnf) then
raise Incorrect_model raise Incorrect_model
| Mcsat.Unsat -> | Mcsat.Unsat ->
print "Unsat (%f)" (Sys.time ()); print "Unsat (%f)" (Sys.time ());
if !p_check then begin if !p_check then begin
let p = Mcsat.get_proof () in let p = Mcsat.get_proof () in
print_mcproof p; print_mcproof p;
if !p_unsat_core then if !p_unsat_core then
print_mc_unsat_core (Mcsat.unsat_core p) print_mc_unsat_core (Mcsat.unsat_core p)
end end
end end
let () = let () =
try try

4
util/smtlib/lexsmtlib.mll
View file

@ -1,5 +1,5 @@
{ {
(* auto-generated by gt *) (* auto-generated by gt *)
open Parsesmtlib;; open Parsesmtlib;;
} }
@ -45,4 +45,4 @@ rule token = parse
| ( '0' | ['1'-'9'] ['0'-'9']* ) '.' ['0'-'9']+ as str { DECIMAL(str) } | ( '0' | ['1'-'9'] ['0'-'9']* ) '.' ['0'-'9']+ as str { DECIMAL(str) }
| eof { EOF } | eof { EOF }
| _ {failwith((Lexing.lexeme lexbuf) ^ | _ {failwith((Lexing.lexeme lexbuf) ^
": lexing error on line "^(string_of_int !Smtlib_util.line))}{} ": lexing error on line "^(string_of_int !Smtlib_util.line))}{}

404
util/smtlib/parsesmtlib.mly
View file

@ -1,9 +1,9 @@
%{ %{
(* auto-generated by gt *) (* auto-generated by gt *)
open Smtlib_syntax;; open Smtlib_syntax;;
let parse_error s = let parse_error s =
print_string s; print_string s;
print_string " on line "; print_string " on line ";
print_int !Smtlib_util.line; print_int !Smtlib_util.line;
print_string "\n";; 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 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 <string> ASCIIWOR BINARY DECIMAL HEXADECIMAL KEYWORD NUMERAL STRINGLIT SYMBOL %token <string> ASCIIWOR BINARY DECIMAL HEXADECIMAL KEYWORD NUMERAL STRINGLIT SYMBOL
%type <Smtlib_syntax.commands option> main %type <Smtlib_syntax.commands option> main
%type <Smtlib_syntax.an_option> an_option %type <Smtlib_syntax.an_option> an_option
%type <Smtlib_syntax.attribute> attribute %type <Smtlib_syntax.attribute> attribute
%type <Smtlib_syntax.attributevalsexpr_attributevalue_sexpr5> attributevalsexpr_attributevalue_sexpr5 %type <Smtlib_syntax.attributevalsexpr_attributevalue_sexpr5> attributevalsexpr_attributevalue_sexpr5
%type <Smtlib_syntax.attributevalue> attributevalue %type <Smtlib_syntax.attributevalue> attributevalue
%type <Smtlib_syntax.command> command %type <Smtlib_syntax.command> command
%type <Smtlib_syntax.commanddeclarefun_command_sort13> commanddeclarefun_command_sort13 %type <Smtlib_syntax.commanddeclarefun_command_sort13> commanddeclarefun_command_sort13
%type <Smtlib_syntax.commanddefinefun_command_sortedvar15> commanddefinefun_command_sortedvar15 %type <Smtlib_syntax.commanddefinefun_command_sortedvar15> commanddefinefun_command_sortedvar15
%type <Smtlib_syntax.commanddefinesort_command_symbol11> commanddefinesort_command_symbol11 %type <Smtlib_syntax.commanddefinesort_command_symbol11> commanddefinesort_command_symbol11
%type <Smtlib_syntax.commandgetvalue_command_term24> commandgetvalue_command_term24 %type <Smtlib_syntax.commandgetvalue_command_term24> commandgetvalue_command_term24
%type <Smtlib_syntax.commands> commands %type <Smtlib_syntax.commands> commands
%type <Smtlib_syntax.commands_commands_command30> commands_commands_command30 %type <Smtlib_syntax.commands_commands_command30> commands_commands_command30
%type <Smtlib_syntax.identifier> identifier %type <Smtlib_syntax.identifier> identifier
%type <Smtlib_syntax.idunderscoresymnum_identifier_numeral33> idunderscoresymnum_identifier_numeral33 %type <Smtlib_syntax.idunderscoresymnum_identifier_numeral33> idunderscoresymnum_identifier_numeral33
%type <Smtlib_syntax.infoflag> infoflag %type <Smtlib_syntax.infoflag> infoflag
%type <Smtlib_syntax.qualidentifier> qualidentifier %type <Smtlib_syntax.qualidentifier> qualidentifier
%type <Smtlib_syntax.sexpr> sexpr %type <Smtlib_syntax.sexpr> sexpr
%type <Smtlib_syntax.sexprinparen_sexpr_sexpr41> sexprinparen_sexpr_sexpr41 %type <Smtlib_syntax.sexprinparen_sexpr_sexpr41> sexprinparen_sexpr_sexpr41
%type <Smtlib_syntax.sort> sort %type <Smtlib_syntax.sort> sort
%type <Smtlib_syntax.sortedvar> sortedvar %type <Smtlib_syntax.sortedvar> sortedvar
%type <Smtlib_syntax.sortidsortmulti_sort_sort44> sortidsortmulti_sort_sort44 %type <Smtlib_syntax.sortidsortmulti_sort_sort44> sortidsortmulti_sort_sort44
%type <Smtlib_syntax.specconstant> specconstant %type <Smtlib_syntax.specconstant> specconstant
%type <Smtlib_syntax.symbol> symbol %type <Smtlib_syntax.symbol> symbol
%type <Smtlib_syntax.term> term %type <Smtlib_syntax.term> term
%type <Smtlib_syntax.termexclimationpt_term_attribute64> termexclimationpt_term_attribute64 %type <Smtlib_syntax.termexclimationpt_term_attribute64> termexclimationpt_term_attribute64
%type <Smtlib_syntax.termexiststerm_term_sortedvar62> termexiststerm_term_sortedvar62 %type <Smtlib_syntax.termexiststerm_term_sortedvar62> termexiststerm_term_sortedvar62
%type <Smtlib_syntax.termforallterm_term_sortedvar60> termforallterm_term_sortedvar60 %type <Smtlib_syntax.termforallterm_term_sortedvar60> termforallterm_term_sortedvar60
%type <Smtlib_syntax.termletterm_term_varbinding58> termletterm_term_varbinding58 %type <Smtlib_syntax.termletterm_term_varbinding58> termletterm_term_varbinding58
%type <Smtlib_syntax.termqualidterm_term_term56> termqualidterm_term_term56 %type <Smtlib_syntax.termqualidterm_term_term56> termqualidterm_term_term56
%type <Smtlib_syntax.varbinding> varbinding %type <Smtlib_syntax.varbinding> varbinding
%type <Smtlib_util.pd> cur_position %type <Smtlib_util.pd> cur_position
%% %%
main: main:
| commands { Some($1) } | commands { Some($1) }
| EOF { None } | EOF { None }
cur_position: cur_position:
| { Smtlib_util.cur_pd() } | { Smtlib_util.cur_pd() }
an_option: an_option:
| attribute { AnOptionAttribute(pd_attribute $1, $1) } | attribute { AnOptionAttribute(pd_attribute $1, $1) }
attribute: attribute:
| cur_position KEYWORD { AttributeKeyword($1, $2) } | cur_position KEYWORD { AttributeKeyword($1, $2) }
attribute: attribute:
| cur_position KEYWORD attributevalue { AttributeKeywordValue($1, $2, $3) } | cur_position KEYWORD attributevalue { AttributeKeywordValue($1, $2, $3) }
attributevalue: attributevalue:
| specconstant { AttributeValSpecConst(pd_specconstant $1, $1) } | specconstant { AttributeValSpecConst(pd_specconstant $1, $1) }
attributevalue: attributevalue:
| symbol { AttributeValSymbol(pd_symbol $1, $1) } | symbol { AttributeValSymbol(pd_symbol $1, $1) }
attributevalue: attributevalue:
| cur_position LPAREN attributevalsexpr_attributevalue_sexpr5 RPAREN { AttributeValSexpr($1, $3) } | cur_position LPAREN attributevalsexpr_attributevalue_sexpr5 RPAREN { AttributeValSexpr($1, $3) }
command: command:
| cur_position LPAREN SETLOGIC symbol RPAREN { CommandSetLogic($1, $4) } | cur_position LPAREN SETLOGIC symbol RPAREN { CommandSetLogic($1, $4) }
command: command:
| cur_position LPAREN SETOPTION an_option RPAREN { CommandSetOption($1, $4) } | cur_position LPAREN SETOPTION an_option RPAREN { CommandSetOption($1, $4) }
command: command:
| cur_position LPAREN SETINFO attribute RPAREN { CommandSetInfo($1, $4) } | cur_position LPAREN SETINFO attribute RPAREN { CommandSetInfo($1, $4) }
command: command:
| cur_position LPAREN DECLARESORT symbol NUMERAL RPAREN { CommandDeclareSort($1, $4, $5) } | cur_position LPAREN DECLARESORT symbol NUMERAL RPAREN { CommandDeclareSort($1, $4, $5) }
command: command:
| cur_position LPAREN DEFINESORT symbol LPAREN commanddefinesort_command_symbol11 RPAREN sort RPAREN { CommandDefineSort($1, $4, $6, $8) } | cur_position LPAREN DEFINESORT symbol LPAREN commanddefinesort_command_symbol11 RPAREN sort RPAREN { CommandDefineSort($1, $4, $6, $8) }
command: command:
| cur_position LPAREN DECLAREFUN symbol LPAREN commanddeclarefun_command_sort13 RPAREN sort RPAREN { CommandDeclareFun($1, $4, $6, $8) } | cur_position LPAREN DECLAREFUN symbol LPAREN commanddeclarefun_command_sort13 RPAREN sort RPAREN { CommandDeclareFun($1, $4, $6, $8) }
command: command:
| cur_position LPAREN DEFINEFUN symbol LPAREN commanddefinefun_command_sortedvar15 RPAREN sort term RPAREN { CommandDefineFun($1, $4, $6, $8, $9) } | cur_position LPAREN DEFINEFUN symbol LPAREN commanddefinefun_command_sortedvar15 RPAREN sort term RPAREN { CommandDefineFun($1, $4, $6, $8, $9) }
command: command:
| cur_position LPAREN PUSH NUMERAL RPAREN { CommandPush($1, $4) } | cur_position LPAREN PUSH NUMERAL RPAREN { CommandPush($1, $4) }
command: command:
| cur_position LPAREN POP NUMERAL RPAREN { CommandPop($1, $4) } | cur_position LPAREN POP NUMERAL RPAREN { CommandPop($1, $4) }
command: command:
| cur_position LPAREN ASSERT term RPAREN { CommandAssert($1, $4) } | cur_position LPAREN ASSERT term RPAREN { CommandAssert($1, $4) }
command: command:
| cur_position LPAREN CHECKSAT RPAREN { CommandCheckSat($1) } | cur_position LPAREN CHECKSAT RPAREN { CommandCheckSat($1) }
command: command:
| cur_position LPAREN GETASSERT RPAREN { CommandGetAssert($1) } | cur_position LPAREN GETASSERT RPAREN { CommandGetAssert($1) }
command: command:
| cur_position LPAREN GETPROOF RPAREN { CommandGetProof($1) } | cur_position LPAREN GETPROOF RPAREN { CommandGetProof($1) }
command: command:
| cur_position LPAREN GETUNSATCORE RPAREN { CommandGetUnsatCore($1) } | cur_position LPAREN GETUNSATCORE RPAREN { CommandGetUnsatCore($1) }
command: command:
| cur_position LPAREN GETVALUE LPAREN commandgetvalue_command_term24 RPAREN RPAREN { CommandGetValue($1, $5) } | cur_position LPAREN GETVALUE LPAREN commandgetvalue_command_term24 RPAREN RPAREN { CommandGetValue($1, $5) }
command: command:
| cur_position LPAREN GETASSIGN RPAREN { CommandGetAssign($1) } | cur_position LPAREN GETASSIGN RPAREN { CommandGetAssign($1) }
command: command:
| cur_position LPAREN GETOPTION KEYWORD RPAREN { CommandGetOption($1, $4) } | cur_position LPAREN GETOPTION KEYWORD RPAREN { CommandGetOption($1, $4) }
command: command:
| cur_position LPAREN GETINFO infoflag RPAREN { CommandGetInfo($1, $4) } | cur_position LPAREN GETINFO infoflag RPAREN { CommandGetInfo($1, $4) }
command: command:
| cur_position LPAREN EXIT RPAREN { CommandExit($1) } | cur_position LPAREN EXIT RPAREN { CommandExit($1) }
commands: commands:
| commands_commands_command30 { Commands(pd_commands_commands_command30 $1, $1) } | commands_commands_command30 { Commands(pd_commands_commands_command30 $1, $1) }
identifier: identifier:
| symbol { IdSymbol(pd_symbol $1, $1) } | symbol { IdSymbol(pd_symbol $1, $1) }
identifier: identifier:
| cur_position LPAREN UNDERSCORE symbol idunderscoresymnum_identifier_numeral33 RPAREN { IdUnderscoreSymNum($1, $4, $5) } | cur_position LPAREN UNDERSCORE symbol idunderscoresymnum_identifier_numeral33 RPAREN { IdUnderscoreSymNum($1, $4, $5) }
infoflag: infoflag:
| cur_position KEYWORD { InfoFlagKeyword($1, $2) } | cur_position KEYWORD { InfoFlagKeyword($1, $2) }
qualidentifier: qualidentifier:
| identifier { QualIdentifierId(pd_identifier $1, $1) } | identifier { QualIdentifierId(pd_identifier $1, $1) }
qualidentifier: qualidentifier:
| cur_position LPAREN AS identifier sort RPAREN { QualIdentifierAs($1, $4, $5) } | cur_position LPAREN AS identifier sort RPAREN { QualIdentifierAs($1, $4, $5) }
sexpr: sexpr:
| specconstant { SexprSpecConst(pd_specconstant $1, $1) } | specconstant { SexprSpecConst(pd_specconstant $1, $1) }
sexpr: sexpr:
| symbol { SexprSymbol(pd_symbol $1, $1) } | symbol { SexprSymbol(pd_symbol $1, $1) }
sexpr: sexpr:
| cur_position KEYWORD { SexprKeyword($1, $2) } | cur_position KEYWORD { SexprKeyword($1, $2) }
sexpr: sexpr:
| cur_position LPAREN sexprinparen_sexpr_sexpr41 RPAREN { SexprInParen($1, $3) } | cur_position LPAREN sexprinparen_sexpr_sexpr41 RPAREN { SexprInParen($1, $3) }
sort: sort:
| identifier { SortIdentifier(pd_identifier $1, $1) } | identifier { SortIdentifier(pd_identifier $1, $1) }
sort: sort:
| cur_position LPAREN identifier sortidsortmulti_sort_sort44 RPAREN { SortIdSortMulti($1, $3, $4) } | cur_position LPAREN identifier sortidsortmulti_sort_sort44 RPAREN { SortIdSortMulti($1, $3, $4) }
sortedvar: sortedvar:
| cur_position LPAREN symbol sort RPAREN { SortedVarSymSort($1, $3, $4) } | cur_position LPAREN symbol sort RPAREN { SortedVarSymSort($1, $3, $4) }
specconstant: specconstant:
| cur_position DECIMAL { SpecConstsDec($1, $2) } | cur_position DECIMAL { SpecConstsDec($1, $2) }
specconstant: specconstant:
| cur_position NUMERAL { SpecConstNum($1, $2) } | cur_position NUMERAL { SpecConstNum($1, $2) }
specconstant: specconstant:
| cur_position STRINGLIT { SpecConstString($1, $2) } | cur_position STRINGLIT { SpecConstString($1, $2) }
specconstant: specconstant:
| cur_position HEXADECIMAL { SpecConstsHex($1, $2) } | cur_position HEXADECIMAL { SpecConstsHex($1, $2) }
specconstant: specconstant:
| cur_position BINARY { SpecConstsBinary($1, $2) } | cur_position BINARY { SpecConstsBinary($1, $2) }
symbol: symbol:
| cur_position SYMBOL { Symbol($1, $2) } | cur_position SYMBOL { Symbol($1, $2) }
symbol: symbol:
| cur_position ASCIIWOR { SymbolWithOr($1, $2) } | cur_position ASCIIWOR { SymbolWithOr($1, $2) }
term: term:
| specconstant { TermSpecConst(pd_specconstant $1, $1) } | specconstant { TermSpecConst(pd_specconstant $1, $1) }
term: term:
| qualidentifier { TermQualIdentifier(pd_qualidentifier $1, $1) } | qualidentifier { TermQualIdentifier(pd_qualidentifier $1, $1) }
term: term:
| cur_position LPAREN qualidentifier termqualidterm_term_term56 RPAREN { TermQualIdTerm($1, $3, $4) } | cur_position LPAREN qualidentifier termqualidterm_term_term56 RPAREN { TermQualIdTerm($1, $3, $4) }
term: term:
| cur_position LPAREN LET LPAREN termletterm_term_varbinding58 RPAREN term RPAREN { TermLetTerm($1, $5, $7) } | cur_position LPAREN LET LPAREN termletterm_term_varbinding58 RPAREN term RPAREN { TermLetTerm($1, $5, $7) }
term: term:
| cur_position LPAREN FORALL LPAREN termforallterm_term_sortedvar60 RPAREN term RPAREN { TermForAllTerm($1, $5, $7) } | cur_position LPAREN FORALL LPAREN termforallterm_term_sortedvar60 RPAREN term RPAREN { TermForAllTerm($1, $5, $7) }
term: term:
| cur_position LPAREN EXISTS LPAREN termexiststerm_term_sortedvar62 RPAREN term RPAREN { TermExistsTerm($1, $5, $7) } | cur_position LPAREN EXISTS LPAREN termexiststerm_term_sortedvar62 RPAREN term RPAREN { TermExistsTerm($1, $5, $7) }
term: term:
| cur_position LPAREN EXCLIMATIONPT term termexclimationpt_term_attribute64 RPAREN { TermExclimationPt($1, $4, $5) } | cur_position LPAREN EXCLIMATIONPT term termexclimationpt_term_attribute64 RPAREN { TermExclimationPt($1, $4, $5) }
varbinding: varbinding:
| cur_position LPAREN symbol term RPAREN { VarBindingSymTerm($1, $3, $4) } | cur_position LPAREN symbol term RPAREN { VarBindingSymTerm($1, $3, $4) }
termexclimationpt_term_attribute64: termexclimationpt_term_attribute64:
| attribute { (pd_attribute $1, ($1)::[]) } | attribute { (pd_attribute $1, ($1)::[]) }
termexclimationpt_term_attribute64: termexclimationpt_term_attribute64:
| attribute termexclimationpt_term_attribute64 { let (p, ( l1 )) = $2 in (pd_attribute $1, ($1)::(l1)) } | attribute termexclimationpt_term_attribute64 { let (p, ( l1 )) = $2 in (pd_attribute $1, ($1)::(l1)) }
termexiststerm_term_sortedvar62: termexiststerm_term_sortedvar62:
| sortedvar { (pd_sortedvar $1, ($1)::[]) } | sortedvar { (pd_sortedvar $1, ($1)::[]) }
termexiststerm_term_sortedvar62: termexiststerm_term_sortedvar62:
| sortedvar termexiststerm_term_sortedvar62 { let (p, ( l1 )) = $2 in (pd_sortedvar $1, ($1)::(l1)) } | sortedvar termexiststerm_term_sortedvar62 { let (p, ( l1 )) = $2 in (pd_sortedvar $1, ($1)::(l1)) }
termforallterm_term_sortedvar60: termforallterm_term_sortedvar60:
| sortedvar { (pd_sortedvar $1, ($1)::[]) } | sortedvar { (pd_sortedvar $1, ($1)::[]) }
termforallterm_term_sortedvar60: termforallterm_term_sortedvar60:
| sortedvar termforallterm_term_sortedvar60 { let (p, ( l1 )) = $2 in (pd_sortedvar $1, ($1)::(l1)) } | sortedvar termforallterm_term_sortedvar60 { let (p, ( l1 )) = $2 in (pd_sortedvar $1, ($1)::(l1)) }
termletterm_term_varbinding58: termletterm_term_varbinding58:
| varbinding { (pd_varbinding $1, ($1)::[]) } | varbinding { (pd_varbinding $1, ($1)::[]) }
termletterm_term_varbinding58: termletterm_term_varbinding58:
| varbinding termletterm_term_varbinding58 { let (p, ( l1 )) = $2 in (pd_varbinding $1, ($1)::(l1)) } | varbinding termletterm_term_varbinding58 { let (p, ( l1 )) = $2 in (pd_varbinding $1, ($1)::(l1)) }
termqualidterm_term_term56: termqualidterm_term_term56:
| term { (pd_term $1, ($1)::[]) } | term { (pd_term $1, ($1)::[]) }
termqualidterm_term_term56: termqualidterm_term_term56:
| term termqualidterm_term_term56 { let (p, ( l1 )) = $2 in (pd_term $1, ($1)::(l1)) } | term termqualidterm_term_term56 { let (p, ( l1 )) = $2 in (pd_term $1, ($1)::(l1)) }
sortidsortmulti_sort_sort44: sortidsortmulti_sort_sort44:
| sort { (pd_sort $1, ($1)::[]) } | sort { (pd_sort $1, ($1)::[]) }
sortidsortmulti_sort_sort44: sortidsortmulti_sort_sort44:
| sort sortidsortmulti_sort_sort44 { let (p, ( l1 )) = $2 in (pd_sort $1, ($1)::(l1)) } | sort sortidsortmulti_sort_sort44 { let (p, ( l1 )) = $2 in (pd_sort $1, ($1)::(l1)) }
sexprinparen_sexpr_sexpr41: sexprinparen_sexpr_sexpr41:
| cur_position { ($1, []) } | cur_position { ($1, []) }
sexprinparen_sexpr_sexpr41: sexprinparen_sexpr_sexpr41:
| sexpr sexprinparen_sexpr_sexpr41 { let (p, ( l1 )) = $2 in (pd_sexpr $1, ($1)::(l1)) } | sexpr sexprinparen_sexpr_sexpr41 { let (p, ( l1 )) = $2 in (pd_sexpr $1, ($1)::(l1)) }
idunderscoresymnum_identifier_numeral33: idunderscoresymnum_identifier_numeral33:
| cur_position NUMERAL { ($1, ($2)::[]) } | cur_position NUMERAL { ($1, ($2)::[]) }
idunderscoresymnum_identifier_numeral33: idunderscoresymnum_identifier_numeral33:
| cur_position NUMERAL idunderscoresymnum_identifier_numeral33 { let (p, ( l1 )) = $3 in ($1, ($2)::(l1)) } | cur_position NUMERAL idunderscoresymnum_identifier_numeral33 { let (p, ( l1 )) = $3 in ($1, ($2)::(l1)) }
commands_commands_command30: commands_commands_command30:
| cur_position { ($1, []) } | cur_position { ($1, []) }
commands_commands_command30: commands_commands_command30:
| command commands_commands_command30 { let (p, ( l1 )) = $2 in (pd_command $1, ($1)::(l1)) } | command commands_commands_command30 { let (p, ( l1 )) = $2 in (pd_command $1, ($1)::(l1)) }
commandgetvalue_command_term24: commandgetvalue_command_term24:
| term { (pd_term $1, ($1)::[]) } | term { (pd_term $1, ($1)::[]) }
commandgetvalue_command_term24: commandgetvalue_command_term24:
| term commandgetvalue_command_term24 { let (p, ( l1 )) = $2 in (pd_term $1, ($1)::(l1)) } | term commandgetvalue_command_term24 { let (p, ( l1 )) = $2 in (pd_term $1, ($1)::(l1)) }
commanddefinefun_command_sortedvar15: commanddefinefun_command_sortedvar15:
| cur_position { ($1, []) } | cur_position { ($1, []) }
commanddefinefun_command_sortedvar15: commanddefinefun_command_sortedvar15:
| sortedvar commanddefinefun_command_sortedvar15 { let (p, ( l1 )) = $2 in (pd_sortedvar $1, ($1)::(l1)) } | sortedvar commanddefinefun_command_sortedvar15 { let (p, ( l1 )) = $2 in (pd_sortedvar $1, ($1)::(l1)) }
commanddeclarefun_command_sort13: commanddeclarefun_command_sort13:
| cur_position { ($1, []) } | cur_position { ($1, []) }
commanddeclarefun_command_sort13: commanddeclarefun_command_sort13:
| sort commanddeclarefun_command_sort13 { let (p, ( l1 )) = $2 in (pd_sort $1, ($1)::(l1)) } | sort commanddeclarefun_command_sort13 { let (p, ( l1 )) = $2 in (pd_sort $1, ($1)::(l1)) }
commanddefinesort_command_symbol11: commanddefinesort_command_symbol11:
| cur_position { ($1, []) } | cur_position { ($1, []) }
commanddefinesort_command_symbol11: commanddefinesort_command_symbol11:
| symbol commanddefinesort_command_symbol11 { let (p, ( l1 )) = $2 in (pd_symbol $1, ($1)::(l1)) } | symbol commanddefinesort_command_symbol11 { let (p, ( l1 )) = $2 in (pd_symbol $1, ($1)::(l1)) }
attributevalsexpr_attributevalue_sexpr5: attributevalsexpr_attributevalue_sexpr5:
| cur_position { ($1, []) } | cur_position { ($1, []) }
attributevalsexpr_attributevalue_sexpr5: attributevalsexpr_attributevalue_sexpr5:
| sexpr attributevalsexpr_attributevalue_sexpr5 { let (p, ( l1 )) = $2 in (pd_sexpr $1, ($1)::(l1)) } | sexpr attributevalsexpr_attributevalue_sexpr5 { let (p, ( l1 )) = $2 in (pd_sexpr $1, ($1)::(l1)) }

130
util/smtlib/smtlib.ml
View file

@ -19,94 +19,94 @@ Hashtbl.add env "true" T.f_true;;
Hashtbl.add env "false" T.f_false;; Hashtbl.add env "false" T.f_false;;
let get_atom s = let get_atom s =
try try
Hashtbl.find env s Hashtbl.find env s
with Not_found -> with Not_found ->
let f = T.make_atom (F.fresh ()) in let f = T.make_atom (F.fresh ()) in
Hashtbl.add env s f; Hashtbl.add env s f;
f f
(* Term translation *) (* Term translation *)
let translate_const = function let translate_const = function
| SpecConstsDec(_, s) | SpecConstsDec(_, s)
| SpecConstNum(_, s) | SpecConstNum(_, s)
| SpecConstString(_, s) | SpecConstString(_, s)
| SpecConstsHex(_, s) | SpecConstsHex(_, s)
| SpecConstsBinary(_, s) -> s | SpecConstsBinary(_, s) -> s
let translate_symbol = function let translate_symbol = function
| Symbol(_, s) | Symbol(_, s)
| SymbolWithOr(_, s) -> s | SymbolWithOr(_, s) -> s
let translate_id = function let translate_id = function
| IdSymbol(_, s) -> translate_symbol s | IdSymbol(_, s) -> translate_symbol s
| IdUnderscoreSymNum(_, s, n) -> raise Incomplete_translation | IdUnderscoreSymNum(_, s, n) -> raise Incomplete_translation
let translate_qualid = function let translate_qualid = function
| QualIdentifierId(_, id) -> translate_id id | QualIdentifierId(_, id) -> translate_id id
| QualIdentifierAs(_, id, s) -> raise Incomplete_translation | QualIdentifierAs(_, id, s) -> raise Incomplete_translation
let left_assoc s f = function let left_assoc s f = function
| x :: r -> List.fold_left f x r | x :: r -> List.fold_left f x r
| _ -> raise (Bad_arity s) | _ -> raise (Bad_arity s)
let rec right_assoc s f = function let rec right_assoc s f = function
| [] -> raise (Bad_arity s) | [] -> raise (Bad_arity s)
| [x] -> x | [x] -> x
| x :: r -> f x (right_assoc s f r) | x :: r -> f x (right_assoc s f r)
let translate_atom = function let translate_atom = function
| TermSpecConst(_, const) -> translate_const const | TermSpecConst(_, const) -> translate_const const
| TermQualIdentifier(_, id) -> translate_qualid id | TermQualIdentifier(_, id) -> translate_qualid id
| _ -> raise Incomplete_translation | _ -> raise Incomplete_translation
let rec translate_term = function let rec translate_term = function
| TermQualIdTerm(_, f, (_, l)) -> | TermQualIdTerm(_, f, (_, l)) ->
begin match (translate_qualid f) with begin match (translate_qualid f) with
| "=" -> | "=" ->
begin match (List.map translate_atom l) with begin match (List.map translate_atom l) with
| [a; b] -> T.make_atom (F.mk_eq a b) | [a; b] -> T.make_atom (F.mk_eq a b)
| _ -> assert false | _ -> assert false
end end
| s -> | s ->
begin match s, (List.map translate_term l) with begin match s, (List.map translate_term l) with
(* CORE theory translation - 'distinct','ite' not yet implemented *) (* CORE theory translation - 'distinct','ite' not yet implemented *)
| "not", [e] -> T.make_not e | "not", [e] -> T.make_not e
| "not", _ -> raise (Bad_arity "not") | "not", _ -> raise (Bad_arity "not")
| "and", l -> T.make_and l | "and", l -> T.make_and l
| "or", l -> T.make_or l | "or", l -> T.make_or l
| "xor" as s, l -> left_assoc s T.make_xor l | "xor" as s, l -> left_assoc s T.make_xor l
| "=>" as s, l -> right_assoc s T.make_imply l | "=>" as s, l -> right_assoc s T.make_imply l
| _ -> | _ ->
Format.printf "unknown : %s@." s; Format.printf "unknown : %s@." s;
raise Unknown_command raise Unknown_command
end end
end end
| e -> (get_atom (translate_atom e)) | e -> (get_atom (translate_atom e))
(* Command Translation *) (* Command Translation *)
let translate_command = function let translate_command = function
| CommandDeclareFun(_, s, (_, []), _) -> | CommandDeclareFun(_, s, (_, []), _) ->
None None
| CommandAssert(_, t) -> | CommandAssert(_, t) ->
Some (translate_term t) Some (translate_term t)
| _ -> None | _ -> None
let rec translate_command_list acc = function let rec translate_command_list acc = function
| [] -> acc | [] -> acc
| c :: r -> | c :: r ->
begin match translate_command c with begin match translate_command c with
| None -> translate_command_list acc r | None -> translate_command_list acc r
| Some t -> translate_command_list (t :: acc) r | Some t -> translate_command_list (t :: acc) r
end end
let translate = function let translate = function
| Some Commands (_, (_, l)) -> List.rev (translate_command_list [] l) | Some Commands (_, (_, l)) -> List.rev (translate_command_list [] l)
| None -> [] | None -> []
let parse file = let parse file =
let f = open_in file in let f = open_in file in
let lexbuf = Lexing.from_channel f in let lexbuf = Lexing.from_channel f in
let commands = Parsesmtlib.main Lexsmtlib.token lexbuf in let commands = Parsesmtlib.main Lexsmtlib.token lexbuf in
close_in f; close_in f;
translate commands translate commands

16
util/smtlib/smtlib_syntax.mli
View file

@ -13,18 +13,18 @@ and attributevalue =
AttributeValSpecConst of Smtlib_util.pd * specconstant AttributeValSpecConst of Smtlib_util.pd * specconstant
| AttributeValSymbol of Smtlib_util.pd * symbol | AttributeValSymbol of Smtlib_util.pd * symbol
| AttributeValSexpr of Smtlib_util.pd * | AttributeValSexpr of Smtlib_util.pd *
attributevalsexpr_attributevalue_sexpr5 attributevalsexpr_attributevalue_sexpr5
and command = and command =
CommandSetLogic of Smtlib_util.pd * symbol CommandSetLogic of Smtlib_util.pd * symbol
| CommandSetOption of Smtlib_util.pd * an_option | CommandSetOption of Smtlib_util.pd * an_option
| CommandSetInfo of Smtlib_util.pd * attribute | CommandSetInfo of Smtlib_util.pd * attribute
| CommandDeclareSort of Smtlib_util.pd * symbol * string | CommandDeclareSort of Smtlib_util.pd * symbol * string
| CommandDefineSort of Smtlib_util.pd * symbol * | CommandDefineSort of Smtlib_util.pd * symbol *
commanddefinesort_command_symbol11 * sort commanddefinesort_command_symbol11 * sort
| CommandDeclareFun of Smtlib_util.pd * symbol * | CommandDeclareFun of Smtlib_util.pd * symbol *
commanddeclarefun_command_sort13 * sort commanddeclarefun_command_sort13 * sort
| CommandDefineFun of Smtlib_util.pd * symbol * | CommandDefineFun of Smtlib_util.pd * symbol *
commanddefinefun_command_sortedvar15 * sort * term commanddefinefun_command_sortedvar15 * sort * term
| CommandPush of Smtlib_util.pd * string | CommandPush of Smtlib_util.pd * string
| CommandPop of Smtlib_util.pd * string | CommandPop of Smtlib_util.pd * string
| CommandAssert of Smtlib_util.pd * term | CommandAssert of Smtlib_util.pd * term
@ -41,7 +41,7 @@ and commands = Commands of Smtlib_util.pd * commands_commands_command30
and identifier = and identifier =
IdSymbol of Smtlib_util.pd * symbol IdSymbol of Smtlib_util.pd * symbol
| IdUnderscoreSymNum 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 infoflag = InfoFlagKeyword of Smtlib_util.pd * string
and qualidentifier = and qualidentifier =
QualIdentifierId of Smtlib_util.pd * identifier QualIdentifierId of Smtlib_util.pd * identifier
@ -54,7 +54,7 @@ and sexpr =
and sort = and sort =
SortIdentifier of Smtlib_util.pd * identifier SortIdentifier of Smtlib_util.pd * identifier
| SortIdSortMulti 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 sortedvar = SortedVarSymSort of Smtlib_util.pd * symbol * sort
and specconstant = and specconstant =
SpecConstsDec of Smtlib_util.pd * string SpecConstsDec of Smtlib_util.pd * string
@ -69,12 +69,12 @@ and term =
TermSpecConst of Smtlib_util.pd * specconstant TermSpecConst of Smtlib_util.pd * specconstant
| TermQualIdentifier of Smtlib_util.pd * qualidentifier | TermQualIdentifier of Smtlib_util.pd * qualidentifier
| TermQualIdTerm 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 | TermLetTerm of Smtlib_util.pd * termletterm_term_varbinding58 * term
| TermForAllTerm of Smtlib_util.pd * termforallterm_term_sortedvar60 * term | TermForAllTerm of Smtlib_util.pd * termforallterm_term_sortedvar60 * term
| TermExistsTerm of Smtlib_util.pd * termexiststerm_term_sortedvar62 * term | TermExistsTerm of Smtlib_util.pd * termexiststerm_term_sortedvar62 * term
| TermExclimationPt of Smtlib_util.pd * term * | TermExclimationPt of Smtlib_util.pd * term *
termexclimationpt_term_attribute64 termexclimationpt_term_attribute64
and varbinding = VarBindingSymTerm of Smtlib_util.pd * symbol * term and varbinding = VarBindingSymTerm of Smtlib_util.pd * symbol * term
and termexclimationpt_term_attribute64 = Smtlib_util.pd * attribute list and termexclimationpt_term_attribute64 = Smtlib_util.pd * attribute list
and termexiststerm_term_sortedvar62 = Smtlib_util.pd * sortedvar list and termexiststerm_term_sortedvar62 = Smtlib_util.pd * sortedvar list