diff --git a/Makefile b/Makefile index 92f4bc5e..dd764e92 100644 --- a/Makefile +++ b/Makefile @@ -3,7 +3,7 @@ LOG=build.log COMP=ocamlbuild -log $(LOG) -use-ocamlfind FLAGS= -DOC=msat.docdir/index.html msat_smt.docdir/index.html +DOC=msat.docdir/index.html msat_sat.docdir/index.html msat_smt.docdir/index.html BIN=main.native TEST_BIN=tests/test_api.native @@ -12,11 +12,13 @@ NAME_BIN=msat NAME_CORE=msat NAME_SAT=msat_sat NAME_SMT=msat_smt +NAME_MCSAT=msat_mcsat LIB_CORE=$(addprefix $(NAME_CORE), .cma .cmxa .cmxs) LIB_SAT=$(addprefix $(NAME_SAT), .cma .cmxa .cmxs) LIB_SMT=$(addprefix $(NAME_SMT), .cma .cmxa .cmxs) -LIB=$(LIB_CORE) $(LIB_SAT) $(LIB_SMT) +LIB_MCSAT=$(addprefix $(NAME_MCSAT), .cma .cmxa .cmxs) +LIB=$(LIB_CORE) $(LIB_SAT) # $(LIB_SMT) $(LIB_MCSAT) all: lib test @@ -26,7 +28,7 @@ lib: doc: $(COMP) $(FLAGS) $(DOC) -bin: +bin: lib $(COMP) $(FLAGS) $(BIN) cp $(BIN) $(NAME_BIN) && rm $(BIN) diff --git a/_tags b/_tags index 47e25776..c1554407 100644 --- a/_tags +++ b/_tags @@ -11,6 +11,7 @@ true: inline(100), optimize(3), unbox_closures, unbox_closures_factor(20) : include : include : include +: include : include # Pack options @@ -18,10 +19,12 @@ true: inline(100), optimize(3), unbox_closures, unbox_closures_factor(20) : for-pack(Msat) : for-pack(Msat) : for-pack(Msat) + : for-pack(Msat_sat) : for-pack(Msat_smt) +: for-pack(Msat_mcsat) -# Bin options +# Testing dependencies : package(dolmen) : package(dolmen) diff --git a/src/main.ml b/src/main.ml index 6ea9a86e..e770c77b 100644 --- a/src/main.ml +++ b/src/main.ml @@ -4,10 +4,8 @@ Copyright 2014 Guillaume Bury Copyright 2014 Simon Cruanes *) -module F = Expr - (* -module T = Msat_smt.Cnf.S module Sat = Msat_sat.Sat.Make(struct end) + (* module Smt = Msat_smt.Smt.Make(struct end) module Mcsat = Msat_smt.Mcsat.Make(struct end) *) @@ -101,7 +99,7 @@ let argspec = Arg.align [ "[smhd] Sets the time limit for the sat solver"; "-u", Arg.Set p_unsat_core, " Prints the unsat-core explanation of the unsat proof (if used with -check)"; - "-v", Arg.Int (fun i -> Log.set_debug i), + "-v", Arg.Int (fun i -> Msat.Log.set_debug i), " Sets the debug verbose level"; ] @@ -117,17 +115,17 @@ let check () = let do_task (module S : Msat.External.S - with type St.formula = Expr.atom) s = + with type St.formula = Msat.Expr.atom) s = match s.Dolmen.Statement.descr with | Dolmen.Statement.Def (id, t) -> Type.new_def id t | Dolmen.Statement.Decl (id, t) -> Type.new_decl id t | Dolmen.Statement.Consequent t -> let f = Type.new_formula t in - let cnf = Expr.Formula.make_cnf f in + let cnf = Msat.Expr.Formula.make_cnf f in S.assume cnf | Dolmen.Statement.Antecedent t -> - let f = Expr.Formula.make_not @@ Type.new_formula t in - let cnf = Expr.Formula.make_cnf f in + let f = Msat.Expr.Formula.make_not @@ Type.new_formula t in + let cnf = Msat.Expr.Formula.make_cnf f in S.assume cnf | Dolmen.Statement.Prove -> begin match S.solve () with diff --git a/src/msat.mlpack b/src/msat.mlpack index b07295d9..4968dec6 100644 --- a/src/msat.mlpack +++ b/src/msat.mlpack @@ -18,12 +18,12 @@ Solver Mcsolver Solver_types -# Backends +# Proofs & Backends +Res Backend_intf Dot Dedukti # Auxiliary modules -Res +Expr Tseitin -Hashcons diff --git a/src/msat_sat.mlpack b/src/msat_sat.mlpack index 492570c2..dc169686 100644 --- a/src/msat_sat.mlpack +++ b/src/msat_sat.mlpack @@ -1,2 +1 @@ Sat - diff --git a/src/msat_smt.mlpack b/src/msat_smt.mlpack index cfd8b1ba..1bba977f 100644 --- a/src/msat_smt.mlpack +++ b/src/msat_smt.mlpack @@ -1,12 +1,3 @@ -Cc -Cnf -Explanation -Expr -ID -Literal -Mcsat Smt -Symbols -Term -Ty -Unionfind +Cc +Explanation diff --git a/src/sat/sat.ml b/src/sat/sat.ml index 448cecb4..07f948ee 100644 --- a/src/sat/sat.ml +++ b/src/sat/sat.ml @@ -4,92 +4,10 @@ Copyright 2014 Guillaume Bury Copyright 2014 Simon Cruanes *) -open Msat +module Make(Dummy : sig end) = + Msat.Solver.Make + (Msat.Expr.Atom) + (Msat.Solver.DummyTheory + (Msat.Expr.Atom)) + (struct end) -module FI = Formula_intf - -module Fsat = struct - - exception Bad_atom - - type t = int - type proof = unit - - let max_lit = max_int - let max_fresh = ref (-1) - let max_index = ref 0 - - let _make i = - if i <> 0 && (abs i) < max_lit then begin - max_index := max !max_index (abs i); - i - end else - raise Bad_atom - - let dummy = 0 - - let neg a = - a - let norm a = abs a, if a < 0 then FI.Negated else FI.Same_sign - let abs = abs - let sign i = i > 0 - let apply_sign b i = if b then i else neg i - let set_sign b i = if b then abs i else neg (abs i) - - let hash (a:int) = a land max_int - let equal (a:int) b = a=b - let compare (a:int) b = Pervasives.compare a b - - let make i = _make (2 * i) - - let fresh, iter = - let create () = - incr max_fresh; - _make (2 * !max_fresh + 1) - in - let iter: (t -> unit) -> unit = fun f -> - for j = 1 to !max_index do - f j - done - in - create, iter - - let print fmt a = - Format.fprintf fmt "%s%s%d" - (if a < 0 then "~" else "") - (if a mod 2 = 0 then "v" else "f") - ((abs a) / 2) - -end - -module Tseitin = Tseitin.Make(Fsat) - -module Make(Dummy : sig end) = struct - - module Tsat = Solver.DummyTheory(Fsat) - include Solver.Make(Fsat)(Tsat)(struct end) - - let print_atom = Fsat.print - let print_clause = St.print_clause - let print_proof out p = - let module Dot = Dot.Make(Proof)(struct - let clause_name c = St.(c.name) - let print_atom = St.print_atom - let lemma_info () = "()", None, [] - end) - in - Dot.print out p - - let print_dimacs_clause fmt l = - Format.fprintf fmt "%a0" (fun fmt l -> - List.iter (fun i -> Format.fprintf fmt "%d " i) l) l - - let print_dimacs fmt l = - let l = List.map (fun c -> - List.map (fun a -> a.St.lit) (Proof.to_list c)) l in - let n, m = List.fold_left (fun (n, m) c -> - let m' = List.fold_left (fun i j -> max i (abs j)) m c in - (n + 1, m')) (0, 0) l in - Format.fprintf fmt "p cnf %d %d@\n" n m; - List.iter (fun c -> Format.fprintf fmt "%a@\n" print_dimacs_clause c) l - -end diff --git a/src/sat/sat.mli b/src/sat/sat.mli index 06e4185b..cab12d63 100644 --- a/src/sat/sat.mli +++ b/src/sat/sat.mli @@ -6,59 +6,6 @@ Copyright 2014 Simon Cruanes open Msat -module Fsat : sig +module Make(Dummy : sig end) : Solver.S with type St.formula = Expr.Atom.t - include Formula_intf.S with type t = private int - - exception Bad_atom - (** Exception raised when a problem with atomic formula encoding is detected. *) - - val make : int -> t - (** Returns the literal corresponding to the integer. - @raise Bad_atom if given [0] as argument.*) - - val fresh : unit -> t - (** [new_atom ()] returns a fresh literal. - @raise Bad_atom if there are no more integer available to represent new atoms. *) - - val neg : t -> t - (** [neg a] returns the negation of a literal. Involutive, i.e [neg (neg a) = a]. *) - - val abs : t -> t - val sign : t -> bool - val apply_sign : bool -> t -> t - val set_sign : bool -> t -> t - (** Convenienc functions for manipulating literals. *) - - val hash : t -> int - val equal : t -> t -> bool - val compare : t -> t -> int - (** Usual hash and comparison functions. For now, directly uses - [Pervasives] and [Hashtbl] builtins. *) - - val iter : (t -> unit) -> unit - (** Allows iteration over all atoms created (even if unused). *) - -end - -module Tseitin : Tseitin.S with type atom = Fsat.t - -module Make(Dummy : sig end) : sig - (** Fonctor to make a pure SAT Solver module with built-in literals. *) - - include Solver.S with type St.formula = Fsat.t - - val print_atom : Format.formatter -> atom -> unit - (** Print the atom on the given formatter. *) - - val print_clause : Format.formatter -> St.clause -> unit - (** Print the clause on the given formatter. *) - - val print_proof : Format.formatter -> Proof.proof -> unit - (** Print the given proof in dot format. *) - - val print_dimacs : Format.formatter -> St.clause list -> unit - (** Prints a cnf in dimacs format on the given formatter *) - -end diff --git a/src/smt/ID.ml b/src/smt/ID.ml deleted file mode 100644 index fb0f64d4..00000000 --- a/src/smt/ID.ml +++ /dev/null @@ -1,39 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2016 Guillaume Bury -Copyright 2016 Simon Cruanes -*) - -type t = { - id: int; - name: string; -} - -let make = - let n = ref 0 in - fun name -> - let x = { id= !n; name; } in - incr n; - x - -let copy {name;_} = make name - -let to_string id = id.name - -let equal a b = a.id=b.id -let compare a b = Pervasives.compare a.id b.id -let hash a = a.id land max_int -let pp out a = Format.fprintf out "%s/%d" a.name a.id -let pp_name out a = Format.pp_print_string out a.name - -module AsKey = struct - type t_ = t - type t = t_ - let equal = equal - let compare = compare - let hash = hash -end - -module Map = Map.Make(AsKey) -module Set = Set.Make(AsKey) -module Tbl = Hashtbl.Make(AsKey) diff --git a/src/smt/ID.mli b/src/smt/ID.mli deleted file mode 100644 index f0ac869d..00000000 --- a/src/smt/ID.mli +++ /dev/null @@ -1,25 +0,0 @@ - -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2016 Guillaume Bury -Copyright 2016 Simon Cruanes -*) - -(** {1 Unique Identifiers} *) - -type t - -val make : string -> t -val copy : t -> t - -val to_string : t -> string - -val equal : t -> t -> bool -val compare : t -> t -> int -val hash : t -> int - -val pp_name : Format.formatter -> t -> unit - -module Map : Map.S with type key = t -module Set : Set.S with type elt = t -module Tbl : Hashtbl.S with type key = t diff --git a/src/smt/smt.ml b/src/smt/smt.ml index 10eafb4c..b42478fc 100644 --- a/src/smt/smt.ml +++ b/src/smt/smt.ml @@ -4,8 +4,6 @@ Copyright 2014 Guillaume Bury Copyright 2014 Simon Cruanes *) -module Fsmt = Expr - module Tsmt = struct module CC = Cc.Make(String) diff --git a/src/smt/symbols.ml b/src/smt/symbols.ml deleted file mode 100644 index c39e60ab..00000000 --- a/src/smt/symbols.ml +++ /dev/null @@ -1,62 +0,0 @@ -(**************************************************************************) -(* *) -(* Cubicle *) -(* Combining model checking algorithms and SMT solvers *) -(* *) -(* Sylvain Conchon and Alain Mebsout *) -(* Universite Paris-Sud 11 *) -(* *) -(* Copyright 2011. This file is distributed under the terms of the *) -(* Apache Software License version 2.0 *) -(* *) -(**************************************************************************) - -type name_kind = Constructor | Other - -type t = - | True - | False - | Name of ID.t * name_kind - | Var of ID.t - -let name ?(kind=Other) s = Name (s, kind) -let var s = Var s - -let compare_kind k1 k2 = match k1, k2 with - | Other, Other -> 0 - | Other, _ -> 1 - | _ , Other -> -1 - | Constructor, Constructor -> 0 - -let compare s1 s2 = match s1, s2 with - | Name (n1,k1), Name (n2,k2) -> - let c = compare_kind k1 k2 in - if c = 0 then ID.compare n1 n2 else c - | Name _, _ -> -1 - | _, Name _ -> 1 - | Var n1, Var n2 -> ID.compare n1 n2 - | Var _, _ -> -1 - | _ ,Var _ -> 1 - | _ -> Pervasives.compare s1 s2 - -let equal s1 s2 = compare s1 s2 = 0 - -let hash = function - | Name (n,_) -> ID.hash n * 19 - | Var n (*| Int n*) -> ID.hash n * 19 + 1 - | s -> Hashtbl.hash s - -let to_string = function - | Name (n,_) -> ID.to_string n - | Var x -> "*var* "^(ID.to_string x) - | True -> "true" - | False -> "false" - -let print fmt s = Format.fprintf fmt "%s" (to_string s) - -module Map = - Map.Make(struct type t' = t type t=t' let compare=compare end) - -module Set = - Set.Make(struct type t' = t type t=t' let compare=compare end) - diff --git a/src/smt/symbols.mli b/src/smt/symbols.mli deleted file mode 100644 index 17dd3e0b..00000000 --- a/src/smt/symbols.mli +++ /dev/null @@ -1,33 +0,0 @@ -(**************************************************************************) -(* *) -(* Cubicle *) -(* Combining model checking algorithms and SMT solvers *) -(* *) -(* Sylvain Conchon and Alain Mebsout *) -(* Universite Paris-Sud 11 *) -(* *) -(* Copyright 2011. This file is distributed under the terms of the *) -(* Apache Software License version 2.0 *) -(* *) -(**************************************************************************) - -type name_kind = Constructor | Other - -type t = - | True - | False - | Name of ID.t * name_kind - | Var of ID.t - -val name : ?kind:name_kind -> ID.t -> t -val var : ID.t -> t - -val equal : t -> t -> bool -val compare : t -> t -> int -val hash : t -> int - -val print : Format.formatter -> t -> unit - -module Map : Map.S with type key = t -module Set : Set.S with type elt = t - diff --git a/src/smt/term.ml b/src/smt/term.ml deleted file mode 100644 index 8a670468..00000000 --- a/src/smt/term.ml +++ /dev/null @@ -1,101 +0,0 @@ -(**************************************************************************) -(* *) -(* Cubicle *) -(* Combining model checking algorithms and SMT solvers *) -(* *) -(* Sylvain Conchon and Alain Mebsout *) -(* Universite Paris-Sud 11 *) -(* *) -(* Copyright 2011. This file is distributed under the terms of the *) -(* Apache Software License version 2.0 *) -(* *) -(**************************************************************************) - -open Msat - -module Sy = Symbols - -type view = { - head: head; - ty: Ty.t; - mutable tag: int; -} - -and head = - | App of Symbols.t * t list - | Ite of t * t * t - -and t = view - -module H = struct - type t = view - let equal t1 t2 = match t1.head, t2.head with - | App (f1,l1), App (f2,l2) -> - begin try - Sy.equal f1 f2 - && List.for_all2 (==) l1 l2 - && Ty.equal t1.ty t2.ty - with Invalid_argument _ -> - false - end - | Ite (a1,b1,c1), Ite (a2,b2,c2) -> - a1==a2 && b1==b2 && c1==c2 - | App _, Ite _ - | Ite _, App _ -> false - - let hash t = match t.head with - | Ite (a,b,c) -> - abs - (List.fold_left - (fun acc x-> acc*19 +x.tag) 17 [a;b;c]) - | App (f,l) -> - abs - (List.fold_left - (fun acc x-> acc*19 +x.tag) (Sy.hash f + Ty.hash t.ty) - l) - let set_id x tag = x.tag <- tag -end - -module T = Hashcons.Make(H) - -let view t = t -let head t = t.head - -let rec print fmt t = match t.head with - | Ite (a,b,c) -> - Format.fprintf fmt "(@[<2>ite@ %a@ %a@ %a@])" print a print b print c - | App (x, l) -> - match x, l with - | _, [] -> Format.fprintf fmt "%a" Sy.print x - | _, _ -> Format.fprintf fmt "%a(%a)" Sy.print x print_list l - -and print_list fmt = function - | [] -> () - | [t] -> print fmt t - | t::l -> Format.fprintf fmt "%a,%a" print t print_list l - -let compare t1 t2 = - let c = Pervasives.compare t2.tag t1.tag in - if c = 0 then c - else match t1.head, t2.head with - | App ((Sy.True | Sy.False), _), App ((Sy.True | Sy.False), _) -> c - | App ((Sy.True | Sy.False), _), _ -> -1 - | _, App ((Sy.True | Sy.False), _) -> 1 - | _,_ -> c - -let app s l ty = T.hashcons {head=App(s,l); ty=ty; tag= -1; } -let const s ty = app s [] ty -let ite a b c = T.hashcons {head=Ite (a,b,c); ty=b.ty; tag= -1; } - -let true_ = app (Sy.True) [] Ty.Tbool -let false_ = app (Sy.False) [] Ty.Tbool - -let equal t1 t2 = t1 == t2 - -let hash t = t.tag - -module Set = - Set.Make(struct type t' = t type t=t' let compare=compare end) - -module Map = - Map.Make(struct type t' = t type t=t' let compare=compare end) diff --git a/src/smt/term.mli b/src/smt/term.mli deleted file mode 100644 index 92defc96..00000000 --- a/src/smt/term.mli +++ /dev/null @@ -1,46 +0,0 @@ -(**************************************************************************) -(* *) -(* Cubicle *) -(* Combining model checking algorithms and SMT solvers *) -(* *) -(* Sylvain Conchon and Alain Mebsout *) -(* Universite Paris-Sud 11 *) -(* *) -(* Copyright 2011. This file is distributed under the terms of the *) -(* Apache Software License version 2.0 *) -(* *) -(**************************************************************************) - -open Msat - -type t - -type view = private { - head: head; - ty: Ty.t; - mutable tag: int; -} - -and head = - | App of Symbols.t * t list - | Ite of t * t * t - -val view : t -> view -val head : t -> head - -val app : Symbols.t -> t list -> Ty.t -> t -val const : Symbols.t -> Ty.t -> t -val ite : t -> t -> t -> t - -val true_ : t -val false_ : t - -val compare : t -> t -> int -val equal : t -> t -> bool -val hash : t -> int - -val print : Format.formatter -> t -> unit - -module Map : Map.S with type key = t -module Set : Set.S with type elt = t - diff --git a/src/smt/ty.ml b/src/smt/ty.ml deleted file mode 100644 index a3af5bd7..00000000 --- a/src/smt/ty.ml +++ /dev/null @@ -1,60 +0,0 @@ -(**************************************************************************) -(* *) -(* Cubicle *) -(* Combining model checking algorithms and SMT solvers *) -(* *) -(* Sylvain Conchon and Alain Mebsout *) -(* Universite Paris-Sud 11 *) -(* *) -(* Copyright 2011. This file is distributed under the terms of the *) -(* Apache Software License version 2.0 *) -(* *) -(**************************************************************************) - -open Msat - -type symbol = Symbols.t - -type t = - | Tbool - | Tabstract of ID.t - | Tsum of ID.t * symbol list - -let bool = Tbool -let abstract i = Tabstract i -let sum i l = Tsum (i, l) - -let hash t = - match t with - | Tabstract s -> ID.hash s - | Tsum (s, l) -> - let h = - List.fold_left - (fun h x -> 13 * h + Symbols.hash x) (ID.hash s) l - in - abs h - | _ -> Hashtbl.hash t - -let equal t1 t2 = - match t1, t2 with - | Tabstract s1, Tabstract s2 - | Tsum (s1, _), Tsum (s2, _) -> - ID.equal s1 s2 - | Tbool, Tbool -> true - | _ -> false - -let compare t1 t2 = - match t1, t2 with - | Tabstract s1, Tabstract s2 -> - ID.compare s1 s2 - | Tabstract _, _ -> -1 | _ , Tabstract _ -> 1 - | Tsum (s1, _), Tsum(s2, _) -> - ID.compare s1 s2 - | Tsum _, _ -> -1 | _ , Tsum _ -> 1 - | t1, t2 -> Pervasives.compare t1 t2 - -let print fmt ty = - match ty with - | Tbool -> Format.fprintf fmt "bool" - | Tabstract s -> Format.fprintf fmt "%s" (ID.to_string s) - | Tsum (s, _) -> Format.fprintf fmt "%s" (ID.to_string s) diff --git a/src/smt/ty.mli b/src/smt/ty.mli deleted file mode 100644 index 0c94cf71..00000000 --- a/src/smt/ty.mli +++ /dev/null @@ -1,29 +0,0 @@ -(**************************************************************************) -(* *) -(* Cubicle *) -(* Combining model checking algorithms and SMT solvers *) -(* *) -(* Sylvain Conchon and Alain Mebsout *) -(* Universite Paris-Sud 11 *) -(* *) -(* Copyright 2011. This file is distributed under the terms of the *) -(* Apache Software License version 2.0 *) -(* *) -(**************************************************************************) -open Msat - -type symbol = Symbols.t - -type t = - | Tbool - | Tabstract of ID.t - | Tsum of ID.t * symbol list - -val bool : t -val abstract : ID.t -> t -val sum : ID.t -> symbol list -> t - -val hash : t -> int -val equal : t -> t -> bool -val compare : t -> t -> int -val print : Format.formatter -> t -> unit diff --git a/src/util/expr.ml b/src/util/expr.ml index 752b55e7..9270d741 100644 --- a/src/util/expr.ml +++ b/src/util/expr.ml @@ -513,10 +513,10 @@ module Atom = struct let norm f = { f with sign = true }, - if f.sign then Msat.Formula_intf.Same_sign - else Msat.Formula_intf.Negated + if f.sign then Formula_intf.Same_sign + else Formula_intf.Negated end -module Formula = Msat.Tseitin.Make(Atom) +module Formula = Tseitin.Make(Atom) diff --git a/src/util/expr.mli b/src/util/expr.mli index 1f819b2c..229cf51b 100644 --- a/src/util/expr.mli +++ b/src/util/expr.mli @@ -290,6 +290,7 @@ end module Atom : sig type t = atom + type proof = unit (** Type alias *) val hash : t -> int @@ -300,6 +301,12 @@ module Atom : sig val print : Format.formatter -> t -> unit (** Printing functions *) + val dummy : atom + (** A dummy atom, different from any other atom. *) + + val fresh : unit -> atom + (** Create a fresh propositional atom. *) + val eq : term -> term -> atom (** Create an equality over two terms. The two given terms must have the same type [t], which must be different from {!Ty.prop} *) @@ -310,10 +317,10 @@ module Atom : sig val neg : atom -> atom (** Returns the negation of the given atom *) - val norm : atom -> atom * Msat.Formula_intf.negated + val norm : atom -> atom * Formula_intf.negated (** Normalization functions as required by msat. *) end -module Formula : Msat.Tseitin.S with type atom = atom +module Formula : Tseitin.S with type atom = atom diff --git a/src/util/type.ml b/src/util/type.ml index 5065c4be..5727a03e 100644 --- a/src/util/type.ml +++ b/src/util/type.ml @@ -14,33 +14,31 @@ module H = Hashtbl.Make(Id) type expect = | Nothing | Type - | Typed of Expr.ty + | Typed of Msat.Expr.ty (* The type returned after parsing an expression. *) type res = | Ttype - | Ty of Expr.ty - | Term of Expr.term - | Formula of Expr.Formula.t + | Ty of Msat.Expr.ty + | Term of Msat.Expr.term + | Formula of Msat.Expr.Formula.t (* The local environments used for type-checking. *) type env = { (* local variables (mostly quantified variables) *) - type_vars : (Expr.ttype Expr.id) M.t; - term_vars : (Expr.ty Expr.id) M.t; + type_vars : (Msat.Expr.ttype Msat.Expr.id) M.t; + term_vars : (Msat.Expr.ty Msat.Expr.id) M.t; (* Bound variables (through let constructions) *) - term_lets : Expr.term M.t; - prop_lets : Expr.Formula.t M.t; + term_lets : Msat.Expr.term M.t; + prop_lets : Msat.Expr.Formula.t M.t; (* Typing options *) expect : expect; } -type 'a typer = env -> Dolmen.Term.t -> 'a - (* Exceptions *) (* ************************************************************************ *) @@ -57,7 +55,7 @@ let _bad_arity s n t = raise (Typing_error ( Format.asprintf "Bad arity for operator '%s' (expected %d arguments)" s n, t)) let _type_mismatch t ty ty' ast = raise (Typing_error ( Format.asprintf "Type Mismatch: '%a' has type %a, but an expression of type %a was expected" - Expr.Print.term t Expr.Print.ty ty Expr.Print.ty ty', ast)) + Msat.Expr.Print.term t Msat.Expr.Print.ty ty Msat.Expr.Print.ty ty', ast)) let _fo_term s t = raise (Typing_error ( Format.asprintf "Let-bound variable '%a' is applied to terms" Id.print s, t)) @@ -74,28 +72,28 @@ let find_global name = (* Symbol declarations *) let decl_ty_cstr id c = if H.mem global_env id then - Log.debugf 0 "Symbol '%a' has already been defined, overwriting previous definition" + Msat.Log.debugf 0 "Symbol '%a' has already been defined, overwriting previous definition" (fun k -> k Id.print id); H.add global_env id (`Ty c); - Log.debugf 1 "New type constructor : %a" (fun k -> k Expr.Print.const_ttype c) + Msat.Log.debugf 1 "New type constructor : %a" (fun k -> k Msat.Expr.Print.const_ttype c) let decl_term id c = if H.mem global_env id then - Log.debugf 0 "Symbol '%a' has already been defined, overwriting previous definition" + Msat.Log.debugf 0 "Symbol '%a' has already been defined, overwriting previous definition" (fun k -> k Id.print id); H.add global_env id (`Term c); - Log.debugf 1 "New constant : %a" (fun k -> k Expr.Print.const_ty c) + Msat.Log.debugf 1 "New constant : %a" (fun k -> k Msat.Expr.Print.const_ty c) (* Symbol definitions *) let def_ty id args body = if H.mem global_env id then - Log.debugf 0 "Symbol '%a' has already been defined, overwriting previous definition" + Msat.Log.debugf 0 "Symbol '%a' has already been defined, overwriting previous definition" (fun k -> k Id.print id); H.add global_env id (`Ty_alias (args, body)) let def_term id ty_args args body = if H.mem global_env id then - Log.debugf 0 "Symbol '%a' has already been defined, overwriting previous definition" + Msat.Log.debugf 0 "Symbol '%a' has already been defined, overwriting previous definition" (fun k -> k Id.print id); H.add global_env id (`Term_alias (ty_args, args, body)) @@ -111,8 +109,6 @@ let empty_env ?(expect=Nothing) () = { expect; } -let expect env expect = { env with expect = expect } - (* Generate new fresh names for shadowed variables *) let new_name pre = let i = ref 0 in @@ -125,12 +121,12 @@ let new_term_name = new_name "term#" let add_type_var env id v = let v' = if M.mem id env.type_vars then - Expr.Id.ttype (new_ty_name ()) + Msat.Expr.Id.ttype (new_ty_name ()) else v in - Log.debugf 1 "New binding : %a -> %a" - (fun k -> k Id.print id Expr.Print.id_ttype v'); + Msat.Log.debugf 1 "New binding : %a -> %a" + (fun k -> k Id.print id Msat.Expr.Print.id_ttype v'); v', { env with type_vars = M.add id v' env.type_vars } let add_type_vars env l = @@ -142,12 +138,12 @@ let add_type_vars env l = let add_term_var env id v = let v' = if M.mem id env.type_vars then - Expr.Id.ty (new_term_name ()) Expr.(v.id_type) + Msat.Expr.Id.ty (new_term_name ()) Msat.Expr.(v.id_type) else v in - Log.debugf 1 "New binding : %a -> %a" - (fun k -> k Id.print id Expr.Print.id_ty v'); + Msat.Log.debugf 1 "New binding : %a -> %a" + (fun k -> k Id.print id Msat.Expr.Print.id_ty v'); v', { env with term_vars = M.add id v' env.term_vars } let find_var env name = @@ -162,13 +158,13 @@ let find_var env name = (* Add local bound variables to env *) let add_let_term env id t = - Log.debugf 1 "New let-binding : %s -> %a" - (fun k -> k id.Id.name Expr.Print.term t); + Msat.Log.debugf 1 "New let-binding : %s -> %a" + (fun k -> k id.Id.name Msat.Expr.Print.term t); { env with term_lets = M.add id t env.term_lets } let add_let_prop env id t = - Log.debugf 1 "New let-binding : %s -> %a" - (fun k -> k id.Id.name Expr.Formula.print t); + Msat.Log.debugf 1 "New let-binding : %s -> %a" + (fun k -> k id.Id.name Msat.Expr.Formula.print t); { env with prop_lets = M.add id t env.prop_lets } let find_let env name = @@ -184,20 +180,12 @@ let find_let env name = let pp_expect fmt = function | Nothing -> Format.fprintf fmt "<>" | Type -> Format.fprintf fmt "" - | Typed ty -> Expr.Print.ty fmt ty + | Typed ty -> Msat.Expr.Print.ty fmt ty let pp_map pp fmt map = M.iter (fun k v -> Format.fprintf fmt "%s->%a;" k.Id.name pp v) map -let pp_env fmt env = - Format.fprintf fmt "(%a) %a%a%a%a" - pp_expect env.expect - (pp_map Expr.Print.id_ttype) env.type_vars - (pp_map Expr.Print.id_ty) env.term_vars - (pp_map Expr.Print.term) env.term_lets - (pp_map Expr.Formula.print) env.prop_lets - (* Some helper functions *) (* ************************************************************************ *) @@ -224,41 +212,41 @@ let diagonal l = (* ************************************************************************ *) let arity f = - List.length Expr.(f.id_type.fun_vars) + - List.length Expr.(f.id_type.fun_args) + List.length Msat.Expr.(f.id_type.fun_vars) + + List.length Msat.Expr.(f.id_type.fun_args) let ty_apply env ast f args = try - Expr.Ty.apply f args - with Expr.Bad_ty_arity _ -> - _bad_arity Expr.(f.id_name) (arity f) ast + Msat.Expr.Ty.apply f args + with Msat.Expr.Bad_ty_arity _ -> + _bad_arity Msat.Expr.(f.id_name) (arity f) ast let term_apply env ast f ty_args t_args = try - Expr.Term.apply f ty_args t_args + Msat.Expr.Term.apply f ty_args t_args with - | Expr.Bad_arity _ -> - _bad_arity Expr.(f.id_name) (arity f) ast - | Expr.Type_mismatch (t, ty, ty') -> + | Msat.Expr.Bad_arity _ -> + _bad_arity Msat.Expr.(f.id_name) (arity f) ast + | Msat.Expr.Type_mismatch (t, ty, ty') -> _type_mismatch t ty ty' ast let ty_subst ast_term id args f_args body = - let aux s v ty = Expr.Subst.Id.bind v ty s in - match List.fold_left2 aux Expr.Subst.empty f_args args with + let aux s v ty = Msat.Expr.Subst.Id.bind v ty s in + match List.fold_left2 aux Msat.Expr.Subst.empty f_args args with | subst -> - Expr.Ty.subst subst body + Msat.Expr.Ty.subst subst body | exception Invalid_argument _ -> _bad_arity id.Id.name (List.length f_args) ast_term let term_subst ast_term id ty_args t_args f_ty_args f_t_args body = - let aux s v ty = Expr.Subst.Id.bind v ty s in - match List.fold_left2 aux Expr.Subst.empty f_ty_args ty_args with + let aux s v ty = Msat.Expr.Subst.Id.bind v ty s in + match List.fold_left2 aux Msat.Expr.Subst.empty f_ty_args ty_args with | ty_subst -> begin - let aux s v t = Expr.Subst.Id.bind v t s in - match List.fold_left2 aux Expr.Subst.empty f_t_args t_args with + let aux s v t = Msat.Expr.Subst.Id.bind v t s in + match List.fold_left2 aux Msat.Expr.Subst.empty f_t_args t_args with | t_subst -> - Expr.Term.subst ty_subst t_subst body + Msat.Expr.Term.subst ty_subst t_subst body | exception Invalid_argument _ -> _bad_arity id.Id.name (List.length f_ty_args + List.length f_t_args) ast_term end @@ -267,14 +255,14 @@ let term_subst ast_term id ty_args t_args f_ty_args f_t_args body = let make_eq ast_term a b = try - Expr.Formula.make_atom @@ Expr.Atom.eq a b - with Expr.Type_mismatch (t, ty, ty') -> + Msat.Expr.Formula.make_atom @@ Msat.Expr.Atom.eq a b + with Msat.Expr.Type_mismatch (t, ty, ty') -> _type_mismatch t ty ty' ast_term let make_pred ast_term p = try - Expr.Formula.make_atom @@ Expr.Atom.pred p - with Expr.Type_mismatch (t, ty, ty') -> + Msat.Expr.Formula.make_atom @@ Msat.Expr.Atom.pred p + with Msat.Expr.Type_mismatch (t, ty, ty') -> _type_mismatch t ty ty' ast_term let infer env s args = @@ -282,19 +270,19 @@ let infer env s args = | Nothing -> `Nothing | Type -> let n = List.length args in - let res = Expr.Id.ty_fun s.Id.name n in + let res = Msat.Expr.Id.ty_fun s.Id.name n in decl_ty_cstr s res; `Ty res | Typed ty -> let n = List.length args in let rec replicate acc n = - if n <= 0 then acc else replicate (Expr.Ty.base :: acc) (n - 1) + if n <= 0 then acc else replicate (Msat.Expr.Ty.base :: acc) (n - 1) in - let res = Expr.Id.term_fun s.Id.name [] (replicate [] n) ty in + let res = Msat.Expr.Id.term_fun s.Id.name [] (replicate [] n) ty in decl_term s res; `Term res -(* Expression parsing *) +(* Msat.Expression parsing *) (* ************************************************************************ *) let rec parse_expr (env : env) t = @@ -303,24 +291,24 @@ let rec parse_expr (env : env) t = (* Basic formulas *) | { Ast.term = Ast.App ({ Ast.term = Ast.Builtin Ast.True }, []) } | { Ast.term = Ast.Builtin Ast.True } -> - Formula Expr.Formula.f_true + Formula Msat.Expr.Formula.f_true | { Ast.term = Ast.App ({ Ast.term = Ast.Builtin Ast.False }, []) } | { Ast.term = Ast.Builtin Ast.False } -> - Formula Expr.Formula.f_false + Formula Msat.Expr.Formula.f_false | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.And}, l) } -> - Formula (Expr.Formula.make_and (List.map (parse_formula env) l)) + Formula (Msat.Expr.Formula.make_and (List.map (parse_formula env) l)) | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Or}, l) } -> - Formula (Expr.Formula.make_or (List.map (parse_formula env) l)) + Formula (Msat.Expr.Formula.make_or (List.map (parse_formula env) l)) | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Xor}, l) } as t -> begin match l with | [p; q] -> let f = parse_formula env p in let g = parse_formula env q in - Formula (Expr.Formula.make_not (Expr.Formula.make_equiv f g)) + Formula (Msat.Expr.Formula.make_not (Msat.Expr.Formula.make_equiv f g)) | _ -> _bad_arity "xor" 2 t end @@ -329,7 +317,7 @@ let rec parse_expr (env : env) t = | [p; q] -> let f = parse_formula env p in let g = parse_formula env q in - Formula (Expr.Formula.make_imply f g) + Formula (Msat.Expr.Formula.make_imply f g) | _ -> _bad_arity "=>" 2 t end @@ -338,14 +326,14 @@ let rec parse_expr (env : env) t = | [p; q] -> let f = parse_formula env p in let g = parse_formula env q in - Formula (Expr.Formula.make_equiv f g) + Formula (Msat.Expr.Formula.make_equiv f g) | _ -> _bad_arity "<=>" 2 t end | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Not}, l) } as t -> begin match l with | [p] -> - Formula (Expr.Formula.make_not (parse_formula env p)) + Formula (Msat.Expr.Formula.make_not (parse_formula env p)) | _ -> _bad_arity "not" 1 t end @@ -365,9 +353,9 @@ let rec parse_expr (env : env) t = let l' = List.map (parse_term env) args in let l'' = diagonal l' in Formula ( - Expr.Formula.make_and + Msat.Expr.Formula.make_and (List.map (fun (a, b) -> - Expr.Formula.make_not + Msat.Expr.Formula.make_not (make_eq t a b)) l'') ) @@ -387,15 +375,15 @@ let rec parse_expr (env : env) t = and parse_var env = function | { Ast.term = Ast.Colon ({ Ast.term = Ast.Symbol s }, e) } -> begin match parse_expr env e with - | Ttype -> `Ty (s, Expr.Id.ttype s.Id.name) - | Ty ty -> `Term (s, Expr.Id.ty s.Id.name ty) + | Ttype -> `Ty (s, Msat.Expr.Id.ttype s.Id.name) + | Ty ty -> `Term (s, Msat.Expr.Id.ty s.Id.name ty) | _ -> _expected "type (or Ttype)" e end | { Ast.term = Ast.Symbol s } -> begin match env.expect with | Nothing -> assert false - | Type -> `Ty (s, Expr.Id.ttype s.Id.name) - | Typed ty -> `Term (s, Expr.Id.ty s.Id.name ty) + | Type -> `Ty (s, Msat.Expr.Id.ttype s.Id.name) + | Typed ty -> `Term (s, Msat.Expr.Id.ty s.Id.name ty) end | t -> _expected "(typed) variable" t @@ -450,10 +438,10 @@ and parse_app env ast s args = | `Not_found -> begin match find_var env s with | `Ty f -> - if args = [] then Ty (Expr.Ty.of_id f) + if args = [] then Ty (Msat.Expr.Ty.of_id f) else _fo_term s ast | `Term f -> - if args = [] then Term (Expr.Term.of_id f) + if args = [] then Term (Msat.Expr.Term.of_id f) else _fo_term s ast | `Not_found -> begin match find_global s with @@ -481,7 +469,7 @@ and parse_app_ty env ast f args = Ty (ty_apply env ast f l) and parse_app_term env ast f args = - let n = List.length Expr.(f.id_type.fun_vars) in + let n = List.length Msat.Expr.(f.id_type.fun_vars) in let ty_l, t_l = take_drop n args in let ty_args = List.map (parse_ty env) ty_l in let t_args = List.map (parse_term env) t_l in @@ -504,13 +492,13 @@ and parse_ty env ast = | _ -> _expected "type" ast and parse_term env ast = - match parse_expr { env with expect = Typed Expr.Ty.base } ast with + match parse_expr { env with expect = Typed Msat.Expr.Ty.base } ast with | Term t -> t | _ -> _expected "term" ast and parse_formula env ast = - match parse_expr { env with expect = Typed Expr.Ty.prop } ast with - | Term t when Expr.(Ty.equal Ty.prop t.t_type) -> + match parse_expr { env with expect = Typed Msat.Expr.Ty.prop } ast with + | Term t when Msat.Expr.(Ty.equal Ty.prop t.t_type) -> make_pred ast t | Formula p -> p | _ -> _expected "formula" ast @@ -597,17 +585,17 @@ let rec parse_fun ty_args t_args env = function let new_decl id t = let env = empty_env () in - Log.debugf 5 "Typing declaration: %s : %a" + Msat.Log.debugf 5 "Typing declaration: %s : %a" (fun k -> k id.Id.name Ast.print t); begin match parse_sig env t with - | `Ty_cstr n -> decl_ty_cstr id (Expr.Id.ty_fun id.Id.name n) + | `Ty_cstr n -> decl_ty_cstr id (Msat.Expr.Id.ty_fun id.Id.name n) | `Fun_ty (vars, args, ret) -> - decl_term id (Expr.Id.term_fun id.Id.name vars args ret) + decl_term id (Msat.Expr.Id.term_fun id.Id.name vars args ret) end let new_def id t = let env = empty_env () in - Log.debugf 5 "Typing definition: %s = %a" + Msat.Log.debugf 5 "Typing definition: %s = %a" (fun k -> k id.Id.name Ast.print t); begin match parse_fun [] [] env t with | `Ty (ty_args, body) -> def_ty id ty_args body @@ -616,7 +604,7 @@ let new_def id t = let new_formula t = let env = empty_env () in - Log.debugf 5 "Typing top-level formula: %a" (fun k -> k Ast.print t); + Msat.Log.debugf 5 "Typing top-level formula: %a" (fun k -> k Ast.print t); let res = parse_formula env t in res diff --git a/src/util/type.mli b/src/util/type.mli index 26fd6ad6..a0414e29 100644 --- a/src/util/type.mli +++ b/src/util/type.mli @@ -11,5 +11,5 @@ val new_decl : Dolmen.Id.t -> Dolmen.Term.t -> unit val new_def : Dolmen.Id.t -> Dolmen.Term.t -> unit -val new_formula : Dolmen.Term.t -> Expr.Formula.t +val new_formula : Dolmen.Term.t -> Msat.Expr.Formula.t