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

[WIP] Some drastic cleanup of code

Browse source 
Some of these changes are to be reverted, among other the structure of
terms used for the instantiation of the pure SAT solver
This commit is contained in:
Guillaume Bury 2016-09-09 18:09:04 +02:00
parent 954892ac4a
commit 9d509241ad
21 changed files with 116 additions and 660 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
Makefile
View file

@ -3,7 +3,7 @@
LOG=build.log LOG=build.log
COMP=ocamlbuild -log $(LOG) -use-ocamlfind COMP=ocamlbuild -log $(LOG) -use-ocamlfind
FLAGS= 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 BIN=main.native
TEST_BIN=tests/test_api.native TEST_BIN=tests/test_api.native
@ -12,11 +12,13 @@ NAME_BIN=msat
NAME_CORE=msat NAME_CORE=msat
NAME_SAT=msat_sat NAME_SAT=msat_sat
NAME_SMT=msat_smt NAME_SMT=msat_smt
NAME_MCSAT=msat_mcsat
LIB_CORE=$(addprefix $(NAME_CORE), .cma .cmxa .cmxs) LIB_CORE=$(addprefix $(NAME_CORE), .cma .cmxa .cmxs)
LIB_SAT=$(addprefix $(NAME_SAT), .cma .cmxa .cmxs) LIB_SAT=$(addprefix $(NAME_SAT), .cma .cmxa .cmxs)
LIB_SMT=$(addprefix $(NAME_SMT), .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 all: lib test
@ -26,7 +28,7 @@ lib:
doc: doc:
$(COMP) $(FLAGS) $(DOC) $(COMP) $(FLAGS) $(DOC)
bin: bin: lib
$(COMP) $(FLAGS) $(BIN) $(COMP) $(FLAGS) $(BIN)
cp $(BIN) $(NAME_BIN) && rm $(BIN) cp $(BIN) $(NAME_BIN) && rm $(BIN)

5
_tags
View file

@ -11,6 +11,7 @@ true: inline(100), optimize(3), unbox_closures, unbox_closures_factor(20)
<src/backend>: include <src/backend>: include
<src/sat>: include <src/sat>: include
<src/smt>: include <src/smt>: include
<src/mcsat>: include
<src/util>: include <src/util>: include
# Pack options # Pack options
@ -18,10 +19,12 @@ true: inline(100), optimize(3), unbox_closures, unbox_closures_factor(20)
<src/solver/*.cmx>: for-pack(Msat) <src/solver/*.cmx>: for-pack(Msat)
<src/backend/*.cmx>: for-pack(Msat) <src/backend/*.cmx>: for-pack(Msat)
<src/util/*.cmx>: for-pack(Msat) <src/util/*.cmx>: for-pack(Msat)
<src/sat/*.cmx>: for-pack(Msat_sat) <src/sat/*.cmx>: for-pack(Msat_sat)
<src/smt/*.cmx>: for-pack(Msat_smt) <src/smt/*.cmx>: for-pack(Msat_smt)
<src/mcsat/*.cmx>: for-pack(Msat_mcsat)
# Bin options # Testing dependencies
<src/main.*>: package(dolmen) <src/main.*>: package(dolmen)
<src/util/type.*>: package(dolmen) <src/util/type.*>: package(dolmen)

14
src/main.ml
View file

@ -4,10 +4,8 @@ Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes Copyright 2014 Simon Cruanes
*) *)
module F = Expr
(*
module T = Msat_smt.Cnf.S
module Sat = Msat_sat.Sat.Make(struct end) module Sat = Msat_sat.Sat.Make(struct end)
(*
module Smt = Msat_smt.Smt.Make(struct end) module Smt = Msat_smt.Smt.Make(struct end)
module Mcsat = Msat_smt.Mcsat.Make(struct end) module Mcsat = Msat_smt.Mcsat.Make(struct end)
*) *)
@ -101,7 +99,7 @@ let argspec = Arg.align [
"<t>[smhd] Sets the time limit for the sat solver"; "<t>[smhd] Sets the time limit for the sat solver";
"-u", Arg.Set p_unsat_core, "-u", Arg.Set p_unsat_core,
" Prints the unsat-core explanation of the unsat proof (if used with -check)"; " 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),
"<lvl> Sets the debug verbose level"; "<lvl> Sets the debug verbose level";
] ]
@ -117,17 +115,17 @@ let check () =
let do_task let do_task
(module S : Msat.External.S (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 match s.Dolmen.Statement.descr with
| Dolmen.Statement.Def (id, t) -> Type.new_def id t | Dolmen.Statement.Def (id, t) -> Type.new_def id t
| Dolmen.Statement.Decl (id, t) -> Type.new_decl id t | Dolmen.Statement.Decl (id, t) -> Type.new_decl id t
| Dolmen.Statement.Consequent t -> | Dolmen.Statement.Consequent t ->
let f = Type.new_formula t in 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 S.assume cnf
| Dolmen.Statement.Antecedent t -> | Dolmen.Statement.Antecedent t ->
let f = Expr.Formula.make_not @@ Type.new_formula t in let f = Msat.Expr.Formula.make_not @@ 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 S.assume cnf
| Dolmen.Statement.Prove -> | Dolmen.Statement.Prove ->
begin match S.solve () with begin match S.solve () with

6
src/msat.mlpack
View file

@ -18,12 +18,12 @@ Solver
Mcsolver Mcsolver
Solver_types Solver_types
# Backends # Proofs & Backends
Res
Backend_intf Backend_intf
Dot Dot
Dedukti Dedukti
# Auxiliary modules # Auxiliary modules
Res Expr
Tseitin Tseitin
Hashcons

1
src/msat_sat.mlpack
View file

@ -1,2 +1 @@
Sat Sat

13
src/msat_smt.mlpack
View file

@ -1,12 +1,3 @@
Cc
Cnf
Explanation
Expr
ID
Literal
Mcsat
Smt Smt
Symbols Cc
Term Explanation
Ty
Unionfind

94
src/sat/sat.ml
View file

@ -4,92 +4,10 @@ Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes 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

55
src/sat/sat.mli
View file

@ -6,59 +6,6 @@ Copyright 2014 Simon Cruanes
open Msat 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

39
src/smt/ID.ml
View file

@ -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)

25
src/smt/ID.mli
View file

@ -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

2
src/smt/smt.ml
View file

@ -4,8 +4,6 @@ Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes Copyright 2014 Simon Cruanes
*) *)
module Fsmt = Expr
module Tsmt = struct module Tsmt = struct
module CC = Cc.Make(String) module CC = Cc.Make(String)

62
src/smt/symbols.ml
View file

@ -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)

33
src/smt/symbols.mli
View file

@ -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

101
src/smt/term.ml
View file

@ -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)

46
src/smt/term.mli
View file

@ -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

60
src/smt/ty.ml
View file

@ -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)

29
src/smt/ty.mli
View file

@ -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

6
src/util/expr.ml
View file

@ -513,10 +513,10 @@ module Atom = struct
let norm f = let norm f =
{ f with sign = true }, { f with sign = true },
if f.sign then Msat.Formula_intf.Same_sign if f.sign then Formula_intf.Same_sign
else Msat.Formula_intf.Negated else Formula_intf.Negated
end end
module Formula = Msat.Tseitin.Make(Atom) module Formula = Tseitin.Make(Atom)

11
src/util/expr.mli
View file

@ -290,6 +290,7 @@ end
module Atom : sig module Atom : sig
type t = atom type t = atom
type proof = unit
(** Type alias *) (** Type alias *)
val hash : t -> int val hash : t -> int
@ -300,6 +301,12 @@ module Atom : sig
val print : Format.formatter -> t -> unit val print : Format.formatter -> t -> unit
(** Printing functions *) (** 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 val eq : term -> term -> atom
(** Create an equality over two terms. The two given terms (** Create an equality over two terms. The two given terms
must have the same type [t], which must be different from {!Ty.prop} *) must have the same type [t], which must be different from {!Ty.prop} *)
@ -310,10 +317,10 @@ module Atom : sig
val neg : atom -> atom val neg : atom -> atom
(** Returns the negation of the given 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. *) (** Normalization functions as required by msat. *)
end end
module Formula : Msat.Tseitin.S with type atom = atom module Formula : Tseitin.S with type atom = atom

164
src/util/type.ml
View file

@ -14,33 +14,31 @@ module H = Hashtbl.Make(Id)
type expect = type expect =
| Nothing | Nothing
| Type | Type
| Typed of Expr.ty | Typed of Msat.Expr.ty
(* The type returned after parsing an expression. *) (* The type returned after parsing an expression. *)
type res = type res =
| Ttype | Ttype
| Ty of Expr.ty | Ty of Msat.Expr.ty
| Term of Expr.term | Term of Msat.Expr.term
| Formula of Expr.Formula.t | Formula of Msat.Expr.Formula.t
(* The local environments used for type-checking. *) (* The local environments used for type-checking. *)
type env = { type env = {
(* local variables (mostly quantified variables) *) (* local variables (mostly quantified variables) *)
type_vars : (Expr.ttype Expr.id) M.t; type_vars : (Msat.Expr.ttype Msat.Expr.id) M.t;
term_vars : (Expr.ty Expr.id) M.t; term_vars : (Msat.Expr.ty Msat.Expr.id) M.t;
(* Bound variables (through let constructions) *) (* Bound variables (through let constructions) *)
term_lets : Expr.term M.t; term_lets : Msat.Expr.term M.t;
prop_lets : Expr.Formula.t M.t; prop_lets : Msat.Expr.Formula.t M.t;
(* Typing options *) (* Typing options *)
expect : expect; expect : expect;
} }
type 'a typer = env -> Dolmen.Term.t -> 'a
(* Exceptions *) (* 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)) Format.asprintf "Bad arity for operator '%s' (expected %d arguments)" s n, t))
let _type_mismatch t ty ty' ast = raise (Typing_error ( 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" 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 ( let _fo_term s t = raise (Typing_error (
Format.asprintf "Let-bound variable '%a' is applied to terms" Id.print s, t)) Format.asprintf "Let-bound variable '%a' is applied to terms" Id.print s, t))
@ -74,28 +72,28 @@ let find_global name =
(* Symbol declarations *) (* Symbol declarations *)
let decl_ty_cstr id c = let decl_ty_cstr id c =
if H.mem global_env id then 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); (fun k -> k Id.print id);
H.add global_env id (`Ty c); 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 = let decl_term id c =
if H.mem global_env id then 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); (fun k -> k Id.print id);
H.add global_env id (`Term c); 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 *) (* Symbol definitions *)
let def_ty id args body = let def_ty id args body =
if H.mem global_env id then 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); (fun k -> k Id.print id);
H.add global_env id (`Ty_alias (args, body)) H.add global_env id (`Ty_alias (args, body))
let def_term id ty_args args body = let def_term id ty_args args body =
if H.mem global_env id then 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); (fun k -> k Id.print id);
H.add global_env id (`Term_alias (ty_args, args, body)) H.add global_env id (`Term_alias (ty_args, args, body))
@ -111,8 +109,6 @@ let empty_env ?(expect=Nothing) () = {
expect; expect;
} }
let expect env expect = { env with expect = expect }
(* Generate new fresh names for shadowed variables *) (* Generate new fresh names for shadowed variables *)
let new_name pre = let new_name pre =
let i = ref 0 in let i = ref 0 in
@ -125,12 +121,12 @@ let new_term_name = new_name "term#"
let add_type_var env id v = let add_type_var env id v =
let v' = let v' =
if M.mem id env.type_vars then if M.mem id env.type_vars then
Expr.Id.ttype (new_ty_name ()) Msat.Expr.Id.ttype (new_ty_name ())
else else
v v
in in
Log.debugf 1 "New binding : %a -> %a" Msat.Log.debugf 1 "New binding : %a -> %a"
(fun k -> k Id.print id Expr.Print.id_ttype v'); (fun k -> k Id.print id Msat.Expr.Print.id_ttype v');
v', { env with type_vars = M.add id v' env.type_vars } v', { env with type_vars = M.add id v' env.type_vars }
let add_type_vars env l = let add_type_vars env l =
@ -142,12 +138,12 @@ let add_type_vars env l =
let add_term_var env id v = let add_term_var env id v =
let v' = let v' =
if M.mem id env.type_vars then 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 else
v v
in in
Log.debugf 1 "New binding : %a -> %a" Msat.Log.debugf 1 "New binding : %a -> %a"
(fun k -> k Id.print id Expr.Print.id_ty v'); (fun k -> k Id.print id Msat.Expr.Print.id_ty v');
v', { env with term_vars = M.add id v' env.term_vars } v', { env with term_vars = M.add id v' env.term_vars }
let find_var env name = let find_var env name =
@ -162,13 +158,13 @@ let find_var env name =
(* Add local bound variables to env *) (* Add local bound variables to env *)
let add_let_term env id t = let add_let_term env id t =
Log.debugf 1 "New let-binding : %s -> %a" Msat.Log.debugf 1 "New let-binding : %s -> %a"
(fun k -> k id.Id.name Expr.Print.term t); (fun k -> k id.Id.name Msat.Expr.Print.term t);
{ env with term_lets = M.add id t env.term_lets } { env with term_lets = M.add id t env.term_lets }
let add_let_prop env id t = let add_let_prop env id t =
Log.debugf 1 "New let-binding : %s -> %a" Msat.Log.debugf 1 "New let-binding : %s -> %a"
(fun k -> k id.Id.name Expr.Formula.print t); (fun k -> k id.Id.name Msat.Expr.Formula.print t);
{ env with prop_lets = M.add id t env.prop_lets } { env with prop_lets = M.add id t env.prop_lets }
let find_let env name = let find_let env name =
@ -184,20 +180,12 @@ let find_let env name =
let pp_expect fmt = function let pp_expect fmt = function
| Nothing -> Format.fprintf fmt "<>" | Nothing -> Format.fprintf fmt "<>"
| Type -> Format.fprintf fmt "<tType>" | Type -> Format.fprintf fmt "<tType>"
| Typed ty -> Expr.Print.ty fmt ty | Typed ty -> Msat.Expr.Print.ty fmt ty
let pp_map pp fmt map = let pp_map pp fmt map =
M.iter (fun k v -> M.iter (fun k v ->
Format.fprintf fmt "%s->%a;" k.Id.name pp v) map 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 *) (* Some helper functions *)
(* ************************************************************************ *) (* ************************************************************************ *)
@ -224,41 +212,41 @@ let diagonal l =
(* ************************************************************************ *) (* ************************************************************************ *)
let arity f = let arity f =
List.length Expr.(f.id_type.fun_vars) + List.length Msat.Expr.(f.id_type.fun_vars) +
List.length Expr.(f.id_type.fun_args) List.length Msat.Expr.(f.id_type.fun_args)
let ty_apply env ast f args = let ty_apply env ast f args =
try try
Expr.Ty.apply f args Msat.Expr.Ty.apply f args
with Expr.Bad_ty_arity _ -> with Msat.Expr.Bad_ty_arity _ ->
_bad_arity Expr.(f.id_name) (arity f) ast _bad_arity Msat.Expr.(f.id_name) (arity f) ast
let term_apply env ast f ty_args t_args = let term_apply env ast f ty_args t_args =
try try
Expr.Term.apply f ty_args t_args Msat.Expr.Term.apply f ty_args t_args
with with
| Expr.Bad_arity _ -> | Msat.Expr.Bad_arity _ ->
_bad_arity Expr.(f.id_name) (arity f) ast _bad_arity Msat.Expr.(f.id_name) (arity f) ast
| Expr.Type_mismatch (t, ty, ty') -> | Msat.Expr.Type_mismatch (t, ty, ty') ->
_type_mismatch t ty ty' ast _type_mismatch t ty ty' ast
let ty_subst ast_term id args f_args body = let ty_subst ast_term id args f_args body =
let aux s v ty = Expr.Subst.Id.bind v ty s in let aux s v ty = Msat.Expr.Subst.Id.bind v ty s in
match List.fold_left2 aux Expr.Subst.empty f_args args with match List.fold_left2 aux Msat.Expr.Subst.empty f_args args with
| subst -> | subst ->
Expr.Ty.subst subst body Msat.Expr.Ty.subst subst body
| exception Invalid_argument _ -> | exception Invalid_argument _ ->
_bad_arity id.Id.name (List.length f_args) ast_term _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 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 let aux s v ty = Msat.Expr.Subst.Id.bind v ty s in
match List.fold_left2 aux Expr.Subst.empty f_ty_args ty_args with match List.fold_left2 aux Msat.Expr.Subst.empty f_ty_args ty_args with
| ty_subst -> | ty_subst ->
begin begin
let aux s v t = Expr.Subst.Id.bind v t s in let aux s v t = Msat.Expr.Subst.Id.bind v t s in
match List.fold_left2 aux Expr.Subst.empty f_t_args t_args with match List.fold_left2 aux Msat.Expr.Subst.empty f_t_args t_args with
| t_subst -> | t_subst ->
Expr.Term.subst ty_subst t_subst body Msat.Expr.Term.subst ty_subst t_subst body
| exception Invalid_argument _ -> | exception Invalid_argument _ ->
_bad_arity id.Id.name (List.length f_ty_args + List.length f_t_args) ast_term _bad_arity id.Id.name (List.length f_ty_args + List.length f_t_args) ast_term
end 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 = let make_eq ast_term a b =
try try
Expr.Formula.make_atom @@ Expr.Atom.eq a b Msat.Expr.Formula.make_atom @@ Msat.Expr.Atom.eq a b
with Expr.Type_mismatch (t, ty, ty') -> with Msat.Expr.Type_mismatch (t, ty, ty') ->
_type_mismatch t ty ty' ast_term _type_mismatch t ty ty' ast_term
let make_pred ast_term p = let make_pred ast_term p =
try try
Expr.Formula.make_atom @@ Expr.Atom.pred p Msat.Expr.Formula.make_atom @@ Msat.Expr.Atom.pred p
with Expr.Type_mismatch (t, ty, ty') -> with Msat.Expr.Type_mismatch (t, ty, ty') ->
_type_mismatch t ty ty' ast_term _type_mismatch t ty ty' ast_term
let infer env s args = let infer env s args =
@ -282,19 +270,19 @@ let infer env s args =
| Nothing -> `Nothing | Nothing -> `Nothing
| Type -> | Type ->
let n = List.length args in 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; decl_ty_cstr s res;
`Ty res `Ty res
| Typed ty -> | Typed ty ->
let n = List.length args in let n = List.length args in
let rec replicate acc n = 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 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; decl_term s res;
`Term res `Term res
(* Expression parsing *) (* Msat.Expression parsing *)
(* ************************************************************************ *) (* ************************************************************************ *)
let rec parse_expr (env : env) t = let rec parse_expr (env : env) t =
@ -303,24 +291,24 @@ let rec parse_expr (env : env) t =
(* Basic formulas *) (* Basic formulas *)
| { Ast.term = Ast.App ({ Ast.term = Ast.Builtin Ast.True }, []) } | { Ast.term = Ast.App ({ Ast.term = Ast.Builtin Ast.True }, []) }
| { 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.App ({ Ast.term = Ast.Builtin Ast.False }, []) }
| { 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) } -> | { 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) } -> | { 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 -> | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Xor}, l) } as t ->
begin match l with begin match l with
| [p; q] -> | [p; q] ->
let f = parse_formula env p in let f = parse_formula env p in
let g = parse_formula env q 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 | _ -> _bad_arity "xor" 2 t
end end
@ -329,7 +317,7 @@ let rec parse_expr (env : env) t =
| [p; q] -> | [p; q] ->
let f = parse_formula env p in let f = parse_formula env p in
let g = parse_formula env q 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 | _ -> _bad_arity "=>" 2 t
end end
@ -338,14 +326,14 @@ let rec parse_expr (env : env) t =
| [p; q] -> | [p; q] ->
let f = parse_formula env p in let f = parse_formula env p in
let g = parse_formula env q 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 | _ -> _bad_arity "<=>" 2 t
end end
| { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Not}, l) } as t -> | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Not}, l) } as t ->
begin match l with begin match l with
| [p] -> | [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 | _ -> _bad_arity "not" 1 t
end end
@ -365,9 +353,9 @@ let rec parse_expr (env : env) t =
let l' = List.map (parse_term env) args in let l' = List.map (parse_term env) args in
let l'' = diagonal l' in let l'' = diagonal l' in
Formula ( Formula (
Expr.Formula.make_and Msat.Expr.Formula.make_and
(List.map (fun (a, b) -> (List.map (fun (a, b) ->
Expr.Formula.make_not Msat.Expr.Formula.make_not
(make_eq t a b)) l'') (make_eq t a b)) l'')
) )
@ -387,15 +375,15 @@ let rec parse_expr (env : env) t =
and parse_var env = function and parse_var env = function
| { Ast.term = Ast.Colon ({ Ast.term = Ast.Symbol s }, e) } -> | { Ast.term = Ast.Colon ({ Ast.term = Ast.Symbol s }, e) } ->
begin match parse_expr env e with begin match parse_expr env e with
| Ttype -> `Ty (s, Expr.Id.ttype s.Id.name) | Ttype -> `Ty (s, Msat.Expr.Id.ttype s.Id.name)
| Ty ty -> `Term (s, Expr.Id.ty s.Id.name ty) | Ty ty -> `Term (s, Msat.Expr.Id.ty s.Id.name ty)
| _ -> _expected "type (or Ttype)" e | _ -> _expected "type (or Ttype)" e
end end
| { Ast.term = Ast.Symbol s } -> | { Ast.term = Ast.Symbol s } ->
begin match env.expect with begin match env.expect with
| Nothing -> assert false | Nothing -> assert false
| Type -> `Ty (s, Expr.Id.ttype s.Id.name) | Type -> `Ty (s, Msat.Expr.Id.ttype s.Id.name)
| Typed ty -> `Term (s, Expr.Id.ty s.Id.name ty) | Typed ty -> `Term (s, Msat.Expr.Id.ty s.Id.name ty)
end end
| t -> _expected "(typed) variable" t | t -> _expected "(typed) variable" t
@ -450,10 +438,10 @@ and parse_app env ast s args =
| `Not_found -> | `Not_found ->
begin match find_var env s with begin match find_var env s with
| `Ty f -> | `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 else _fo_term s ast
| `Term f -> | `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 else _fo_term s ast
| `Not_found -> | `Not_found ->
begin match find_global s with 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) Ty (ty_apply env ast f l)
and parse_app_term env ast f args = 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_l, t_l = take_drop n args in
let ty_args = List.map (parse_ty env) ty_l in let ty_args = List.map (parse_ty env) ty_l in
let t_args = List.map (parse_term env) t_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 | _ -> _expected "type" ast
and parse_term env 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 | Term t -> t
| _ -> _expected "term" ast | _ -> _expected "term" ast
and parse_formula env ast = and parse_formula env ast =
match parse_expr { env with expect = Typed Expr.Ty.prop } ast with match parse_expr { env with expect = Typed Msat.Expr.Ty.prop } ast with
| Term t when Expr.(Ty.equal Ty.prop t.t_type) -> | Term t when Msat.Expr.(Ty.equal Ty.prop t.t_type) ->
make_pred ast t make_pred ast t
| Formula p -> p | Formula p -> p
| _ -> _expected "formula" ast | _ -> _expected "formula" ast
@ -597,17 +585,17 @@ let rec parse_fun ty_args t_args env = function
let new_decl id t = let new_decl id t =
let env = empty_env () in 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); (fun k -> k id.Id.name Ast.print t);
begin match parse_sig env t with 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) -> | `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 end
let new_def id t = let new_def id t =
let env = empty_env () in 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); (fun k -> k id.Id.name Ast.print t);
begin match parse_fun [] [] env t with begin match parse_fun [] [] env t with
| `Ty (ty_args, body) -> def_ty id ty_args body | `Ty (ty_args, body) -> def_ty id ty_args body
@ -616,7 +604,7 @@ let new_def id t =
let new_formula t = let new_formula t =
let env = empty_env () in 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 let res = parse_formula env t in
res res

2
src/util/type.mli
View file

@ -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_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