simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-24 02:16:41 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

refactor: remove minismt things, make simple msat.sh

Browse source
This commit is contained in:
Simon Cruanes 2019-01-18 19:39:12 -06:00 • committed by Guillaume Bury
parent 5846ae7e17
commit 05e2506362
45 changed files with 137 additions and 2830 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
Makefile
View file

@ -20,12 +20,11 @@ build:
build-dev:
@dune build $(OPTS) @install
test: build
test:
@echo "run API tests…"
@dune runtest
@echo "run benchmarks…"
# @/usr/bin/time -f "%e" ./tests/run smt
@/usr/bin/time -f "%e" ./tests/run mcsat
@/usr/bin/time -f "%e" ./tests/run sat
enable_log:
cd src/core; ln -sf log_real.ml log.ml

1
dune-project
View file

@ -1 +1,2 @@
(lang dune 1.1)
(using menhir 1.0)

22
minismt.opam
View file

@ -1,22 +0,0 @@
opam-version: "2.0"
name: "minismt"
synopsis: "Test library for msat"
license: "Apache"
version: "dev"
author: ["Simon Cruanes" "Guillaume Bury"]
maintainer: ["guillaume.bury@gmail.com" "simon.cruanes.2007@m4x.org"]
build: [
["dune" "build" "@install" "-p" name "-j" jobs]
["dune" "build" "@doc" "-p" name] {with-doc}
["dune" "runtest" "-p" name] {with-test}
]
depends: [
"dune" {build}
"dolmen"
"msat"
]
tags: [ "sat" "smt" ]
homepage: "https://github.com/Gbury/mSAT"
dev-repo: "git+https://github.com/Gbury/mSAT.git"
bug-reports: "https://github.com/Gbury/mSAT/issues/"

1
msat.exe
View file

@ -1 +0,0 @@
_build/default/src/main/main.exe

2
msat.opam
View file

@ -13,7 +13,7 @@ build: [
depends: [
"ocaml" { >= "4.03" }
"dune" {build}
"dolmen" {with-test & = "dev" }
"containers" {with-test}
]
tags: [ "sat" "smt" ]
homepage: "https://github.com/Gbury/mSAT"

3
msat.sh Executable file
View file

@ -0,0 +1,3 @@
#!/bin/sh
exec dune exec src/main/main.exe -- $@

2
src/core/Msat.ml
View file

@ -33,6 +33,8 @@ module Make_mcsat_expr(E : Expr_intf.S) = Solver_types.McMake(E)
module Make = Solver.Make
module Make_dummy = Plugin_intf.Dummy
(**/**)
module Vec = Vec
module Log = Log

19
src/core/Plugin_intf.ml
View file

@ -119,3 +119,22 @@ module type S = sig
end
module Dummy(F: Solver_types.S)
: S with type formula = F.formula
and type term = F.term
and type proof = F.proof
= struct
type formula = F.formula
type term = F.term
type proof = F.proof
type level = unit
let dummy = ()
let current_level () = ()
let assume _ = Sat
let if_sat _ = Sat
let backtrack _ = ()
let eval _ = Unknown
let assign t = t
let mcsat = false
let iter_assignable _ _ = ()
end

12
src/core/Theory_intf.ml
View file

@ -83,3 +83,15 @@ module type S = sig
end
module Dummy(F: Formula_intf.S)
: S with type formula = F.t
= struct
type formula = F.t
type proof = unit
type level = unit
let dummy = ()
let current_level () = ()
let assume _ = Sat
let if_sat _ = Sat
let backtrack _ = ()
end

20
src/main/Dimacs_lex.mll Normal file
View file

@ -0,0 +1,20 @@
{
open Dimacs_parse
}
let number = ['1' - '9'] ['0' - '9']*
rule token = parse
| eof { EOF }
| "c" { comment lexbuf }
| [' ' '\t' '\r'] { token lexbuf }
| 'p' { P }
| "cnf" { CNF }
| '\n' { Lexing.new_line lexbuf; token lexbuf }
| '0' { ZERO }
| '-'? number { LIT (int_of_string (Lexing.lexeme lexbuf)) }
| _ { failwith @@ Printf.sprintf "dimacs.lexer: unexpected char `%s`" (Lexing.lexeme lexbuf) }
and comment = parse
| '\n' { Lexing.new_line lexbuf; token lexbuf }
| [^'\n'] { comment lexbuf }

41
src/main/Dimacs_parse.mly Normal file
View file

@ -0,0 +1,41 @@
/* Copyright 2005 INRIA */
%{
let lnum pos = pos.Lexing.pos_lnum
let cnum pos = pos.Lexing.pos_cnum - pos.Lexing.pos_bol
let pp_pos out (start,stop) =
Format.fprintf out "(at %d:%d - %d:%d)"
(lnum start) (cnum start) (lnum stop) (cnum stop)
%}
%token <int> LIT
%token ZERO
%token P CNF EOF
%start file
%type <int list list> file
%%
/* DIMACS syntax */
prelude:
| P CNF LIT LIT { () }
| error
{
failwith @@ Format.asprintf "expected prelude %a" pp_pos ($startpos,$endpos)
}
clauses:
| l=clause* { l }
| error
{
failwith @@ Format.asprintf "expected list of clauses %a"
pp_pos ($startpos,$endpos)
}
file:
| prelude l=clauses EOF { l }
clause:
| l=LIT+ ZERO { l }

10
src/main/dune
View file

@ -2,10 +2,12 @@
; main binary
(executable
(name main)
(public_name msat_solver)
(package minismt)
(libraries msat msat.backend minismt.sat minismt.smt minismt.mcsat dolmen)
(flags :standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string)
;(package msat)
(libraries containers msat msat_sat msat.backend)
(flags :standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Msat)
(ocamlopt_flags :standard -O3 -color always
-unbox-closures -unbox-closures-factor 20)
)
(menhir (modules Dimacs_parse))
(ocamllex (modules Dimacs_lex))

104
src/main/main.ml
View file

@ -4,8 +4,6 @@ Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
open Msat
exception Incorrect_model
exception Out_of_time
exception Out_of_space
@ -18,21 +16,9 @@ let p_proof_print = ref false
let time_limit = ref 300.
let size_limit = ref 1000_000_000.
module P =
Dolmen.Logic.Make(Dolmen.ParseLocation)
(Dolmen.Id)(Dolmen.Term)(Dolmen.Statement)
module type S = sig
val do_task : Dolmen.Statement.t -> unit
end
module Make
(S : Msat.S)
(T : Minismt.Type.S with type atom := S.atom)
: sig
val do_task : Dolmen.Statement.t -> unit
end = struct
module S = Msat_sat
module Process = struct
module D = Msat_backend.Dot.Make(S.Proof)(Msat_backend.Dot.Default(S.Proof))
let hyps = ref []
@ -73,65 +59,25 @@ module Make
Format.printf "Unsat (%f/%f)@." t t'
end
let do_task s =
match s.Dolmen.Statement.descr with
| Dolmen.Statement.Def (id, t) -> T.def id t
| Dolmen.Statement.Decl (id, t) -> T.decl id t
| Dolmen.Statement.Clause l ->
let cnf = T.antecedent (Dolmen.Term.or_ l) in
hyps := cnf @ !hyps;
S.assume st cnf
| Dolmen.Statement.Consequent t ->
let cnf = T.consequent t in
hyps := cnf @ !hyps;
S.assume st cnf
| Dolmen.Statement.Antecedent t ->
let cnf = T.antecedent t in
hyps := cnf @ !hyps;
S.assume st cnf
| Dolmen.Statement.Pack [
{ Dolmen.Statement.descr = Dolmen.Statement.Push 1;_ };
{ Dolmen.Statement.descr = Dolmen.Statement.Antecedent f;_ };
{ Dolmen.Statement.descr = Dolmen.Statement.Prove [];_ };
{ Dolmen.Statement.descr = Dolmen.Statement.Pop 1;_ };
] ->
let assumptions = T.assumptions f in
prove ~assumptions ()
| Dolmen.Statement.Prove l ->
let assumptions = List.map T.assumptions l |> List.flatten in
prove ~assumptions ()
| Dolmen.Statement.Set_info _
| Dolmen.Statement.Set_logic _ -> ()
| Dolmen.Statement.Exit -> exit 0
| _ ->
Format.printf "Command not supported:@\n%a@."
Dolmen.Statement.print s
let conv_c c = List.rev_map S.Expr.make c
let add_clauses cs =
S.assume st @@ CCList.map conv_c cs
end
module Sat = Make(Minismt_sat)(Minismt_sat.Type)
module Smt = Make(Minismt_smt)(Minismt_smt.Type)
module Mcsat = Make(Minismt_mcsat)(Minismt_smt.Type)
let solver = ref (module Sat : S)
let solver_list = [
"sat", (module Sat : S);
"smt", (module Smt : S);
"mcsat", (module Mcsat : S);
]
let parse_file f =
let module L = Lexing in
CCIO.with_in f
(fun ic ->
let buf = L.from_channel ic in
buf.L.lex_curr_p <- {buf.L.lex_curr_p with L.pos_fname=f;};
Dimacs_parse.file Dimacs_lex.token buf)
let error_msg opt arg l =
Format.fprintf Format.str_formatter "'%s' is not a valid argument for '%s', valid arguments are : %a"
arg opt (fun fmt -> List.iter (fun (s, _) -> Format.fprintf fmt "%s, " s)) l;
Format.flush_str_formatter ()
let set_flag opt arg flag l =
try
flag := List.assoc arg l
with Not_found ->
invalid_arg (error_msg opt arg l)
let set_solver s = set_flag "Solver" s solver solver_list
(* Arguments parsing *)
let int_arg r arg =
let l = String.length arg in
@ -174,8 +120,6 @@ let argspec = Arg.align [
" If provided, print the dot proof in the given file";
"-gc", Arg.Unit setup_gc_stat,
" Outputs statistics about the GC";
"-s", Arg.String set_solver,
"{sat,smt,mcsat} Sets the solver to use (default smt)";
"-size", Arg.String (int_arg size_limit),
"<s>[kMGT] Sets the size limit for the sat solver";
"-time", Arg.String (int_arg time_limit),
@ -194,7 +138,6 @@ let check () =
else if s > !size_limit then
raise Out_of_space
let main () =
(* Administrative duties *)
Arg.parse argspec input_file usage;
@ -205,14 +148,9 @@ let main () =
let al = Gc.create_alarm check in
(* Interesting stuff happening *)
let lang, input = P.parse_file !file in
let module S = (val !solver : S) in
List.iter S.do_task input;
(* Small hack for dimacs, which do not output a "Prove" statement *)
begin match lang with
| P.Dimacs -> S.do_task @@ Dolmen.Statement.check_sat []
| _ -> ()
end;
let clauses = parse_file !file in
Process.add_clauses clauses;
Process.prove ~assumptions:[] ();
Gc.delete_alarm al;
()
@ -229,14 +167,4 @@ let () =
| Incorrect_model ->
Format.printf "Internal error : incorrect *sat* model@.";
exit 4
| Minismt_sat.Type.Typing_error (msg, t)
| Minismt_smt.Type.Typing_error (msg, t) ->
let b = Printexc.get_backtrace () in
let loc = match t.Dolmen.Term.loc with
| Some l -> l | None -> Dolmen.ParseLocation.mk "<>" 0 0 0 0
in
Format.fprintf Format.std_formatter "While typing:@\n%a@\n%a: typing error\n%s@."
Dolmen.Term.print t Dolmen.ParseLocation.fmt loc msg;
if Printexc.backtrace_status () then
Format.fprintf Format.std_formatter "%s@." b

13
src/mcsat/Minismt_mcsat.ml
View file

@ -1,13 +0,0 @@
(*
MSAT is free software, using the Apache license, see file LICENSE
Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
include
Minismt.Mcsolver.Make(struct
type proof = unit
module Term = Minismt_smt.Expr.Term
module Formula = Minismt_smt.Expr.Atom
end)(Plugin_mcsat)

8
src/mcsat/Minismt_mcsat.mli
View file

@ -1,8 +0,0 @@
(*
MSAT is free software, using the Apache license, see file LICENSE
Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
include Minismt.Solver.S with type formula = Minismt_smt.Expr.atom

68
src/mcsat/README.md
View file

@ -1,68 +0,0 @@
# Equality in McSat
## Basics
McSat theories have different interfaces and requirements than classic SMT theories.
The good point of these additional requirements is that it becomes easier to combine
theories, since the assignments allow theories to exchange information about
the equality of terms. In a context where there are multiple theories, they each have
to handle the following operations:
- return an assignment value for a given term
- receive a new assignment value for a term (the assignment may, or not, have been
done by another theory)
- receive a new assertion (i.e an atomic formula asserted to be true by the sat solver)
With assignments, the reason for a theory returning UNSAT now becomes when
some term has no potential assignment value because of past assignments
and assertions, (or in some cases, an assignments decided by a theory A is
incompatible with the possible assignments of the same term according to theory B).
When returning UNSAT, the theory must, as usual return a conflict clause.
The conflict clause must be a tautology, and such that every atomic proposition
in it must evaluate to false using assignments.
## Equality of uninterpreted types
To handle equality on arbitrary values efficiently, we maintain a simple union-find
of known equalities (*NOT* computing congruence closure, only the reflexive-transitive
closure of the equalities), where each class can be tagged with an optional assignment.
When receiving a new assertions by the sat, we update the union-find. When the theory is
asked for an assignment value for a term, we lookup its class. If it is tagged, we return
the tagged value. Else, we take an arbitrary representative $x$ of the class and return it.
When a new assignment $t \mapsto v$ is propagated by the sat solver, there are three cases:
- the class of $t$ if not tagged, we then tag it with $t \mapsto v$ and continue
- the class of $t$ is already tagged with $\_ mapsto v$, we do nothing
- the class of $t$ is tagged with a $t' \mapsto v'$, we raise unsat,
using the explanation of why $t$ and $t'$ are in the same class and the equality
$t' = v'$
Additionally, in order to handle disequalities, each class contains the list of classes
it must be distinct from. There are then two possible reasons to raise unsat, when
a disequality $x <> y$ is invalidated by assignemnts or later equalities:
- when two classes that should be distinct are merged
- when two classes that should be distinct are assigned to the same value
in both cases, we use the union-find structure to get the explanation of why $x$ and $y$
must now be equal (since their class have been merged), and use that to create the
conflict clause.
## Uninterpreted functions
The uninterpreted function theory is much simpler, it doesn't return any assignemnt values
(the equality theory does it already), but rather check that the assignemnts so far are
coherent with the semantics of uninterpreted functions.
So for each function asignment $f(x1,...,xn) \mapsto v$, we wait for all the arguments to
also be assigned to values $x1 \mapsto v1$, etc... $xn \mapsto vn$, and we add the binding
$(f,v1,...,vn) \mapsto (v,x1,...,xn)$ in a map (meaning that in the model $f$ applied to
$v1,...,vn$ is equal to $v$). If a binding $(f,v1,...,vn) \mapsto (v',y1,...,yn)$ already
exists (with $v' <> v$), then we raise UNSAT, with the explanation:
$( x1=y1 /\ ... /\ xn = yn) => f(x1,...,xn) = f(y1,...,yn)$

99
src/mcsat/backtrack.ml
View file

@ -1,99 +0,0 @@
module Stack = struct
type op =
(* Stack structure *)
| Nil : op
| Level : op * int -> op
(* Undo operations *)
| Set : 'a ref * 'a * op -> op
| Call1 : ('a -> unit) * 'a * op -> op
| Call2 : ('a -> 'b -> unit) * 'a * 'b * op -> op
| Call3 : ('a -> 'b -> 'c -> unit) * 'a * 'b * 'c * op -> op
| CallUnit : (unit -> unit) * op -> op
type t = {
mutable stack : op;
mutable last : int;
}
type level = int
let dummy_level = -1
let create () = {
stack = Nil;
last = dummy_level;
}
let register_set t ref value = t.stack <- Set(ref, value, t.stack)
let register_undo t f = t.stack <- CallUnit (f, t.stack)
let register1 t f x = t.stack <- Call1 (f, x, t.stack)
let register2 t f x y = t.stack <- Call2 (f, x, y, t.stack)
let register3 t f x y z = t.stack <- Call3 (f, x, y, z, t.stack)
let curr = ref 0
let push t =
let level = !curr in
t.stack <- Level (t.stack, level);
t.last <- level;
incr curr
let rec level t =
match t.stack with
| Level (_, lvl) -> lvl
| _ -> push t; level t
let backtrack t lvl =
let rec pop = function
| Nil -> assert false
| Level (op, level) as current ->
if level = lvl then begin
t.stack <- current;
t.last <- level
end else
pop op
| Set (ref, x, op) -> ref := x; pop op
| CallUnit (f, op) -> f (); pop op
| Call1 (f, x, op) -> f x; pop op
| Call2 (f, x, y, op) -> f x y; pop op
| Call3 (f, x, y, z, op) -> f x y z; pop op
in
pop t.stack
let pop t = backtrack t (t.last)
end
module Hashtbl(K : Hashtbl.HashedType) = struct
module H = Hashtbl.Make(K)
type key = K.t
type 'a t = {
tbl : 'a H.t;
stack : Stack.t;
}
let create ?(size=256) stack = {tbl = H.create size; stack; }
let mem {tbl; _} x = H.mem tbl x
let find {tbl; _} k = H.find tbl k
let add t k v =
Stack.register2 t.stack H.remove t.tbl k;
H.add t.tbl k v
let remove t k =
try
let v = find t k in
Stack.register3 t.stack H.add t.tbl k v;
H.remove t.tbl k
with Not_found -> ()
let fold t f acc = H.fold f t.tbl acc
let iter f t = H.iter f t.tbl
end

77
src/mcsat/backtrack.mli
View file

@ -1,77 +0,0 @@
(** Provides helpers for backtracking.
This module defines backtracking stacks, i.e stacks of undo actions
to perform when backtracking to a certain point. This allows for
side-effect backtracking, and so to have backtracking automatically
handled by extensions without the need for explicit synchronisation
between the dispatcher and the extensions.
*)
module Stack : sig
(** A backtracking stack is a stack of undo actions to perform
in order to revert back to a (mutable) state. *)
type t
(** The type for a stack. *)
type level
(** The type of backtracking point. *)
val create : unit -> t
(** Creates an empty stack. *)
val dummy_level : level
(** A dummy level. *)
val push : t -> unit
(** Creates a backtracking point at the top of the stack. *)
val pop : t -> unit
(** Pop all actions in the undo stack until the first backtracking point. *)
val level : t -> level
(** Insert a named backtracking point at the top of the stack. *)
val backtrack : t -> level -> unit
(** Backtrack to the given named backtracking point. *)
val register_undo : t -> (unit -> unit) -> unit
(** Adds a callback at the top of the stack. *)
val register1 : t -> ('a -> unit) -> 'a -> unit
val register2 : t -> ('a -> 'b -> unit) -> 'a -> 'b -> unit
val register3 : t -> ('a -> 'b -> 'c -> unit) -> 'a -> 'b -> 'c -> unit
(** Register functions to be called on the given arguments at the top of the stack.
Allows to save some space by not creating too much closure as would be the case if
only [unit -> unit] callbacks were stored. *)
val register_set : t -> 'a ref -> 'a -> unit
(** Registers a ref to be set to the given value upon backtracking. *)
end
module Hashtbl :
functor (K : Hashtbl.HashedType) ->
sig
(** Provides wrappers around hastables in order to have
very simple integration with backtraking stacks.
All actions performed on this table register the corresponding
undo operations so that backtracking is automatic. *)
type key = K.t
(** The type of keys of the Hashtbl. *)
type 'a t
(** The type of hastable from keys to values of type ['a]. *)
val create : ?size:int -> Stack.t -> 'a t
(** Creates an empty hashtable, that registers undo operations on the given stack. *)
val add : 'a t -> key -> 'a -> unit
val mem : 'a t -> key -> bool
val find : 'a t -> key -> 'a
val remove : 'a t -> key -> unit
val iter : (key -> 'a -> unit) -> 'a t -> unit
val fold : 'a t -> (key -> 'a -> 'b -> 'b) -> 'b -> 'b
(** Usual operations on the hashtabl. For more information see the Hashtbl module of the stdlib. *)
end

12
src/mcsat/dune
View file

@ -1,12 +0,0 @@
(library
(name minismt_mcsat)
(public_name minismt.mcsat)
(libraries msat minismt minismt.smt)
(synopsis "mcsat interface")
(flags :standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Msat)
(ocamlopt_flags :standard -O3 -bin-annot
-unbox-closures -unbox-closures-factor 20)
)

232
src/mcsat/eclosure.ml
View file

@ -1,232 +0,0 @@
module type Key = sig
type t
val hash : t -> int
val equal : t -> t -> bool
val compare : t -> t -> int
val print : Format.formatter -> t -> unit
end
module type S = sig
type t
type var
exception Unsat of var * var * var list
val create : Backtrack.Stack.t -> t
val find : t -> var -> var
val add_eq : t -> var -> var -> unit
val add_neq : t -> var -> var -> unit
val add_tag : t -> var -> var -> unit
val find_tag : t -> var -> var * (var * var) option
end
module Make(T : Key) = struct
module M = Map.Make(T)
module H = Backtrack.Hashtbl(T)
type var = T.t
exception Equal of var * var
exception Same_tag of var * var
exception Unsat of var * var * var list
type repr_info = {
rank : int;
tag : (T.t * T.t) option;
forbidden : (var * var) M.t;
}
type node =
| Follow of var
| Repr of repr_info
type t = {
size : int H.t;
expl : var H.t;
repr : node H.t;
}
let create s = {
size = H.create s;
expl = H.create s;
repr = H.create s;
}
(* Union-find algorithm with path compression *)
let self_repr = Repr { rank = 0; tag = None; forbidden = M.empty }
let find_hash m i default =
try H.find m i
with Not_found -> default
let rec find_aux m i =
match find_hash m i self_repr with
| Repr r -> r, i
| Follow j ->
let r, k = find_aux m j in
H.add m i (Follow k);
r, k
let get_repr h x =
let r, y = find_aux h.repr x in
y, r
let tag h x v =
let r, y = find_aux h.repr x in
let new_m =
{ r with
tag = match r.tag with
| Some (_, v') when not (T.equal v v') -> raise (Equal (x, y))
| (Some _) as t -> t
| None -> Some (x, v) }
in
H.add h.repr y (Repr new_m)
let find h x = fst (get_repr h x)
let find_tag h x =
let r, y = find_aux h.repr x in
y, r.tag
let forbid_aux m x =
try
let a, b = M.find x m in
raise (Equal (a, b))
with Not_found -> ()
let link h x mx y my =
let new_m = {
rank = if mx.rank = my.rank then mx.rank + 1 else mx.rank;
tag = (match mx.tag, my.tag with
| Some (z, t1), Some (w, t2) ->
if not (T.equal t1 t2) then begin
Log.debugf 3
(fun k -> k "Tag shenanigan : %a (%a) <> %a (%a)"
T.print t1 T.print z T.print t2 T.print w);
raise (Equal (z, w))
end else Some (z, t1)
| Some t, None | None, Some t -> Some t
| None, None -> None);
forbidden = M.merge (fun _ b1 b2 -> match b1, b2 with
| Some r, _ | None, Some r -> Some r | _ -> assert false)
mx.forbidden my.forbidden;}
in
let aux m z eq =
match H.find m z with
| Repr r ->
let r' = { r with
forbidden = M.add x eq (M.remove y r.forbidden) }
in
H.add m z (Repr r')
| _ -> assert false
in
M.iter (aux h.repr) my.forbidden;
H.add h.repr y (Follow x);
H.add h.repr x (Repr new_m)
let union h x y =
let rx, mx = get_repr h x in
let ry, my = get_repr h y in
if T.compare rx ry <> 0 then begin
forbid_aux mx.forbidden ry;
forbid_aux my.forbidden rx;
if mx.rank > my.rank then begin
link h rx mx ry my
end else begin
link h ry my rx mx
end
end
let forbid h x y =
let rx, mx = get_repr h x in
let ry, my = get_repr h y in
if T.compare rx ry = 0 then
raise (Equal (x, y))
else match mx.tag, my.tag with
| Some (a, v), Some (b, v') when T.compare v v' = 0 ->
raise (Same_tag(a, b))
| _ ->
H.add h.repr ry (Repr { my with forbidden = M.add rx (x, y) my.forbidden });
H.add h.repr rx (Repr { mx with forbidden = M.add ry (x, y) mx.forbidden })
(* Equivalence closure with explanation output *)
let find_parent v m = find_hash m v v
let rec root m acc curr =
let parent = find_parent curr m in
if T.compare curr parent = 0 then
curr :: acc
else
root m (curr :: acc) parent
let rec rev_root m curr =
let next = find_parent curr m in
if T.compare curr next = 0 then
curr
else begin
H.remove m curr;
let res = rev_root m next in
H.add m next curr;
res
end
let expl t a b =
let rec aux last = function
| x :: r, y :: r' when T.compare x y = 0 ->
aux (Some x) (r, r')
| l, l' -> begin match last with
| Some z -> List.rev_append (z :: l) l'
| None -> List.rev_append l l'
end
in
aux None (root t.expl [] a, root t.expl [] b)
let add_eq_aux t i j =
if T.compare (find t i) (find t j) = 0 then
()
else begin
let old_root_i = rev_root t.expl i in
let old_root_j = rev_root t.expl j in
let nb_i = find_hash t.size old_root_i 0 in
let nb_j = find_hash t.size old_root_j 0 in
if nb_i < nb_j then begin
H.add t.expl i j;
H.add t.size j (nb_i + nb_j + 1)
end else begin
H.add t.expl j i;
H.add t.size i (nb_i + nb_j + 1)
end
end
(* Functions wrapped to produce explanation in case
* something went wrong *)
let add_tag t x v =
match tag t x v with
| () -> ()
| exception Equal (a, b) ->
raise (Unsat (a, b, expl t a b))
let add_eq t i j =
add_eq_aux t i j;
match union t i j with
| () -> ()
| exception Equal (a, b) ->
raise (Unsat (a, b, expl t a b))
let add_neq t i j =
match forbid t i j with
| () -> ()
| exception Equal (a, b) ->
raise (Unsat (a, b, expl t a b))
| exception Same_tag (_, _) ->
add_eq_aux t i j;
let res = expl t i j in
raise (Unsat (i, j, res))
end

60
src/mcsat/eclosure.mli
View file

@ -1,60 +0,0 @@
(** Equality closure using an union-find structure.
This module implements a equality closure algorithm using an union-find structure.
It supports adding of equality as well as inequalities, and raises exceptions
when trying to build an incoherent closure.
Please note that this does not implement congruence closure, as we do not
look inside the terms we are given. *)
module type Key = sig
(** The type of keys used by the equality closure algorithm *)
type t
val hash : t -> int
val equal : t -> t -> bool
val compare : t -> t -> int
val print : Format.formatter -> t -> unit
end
module type S = sig
(** Type signature for the equality closure algorithm *)
type t
(** Mutable state of the equality closure algorithm. *)
type var
(** The type of expressions on which equality closure is built *)
exception Unsat of var * var * var list
(** Raise when trying to build an incoherent equality closure, with an explanation
of the incoherence.
[Unsat (a, b, l)] is such that:
- [a <> b] has been previously added to the closure.
- [l] start with [a] and ends with [b]
- for each consecutive terms [p] and [q] in [l],
an equality [p = q] has been added to the closure.
*)
val create : Backtrack.Stack.t -> t
(** Creates an empty state which uses the given backtrack stack *)
val find : t -> var -> var
(** Returns the representative of the given expression in the current closure state *)
val add_eq : t -> var -> var -> unit
val add_neq : t -> var -> var -> unit
(** Add an equality of inequality to the closure. *)
val add_tag : t -> var -> var -> unit
(** Add a tag to an expression. The algorithm ensures that each equality class
only has one tag. If incoherent tags are added, an exception is raised. *)
val find_tag : t -> var -> var * (var * var) option
(** Returns the tag associated with the equality class of the given term, if any.
More specifically, [find_tag e] returns a pair [(repr, o)] where [repr] is the representant of the equality
class of [e]. If the class has a tag, then [o = Some (e', t)] such that [e'] has been tagged with [t] previously. *)
end
module Make(T : Key) : S with type var = T.t

200
src/mcsat/plugin_mcsat.ml
View file

@ -1,200 +0,0 @@
(* Module initialization *)
module Expr_smt = Minismt_smt.Expr
module E = Eclosure.Make(Expr_smt.Term)
module H = Backtrack.Hashtbl(Expr_smt.Term)
module M = Hashtbl.Make(Expr_smt.Term)
(* Type definitions *)
type proof = unit
type term = Expr_smt.Term.t
type formula = Expr_smt.Atom.t
type level = Backtrack.Stack.level
exception Absurd of Expr_smt.Atom.t list
(* Backtracking *)
let stack = Backtrack.Stack.create ()
let dummy = Backtrack.Stack.dummy_level
let current_level () = Backtrack.Stack.level stack
let backtrack = Backtrack.Stack.backtrack stack
(* Equality closure *)
let uf = E.create stack
let assign t =
match E.find_tag uf t with
| _, None -> t
| _, Some (_, v) -> v
(* Propositional constants *)
let true_ = Expr_smt.(Term.of_id (Id.ty "true" Ty.prop))
let false_ = Expr_smt.(Term.of_id (Id.ty "false" Ty.prop))
(* Uninterpreted functions and predicates *)
let map : Expr_smt.term H.t = H.create stack
let watch = M.create 4096
let interpretation = H.create stack
let pop_watches t =
try
let l = M.find watch t in
M.remove watch t;
l
with Not_found ->
[]
let add_job j x =
let l = try M.find watch x with Not_found -> [] in
M.add watch x (j :: l)
let update_job x ((t, watchees) as job) =
try
let y = List.find (fun y -> not (H.mem map y)) watchees in
add_job job y
with Not_found ->
add_job job x;
begin match t with
| { Expr_smt.term = Expr_smt.App (f, tys, l);_ } ->
let is_prop = Expr_smt.(Ty.equal t.t_type Ty.prop) in
let t_v = H.find map t in
let l' = List.map (H.find map) l in
let u = Expr_smt.Term.apply f tys l' in
begin try
let t', u_v = H.find interpretation u in
if not (Expr_smt.Term.equal t_v u_v) then begin
match t' with
| { Expr_smt.term = Expr_smt.App (_, _, r); _ } when is_prop ->
let eqs = List.map2 (fun a b -> Expr_smt.Atom.neg (Expr_smt.Atom.eq a b)) l r in
if Expr_smt.(Term.equal u_v true_) then begin
let res = Expr_smt.Atom.pred t ::
Expr_smt.Atom.neg (Expr_smt.Atom.pred t') :: eqs in
raise (Absurd res)
end else begin
let res = Expr_smt.Atom.pred t' ::
Expr_smt.Atom.neg (Expr_smt.Atom.pred t) :: eqs in
raise (Absurd res)
end
| { Expr_smt.term = Expr_smt.App (_, _, r); _ } ->
let eqs = List.map2 (fun a b -> Expr_smt.Atom.neg (Expr_smt.Atom.eq a b)) l r in
let res = Expr_smt.Atom.eq t t' :: eqs in
raise (Absurd res)
| _ -> assert false
end
with Not_found ->
H.add interpretation u (t, t_v);
end
| _ -> assert false
end
let rec update_watches x = function
| [] -> ()
| job :: r ->
begin
try
update_job x job;
with exn ->
List.iter (fun j -> add_job j x) r;
raise exn
end;
update_watches x r
let add_watch t l =
update_job t (t, l)
let add_assign t v =
H.add map t v;
update_watches t (pop_watches t)
(* Assignemnts *)
let rec iter_aux f = function
| { Expr_smt.term = Expr_smt.Var _; _ } as t ->
Log.debugf 10 (fun k -> k "Adding %a as assignable" Expr_smt.Term.print t);
f t
| { Expr_smt.term = Expr_smt.App (_, _, l); _ } as t ->
if l <> [] then add_watch t (t :: l);
List.iter (iter_aux f) l;
Log.debugf 10 (fun k -> k "Adding %a as assignable" Expr_smt.Term.print t);
f t
let iter_assignable f = function
| { Expr_smt.atom = Expr_smt.Pred { Expr_smt.term = Expr_smt.Var _;_ }; _ } -> ()
| { Expr_smt.atom = Expr_smt.Pred ({ Expr_smt.term = Expr_smt.App (_, _, l);_} as t); _ } ->
if l <> [] then add_watch t (t :: l);
List.iter (iter_aux f) l;
| { Expr_smt.atom = Expr_smt.Equal (a, b);_ } ->
iter_aux f a; iter_aux f b
let eval = function
| { Expr_smt.atom = Expr_smt.Pred t; _ } ->
begin try
let v = H.find map t in
if Expr_smt.Term.equal v true_ then
Plugin_intf.Valued (true, [t])
else if Expr_smt.Term.equal v false_ then
Plugin_intf.Valued (false, [t])
else
Plugin_intf.Unknown
with Not_found ->
Plugin_intf.Unknown
end
| { Expr_smt.atom = Expr_smt.Equal (a, b); sign; _ } ->
begin try
let v_a = H.find map a in
let v_b = H.find map b in
if Expr_smt.Term.equal v_a v_b then
Plugin_intf.Valued(sign, [a; b])
else
Plugin_intf.Valued(not sign, [a; b])
with Not_found ->
Plugin_intf.Unknown
end
(* Theory propagation *)
let rec chain_eq = function
| [] | [_] -> []
| a :: ((b :: _) as l) -> (Expr_smt.Atom.eq a b) :: chain_eq l
let assume s =
let open Plugin_intf in
try
for i = s.start to s.start + s.length - 1 do
match s.get i with
| Assign (t, v) ->
add_assign t v;
E.add_tag uf t v
| Lit f ->
begin match f with
| { Expr_smt.atom = Expr_smt.Equal (u, v); sign = true;_ } ->
E.add_eq uf u v
| { Expr_smt.atom = Expr_smt.Equal (u, v); sign = false;_ } ->
E.add_neq uf u v
| { Expr_smt.atom = Expr_smt.Pred p; sign;_ } ->
let v = if sign then true_ else false_ in
add_assign p v
end
done;
Plugin_intf.Sat
with
| Absurd l ->
Plugin_intf.Unsat (l, ())
| E.Unsat (a, b, l) ->
let c = Expr_smt.Atom.eq a b :: List.map Expr_smt.Atom.neg (chain_eq l) in
Plugin_intf.Unsat (c, ())
let if_sat _ =
Plugin_intf.Sat

4
src/sat/Minismt_sat.ml → src/sat/Msat_sat.ml
View file

@ -4,7 +4,7 @@ Copyright 2016 Guillaume Bury
*)
module Expr = Expr_sat
module Type = Type_sat
include Minismt.Solver.Make(Expr)(Minismt.Solver.DummyTheory(Expr))
module F = Msat.Make_smt_expr(Expr)
include Msat.Make(F)(Msat.Make_dummy(F))

3
src/sat/Minismt_sat.mli → src/sat/Msat_sat.mli
View file

@ -10,8 +10,7 @@ Copyright 2016 Guillaume Bury
*)
module Expr = Expr_sat
module Type = Type_sat
include Minismt.Solver.S with type formula = Expr.t
include Msat.S with type formula = Expr.t
(** A functor that can generate as many solvers as needed. *)

10
src/sat/dune
View file

@ -1,12 +1,10 @@
(library
(name minismt_sat)
(public_name minismt.sat)
(libraries msat msat.tseitin minismt dolmen)
(synopsis "sat interface")
(name msat_sat)
; private
(libraries msat)
(flags :standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Msat)
(ocamlopt_flags :standard -O3 -bin-annot
(ocamlopt_flags :standard -O3 -color always
-unbox-closures -unbox-closures-factor 20)
)

90
src/sat/type_sat.ml
View file

@ -1,90 +0,0 @@
(*
MSAT is free software, using the Apache license, see file LICENSE
Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
(* Log&Module Init *)
(* ************************************************************************ *)
module Id = Dolmen.Id
module Ast = Dolmen.Term
module H = Hashtbl.Make(Id)
module Formula = Msat_tseitin.Make(Expr_sat)
(* Exceptions *)
(* ************************************************************************ *)
exception Typing_error of string * Dolmen.Term.t
(* Identifiers *)
(* ************************************************************************ *)
let symbols = H.create 42
let find_id id =
try
H.find symbols id
with Not_found ->
let res = Expr_sat.fresh () in
H.add symbols id res;
res
(* Actual parsing *)
(* ************************************************************************ *)
[@@@ocaml.warning "-9"]
let rec parse = function
| { Ast.term = Ast.Builtin Ast.True } ->
Formula.f_true
| { Ast.term = Ast.Builtin Ast.False } ->
Formula.f_false
| { Ast.term = Ast.Symbol id } ->
let s = find_id id in
Formula.make_atom s
| { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Not }, [p]) }
| { Ast.term = Ast.App ({Ast.term = Ast.Symbol { Id.name = "not" } }, [p]) } ->
Formula.make_not (parse p)
| { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.And }, l) }
| { Ast.term = Ast.App ({Ast.term = Ast.Symbol { Id.name = "and" } }, l) } ->
Formula.make_and (List.map parse l)
| { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Or }, l) }
| { Ast.term = Ast.App ({Ast.term = Ast.Symbol { Id.name = "or" } }, l) } ->
Formula.make_or (List.map parse l)
| { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Imply }, [p; q]) } ->
Formula.make_imply (parse p) (parse q)
| { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Equiv }, [p; q]) } ->
Formula.make_equiv (parse p) (parse q)
| { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Xor }, [p; q]) } ->
Formula.make_xor (parse p) (parse q)
| t ->
raise (Typing_error ("Term is not a pure proposition", t))
[@@@ocaml.warning "+9"]
(* Exported functions *)
(* ************************************************************************ *)
let decl _ t =
raise (Typing_error ("Declarations are not allowed in pure sat", t))
let def _ t =
raise (Typing_error ("Definitions are not allowed in pure sat", t))
let assumptions t =
let f = parse t in
let cnf = Formula.make_cnf f in
List.map (function
| [ x ] -> x
| _ -> assert false
) cnf
let antecedent t =
let f = parse t in
Formula.make_cnf f
let consequent t =
let f = parse t in
Formula.make_cnf @@ Formula.make_not f

12
src/sat/type_sat.mli
View file

@ -1,12 +0,0 @@
(*
MSAT is free software, using the Apache license, see file LICENSE
Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
(** Typechecking of terms from Dolmen.Term.t
This module provides functions to parse terms from the untyped syntax tree
defined in Dolmen, and generate formulas as defined in the Expr_sat module. *)
include Minismt.Type.S with type atom := Expr_sat.t

13
src/smt/Minismt_smt.ml
View file

@ -1,13 +0,0 @@
(*
MSAT is free software, using the Apache license, see file LICENSE
Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
module Expr = Expr_smt
module Type = Type_smt
module Th = Minismt.Solver.DummyTheory(Expr.Atom)
include Minismt.Solver.Make(Expr.Atom)(Th)

11
src/smt/Minismt_smt.mli
View file

@ -1,11 +0,0 @@
(*
MSAT is free software, using the Apache license, see file LICENSE
Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
module Expr = Expr_smt
module Type = Type_smt
include Minismt.Solver.S with type formula = Expr_smt.atom

12
src/smt/dune
View file

@ -1,12 +0,0 @@
(library
(name minismt_smt)
(public_name minismt.smt)
(libraries msat minismt msat.tseitin dolmen)
(synopsis "smt interface")
(flags :standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Msat)
(ocamlopt_flags :standard -O3 -bin-annot
-unbox-closures -unbox-closures-factor 20)
)

525
src/smt/expr_smt.ml
View file

@ -1,525 +0,0 @@
(*
Base modules that defines the terms used in the prover.
*)
(* Type definitions *)
(* ************************************************************************ *)
(* Private aliases *)
type hash = int
type index = int
(* Identifiers, parametrized by the kind of the type of the variable *)
type 'ty id = {
id_type : 'ty;
id_name : string;
index : index; (** unique *)
}
(* Type for first order types *)
type ttype = Type
(* The type of functions *)
type 'ty function_descr = {
fun_vars : ttype id list; (* prenex forall *)
fun_args : 'ty list;
fun_ret : 'ty;
}
(* Types *)
type ty_descr =
| TyVar of ttype id (** Bound variables *)
| TyApp of ttype function_descr id * ty list
and ty = {
ty : ty_descr;
mutable ty_hash : hash; (** lazy hash *)
}
(* Terms & formulas *)
type term_descr =
| Var of ty id
| App of ty function_descr id * ty list * term list
and term = {
term : term_descr;
t_type : ty;
mutable t_hash : hash; (* lazy hash *)
}
type atom_descr =
| Pred of term
| Equal of term * term
and atom = {
sign : bool;
atom : atom_descr;
mutable f_hash : hash; (* lazy hash *)
}
(* Utilities *)
(* ************************************************************************ *)
let rec list_cmp ord l1 l2 =
match l1, l2 with
| [], [] -> 0
| [], _ -> -1
| _, [] -> 1
| x1::l1', x2::l2' ->
let c = ord x1 x2 in
if c = 0
then list_cmp ord l1' l2'
else c
(* Exceptions *)
(* ************************************************************************ *)
exception Type_mismatch of term * ty * ty
exception Bad_arity of ty function_descr id * ty list * term list
exception Bad_ty_arity of ttype function_descr id * ty list
(* Printing functions *)
(* ************************************************************************ *)
module Print = struct
let rec list f sep fmt = function
| [] -> ()
| [x] -> f fmt x
| x :: ((_ :: _) as r) ->
Format.fprintf fmt "%a%s" f x sep;
list f sep fmt r
let id fmt v = Format.fprintf fmt "%s" v.id_name
let ttype fmt = function Type -> Format.fprintf fmt "Type"
let rec ty fmt t = match t.ty with
| TyVar v -> id fmt v
| TyApp (f, []) ->
Format.fprintf fmt "%a" id f
| TyApp (f, l) ->
Format.fprintf fmt "%a(%a)" id f (list ty ", ") l
let params fmt = function
| [] -> ()
| l -> Format.fprintf fmt "∀ %a. " (list id ", ") l
let signature print fmt f =
match f.fun_args with
| [] -> Format.fprintf fmt "%a%a" params f.fun_vars print f.fun_ret
| l -> Format.fprintf fmt "%a%a -> %a" params f.fun_vars
(list print " -> ") l print f.fun_ret
let fun_ty = signature ty
let fun_ttype = signature ttype
let id_type print fmt v = Format.fprintf fmt "%a : %a" id v print v.id_type
let id_ty = id_type ty
let id_ttype = id_type ttype
let const_ty = id_type fun_ty
let const_ttype = id_type fun_ttype
let rec term fmt t = match t.term with
| Var v -> id fmt v
| App (f, [], []) ->
Format.fprintf fmt "%a" id f
| App (f, [], args) ->
Format.fprintf fmt "%a(%a)" id f
(list term ", ") args
| App (f, tys, args) ->
Format.fprintf fmt "%a(%a; %a)" id f
(list ty ", ") tys
(list term ", ") args
let atom_aux fmt f =
match f.atom with
| Equal (a, b) ->
Format.fprintf fmt "%a %s %a"
term a (if f.sign then "=" else "<>") term b
| Pred t ->
Format.fprintf fmt "%s%a" (if f.sign then "" else "¬ ") term t
let atom fmt f = Format.fprintf fmt "⟦%a⟧" atom_aux f
end
(* Substitutions *)
(* ************************************************************************ *)
module Subst = struct
module Mi = Map.Make(struct
type t = int * int
let compare (a, b) (c, d) = match compare a c with 0 -> compare b d | x -> x
end)
type ('a, 'b) t = ('a * 'b) Mi.t
(* Usual functions *)
let empty = Mi.empty
let is_empty = Mi.is_empty
let iter f = Mi.iter (fun _ (key, value) -> f key value)
let fold f = Mi.fold (fun _ (key, value) acc -> f key value acc)
let bindings s = Mi.fold (fun _ (key, value) acc -> (key, value) :: acc) s []
(* Comparisons *)
let equal f = Mi.equal (fun (_, value1) (_, value2) -> f value1 value2)
let compare f = Mi.compare (fun (_, value1) (_, value2) -> f value1 value2)
let hash h s = Mi.fold (fun i (_, value) acc -> Hashtbl.hash (acc, i, h value)) s 1
let choose m = snd (Mi.choose m)
(* Iterators *)
let exists pred s =
try
iter (fun m s -> if pred m s then raise Exit) s;
false
with Exit ->
true
let for_all pred s =
try
iter (fun m s -> if not (pred m s) then raise Exit) s;
true
with Exit ->
false
let print print_key print_value fmt map =
let aux _ (key, value) =
Format.fprintf fmt "%a -> %a@ " print_key key print_value value
in
Format.fprintf fmt "@[<hov 0>%a@]" (fun _ -> Mi.iter aux) map
module type S = sig
type 'a key
val get : 'a key -> ('a key, 'b) t -> 'b
val mem : 'a key -> ('a key, 'b) t -> bool
val bind : 'a key -> 'b -> ('a key, 'b) t -> ('a key, 'b) t
val remove : 'a key -> ('a key, 'b) t -> ('a key, 'b) t
end
(* Variable substitutions *)
module Id = struct
type 'a key = 'a id
let tok v = (v.index, 0)
let get v s = snd (Mi.find (tok v) s)
let mem v s = Mi.mem (tok v) s
let bind v t s = Mi.add (tok v) (v, t) s
let remove v s = Mi.remove (tok v) s
end
end
(* Dummies *)
(* ************************************************************************ *)
module Dummy = struct
let id_ttype =
{ index = -1; id_name = "<dummy>"; id_type = Type; }
let ty =
{ ty = TyVar id_ttype; ty_hash = -1; }
let id =
{ index = -2; id_name = "<dummy>"; id_type = ty; }
let term =
{ term = Var id; t_type = ty; t_hash = -1; }
let atom =
{ atom = Pred term; sign = true; f_hash = -1; }
end
(* Variables *)
(* ************************************************************************ *)
module Id = struct
type 'a t = 'a id
(* Hash & comparisons *)
let hash v = v.index
let compare: 'a. 'a id -> 'a id -> int =
fun v1 v2 -> compare v1.index v2.index
let equal v1 v2 = compare v1 v2 = 0
(* Printing functions *)
let print = Print.id
(* Id count *)
let _count = ref 0
(* Constructors *)
let mk_new id_name id_type =
incr _count;
let index = !_count in
{ index; id_name; id_type }
let ttype name = mk_new name Type
let ty name ty = mk_new name ty
let const name fun_vars fun_args fun_ret =
mk_new name { fun_vars; fun_args; fun_ret; }
let ty_fun name n =
let rec replicate acc n =
if n <= 0 then acc
else replicate (Type :: acc) (n - 1)
in
const name [] (replicate [] n) Type
let term_fun = const
(* Builtin Types *)
let prop = ty_fun "Prop" 0
let base = ty_fun "$i" 0
end
(* Types *)
(* ************************************************************************ *)
module Ty = struct
type t = ty
type subst = (ttype id, ty) Subst.t
(* Hash & Comparisons *)
let rec hash_aux t = match t.ty with
| TyVar v -> Id.hash v
| TyApp (f, args) ->
Hashtbl.hash (Id.hash f, List.map hash args)
and hash t =
if t.ty_hash = -1 then
t.ty_hash <- hash_aux t;
t.ty_hash
let discr ty = match ty.ty with
| TyVar _ -> 1
| TyApp _ -> 2
let rec compare u v =
let hu = hash u and hv = hash v in
if hu <> hv then Pervasives.compare hu hv
else match u.ty, v.ty with
| TyVar v1, TyVar v2 -> Id.compare v1 v2
| TyApp (f1, args1), TyApp (f2, args2) ->
begin match Id.compare f1 f2 with
| 0 -> list_cmp compare args1 args2
| x -> x
end
| _, _ -> Pervasives.compare (discr u) (discr v)
let equal u v =
u == v || (hash u = hash v && compare u v = 0)
(* Printing functions *)
let print = Print.ty
(* Constructors *)
let mk_ty ty = { ty; ty_hash = -1; }
let of_id v = mk_ty (TyVar v)
let apply f args =
assert (f.id_type.fun_vars = []);
if List.length args <> List.length f.id_type.fun_args then
raise (Bad_ty_arity (f, args))
else
mk_ty (TyApp (f, args))
(* Builtin types *)
let prop = apply Id.prop []
let base = apply Id.base []
(* Substitutions *)
let rec subst_aux map t = match t.ty with
| TyVar v -> begin try Subst.Id.get v map with Not_found -> t end
| TyApp (f, args) ->
let new_args = List.map (subst_aux map) args in
if List.for_all2 (==) args new_args then t
else apply f new_args
let subst map t = if Subst.is_empty map then t else subst_aux map t
(* Typechecking *)
let instantiate f tys args =
if List.length f.id_type.fun_vars <> List.length tys ||
List.length f.id_type.fun_args <> List.length args then
raise (Bad_arity (f, tys, args))
else
let map = List.fold_left2 (fun acc v ty -> Subst.Id.bind v ty acc) Subst.empty f.id_type.fun_vars tys in
let fun_args = List.map (subst map) f.id_type.fun_args in
List.iter2 (fun t ty ->
if not (equal t.t_type ty) then raise (Type_mismatch (t, t.t_type, ty)))
args fun_args;
subst map f.id_type.fun_ret
end
(* Terms *)
(* ************************************************************************ *)
module Term = struct
type t = term
type subst = (ty id, term) Subst.t
(* Hash & Comparisons *)
let rec hash_aux t = match t.term with
| Var v -> Id.hash v
| App (f, tys, args) ->
let l = List.map Ty.hash tys in
let l' = List.map hash args in
Hashtbl.hash (Id.hash f, l, l')
and hash t =
if t.t_hash = -1 then
t.t_hash <- hash_aux t;
t.t_hash
let discr t = match t.term with
| Var _ -> 1
| App _ -> 2
let rec compare u v =
let hu = hash u and hv = hash v in
if hu <> hv then Pervasives.compare hu hv
else match u.term, v.term with
| Var v1, Var v2 -> Id.compare v1 v2
| App (f1, tys1, args1), App (f2, tys2, args2) ->
begin match Id.compare f1 f2 with
| 0 ->
begin match list_cmp Ty.compare tys1 tys2 with
| 0 -> list_cmp compare args1 args2
| x -> x
end
| x -> x
end
| _, _ -> Pervasives.compare (discr u) (discr v)
let equal u v =
u == v || (hash u = hash v && compare u v = 0)
(* Printing functions *)
let print = Print.term
(* Constructors *)
let mk_term term t_type =
{ term; t_type; t_hash = -1; }
let of_id v =
mk_term (Var v) v.id_type
let apply f ty_args t_args =
mk_term (App (f, ty_args, t_args)) (Ty.instantiate f ty_args t_args)
(* Substitutions *)
let rec subst_aux ty_map t_map t = match t.term with
| Var v -> begin try Subst.Id.get v t_map with Not_found -> t end
| App (f, tys, args) ->
let new_tys = List.map (Ty.subst ty_map) tys in
let new_args = List.map (subst_aux ty_map t_map) args in
if List.for_all2 (==) new_tys tys && List.for_all2 (==) new_args args then t
else apply f new_tys new_args
let subst ty_map t_map t =
if Subst.is_empty ty_map && Subst.is_empty t_map then
t
else
subst_aux ty_map t_map t
let rec replace (t, t') t'' = match t''.term with
| _ when equal t t'' -> t'
| App (f, ty_args, t_args) ->
apply f ty_args (List.map (replace (t, t')) t_args)
| _ -> t''
end
(* Formulas *)
(* ************************************************************************ *)
module Atom = struct
type t = atom
type proof = unit
(* Hash & Comparisons *)
let h_eq = 2
let h_pred = 3
let rec hash_aux f = match f.atom with
| Equal (t1, t2) ->
Hashtbl.hash (h_eq, Term.hash t1, Term.hash t2)
| Pred t ->
Hashtbl.hash (h_pred, Term.hash t)
and hash f =
if f.f_hash = -1 then
f.f_hash <- hash_aux f;
f.f_hash
let discr f = match f.atom with
| Equal _ -> 1
| Pred _ -> 2
let compare f g =
let hf = hash f and hg = hash g in
if hf <> hg then Pervasives.compare hf hg
else match f.atom, g.atom with
| Equal (u1, v1), Equal(u2, v2) ->
list_cmp Term.compare [u1; v1] [u2; v2]
| Pred t1, Pred t2 -> Term.compare t1 t2
| _, _ -> Pervasives.compare (discr f) (discr g)
let equal u v =
u == v || (hash u = hash v && compare u v = 0)
(* Printing functions *)
let print = Print.atom
(* Constructors *)
let mk_formula f = {
sign = true;
atom = f;
f_hash = -1;
}
let dummy = Dummy.atom
let pred t =
if not (Ty.equal Ty.prop t.t_type) then
raise (Type_mismatch (t, t.t_type, Ty.prop))
else
mk_formula (Pred t)
let fresh () =
let id = Id.ty "fresh" Ty.prop in
pred (Term.of_id id)
let neg f =
{ f with sign = not f.sign }
let eq a b =
if not (Ty.equal a.t_type b.t_type) then
raise (Type_mismatch (b, b.t_type, a.t_type))
else if Term.compare a b < 0 then
mk_formula (Equal (a, b))
else
mk_formula (Equal (b, a))
let norm f =
{ f with sign = true },
if f.sign then Formula_intf.Same_sign
else Formula_intf.Negated
end
module Formula = Msat_tseitin.Make(Atom)

326
src/smt/expr_smt.mli
View file

@ -1,326 +0,0 @@
(** Expressions for TabSat *)
(** {2 Type definitions} *)
(** These are custom types used in functions later. *)
(** {3 Identifiers} *)
(** Identifiers are the basic building blocks used to build types terms and expressions. *)
type hash
type index = private int
(** Private aliases to provide access. You should not have any need
to use these, instead use the functions provided by this module. *)
type 'ty id = private {
id_type : 'ty;
id_name : string;
index : index; (** unique *)
}
(** The type of identifiers. An ['a id] is an identifier whose solver-type
is represented by an inhabitant of type ['a].
All identifier have an unique [index] which is used for comparison,
so that the name of a variable is only there for tracability
and/or pretty-printing. *)
(** {3 Types} *)
type ttype = Type
(** The caml type of solver-types. *)
type 'ty function_descr = private {
fun_vars : ttype id list; (* prenex forall *)
fun_args : 'ty list;
fun_ret : 'ty;
}
(** This represents the solver-type of a function.
Functions can be polymorphic in the variables described in the
[fun_vars] field. *)
type ty_descr = private
| TyVar of ttype id
(** bound variables (i.e should only appear under a quantifier) *)
| TyApp of ttype function_descr id * ty list
(** application of a constant to some arguments *)
and ty = private {
ty : ty_descr;
mutable ty_hash : hash; (** Use Ty.hash instead *)
}
(** These types defines solver-types, i.e the representation of the types
of terms in the solver. Record definition for [type ty] is shown in order
to be able to use the [ty.ty] field in patter matches. Other fields shoud not
be accessed directly, but throught the functions provided by the [Ty] module. *)
(** {3 Terms} *)
type term_descr = private
| Var of ty id
(** bound variables (i.e should only appear under a quantifier) *)
| App of ty function_descr id * ty list * term list
(** application of a constant to some arguments *)
and term = private {
term : term_descr;
t_type : ty;
mutable t_hash : hash; (** Do not use this filed, call Term.hash instead *)
}
(** Types defining terms in the solver. The definition is vary similar to that
of solver-types, except for type arguments of polymorphic functions which
are explicit. This has the advantage that there is a clear and typed distinction
between solver-types and terms, but may lead to some duplication of code
in some places. *)
(** {3 Formulas} *)
type atom_descr = private
(** Atoms *)
| Pred of term
| Equal of term * term
and atom = private {
sign : bool;
atom : atom_descr;
mutable f_hash : hash; (** Use Formula.hash instead *)
}
(** The type of atoms in the solver. The list of free arguments in quantifiers
is a bit tricky, so you should not touch it (see full doc for further
explanations). *)
(** {3 Exceptions} *)
exception Type_mismatch of term * ty * ty
(* Raised when as Type_mismatch(term, actual_type, expected_type) *)
exception Bad_arity of ty function_descr id * ty list * term list
exception Bad_ty_arity of ttype function_descr id * ty list
(** Raised when trying to build an application with wrong arity *)
(** {2 Printing} *)
module Print : sig
(** Pretty printing functions *)
val id : Format.formatter -> 'a id -> unit
val id_ty : Format.formatter -> ty id -> unit
val id_ttype : Format.formatter -> ttype id -> unit
val const_ty : Format.formatter -> ty function_descr id -> unit
val const_ttype : Format.formatter -> ttype function_descr id -> unit
val ty : Format.formatter -> ty -> unit
val fun_ty : Format.formatter -> ty function_descr -> unit
val ttype : Format.formatter -> ttype -> unit
val fun_ttype : Format.formatter -> ttype function_descr -> unit
val term : Format.formatter -> term -> unit
val atom : Format.formatter -> atom -> unit
end
(** {2 Identifiers & Metas} *)
module Id : sig
type 'a t = 'a id
(* Type alias *)
val hash : 'a t -> int
val equal : 'a t -> 'a t -> bool
val compare : 'a t -> 'a t -> int
(** Usual functions for hash/comparison *)
val print : Format.formatter -> 'a t -> unit
(** Printing for variables *)
val prop : ttype function_descr id
val base : ttype function_descr id
(** Constants representing the type for propositions and a default type
for term, respectively. *)
val ttype : string -> ttype id
(** Create a fresh type variable with the given name. *)
val ty : string -> ty -> ty id
(** Create a fresh variable with given name and type *)
val ty_fun : string -> int -> ttype function_descr id
(** Create a fresh type constructor with given name and arity *)
val term_fun : string -> ttype id list -> ty list -> ty -> ty function_descr id
(** [ty_fun name type_vars arg_types return_type] returns a fresh constant symbol,
possibly polymorphic with respect to the variables in [type_vars] (which may appear in the
types in [arg_types] and in [return_type]). *)
end
(** {2 Substitutions} *)
module Subst : sig
(** Module to handle substitutions *)
type ('a, 'b) t
(** The type of substitutions from values of type ['a] to values of type ['b]. *)
val empty : ('a, 'b) t
(** The empty substitution *)
val is_empty : ('a, 'b) t -> bool
(** Test wether a substitution is empty *)
val iter : ('a -> 'b -> unit) -> ('a, 'b) t -> unit
(** Iterates over the bindings of the substitution. *)
val fold : ('a -> 'b -> 'c -> 'c) -> ('a, 'b) t -> 'c -> 'c
(** Fold over the elements *)
val bindings : ('a, 'b) t -> ('a * 'b) list
(** Returns the list of bindings ofa substitution. *)
val exists : ('a -> 'b -> bool) -> ('a, 'b) t -> bool
(** Tests wether the predicate holds for at least one binding. *)
val for_all : ('a -> 'b -> bool) -> ('a, 'b) t -> bool
(** Tests wether the predicate holds for all bindings. *)
val hash : ('b -> int) -> ('a, 'b) t -> int
val compare : ('b -> 'b -> int) -> ('a, 'b) t -> ('a, 'b) t -> int
val equal : ('b -> 'b -> bool) -> ('a, 'b) t -> ('a, 'b) t -> bool
(** Comparison and hash functions, with a comparison/hash function on values as parameter *)
val print :
(Format.formatter -> 'a -> unit) ->
(Format.formatter -> 'b -> unit) ->
Format.formatter -> ('a, 'b) t -> unit
(** Prints the substitution, using the given functions to print keys and values. *)
val choose : ('a, 'b) t -> 'a * 'b
(** Return one binding of the given substitution, or raise Not_found if the substitution is empty.*)
(** {5 Concrete subtitutions } *)
module type S = sig
type 'a key
val get : 'a key -> ('a key, 'b) t -> 'b
(** [get v subst] returns the value associated with [v] in [subst], if it exists.
@raise Not_found if there is no binding for [v]. *)
val mem : 'a key -> ('a key, 'b) t -> bool
(** [get v subst] returns wether there is a value associated with [v] in [subst]. *)
val bind : 'a key -> 'b -> ('a key, 'b) t -> ('a key, 'b) t
(** [bind v t subst] returns the same substitution as [subst] with the additional binding from [v] to [t].
Erases the previous binding of [v] if it exists. *)
val remove : 'a key -> ('a key, 'b) t -> ('a key, 'b) t
(** [remove v subst] returns the same substitution as [subst] except for [v] which is unbound in the returned substitution. *)
end
module Id : S with type 'a key = 'a id
end
(** {2 Types} *)
module Ty : sig
type t = ty
(** Type alias *)
type subst = (ttype id, ty) Subst.t
(** The type of substitutions over types. *)
val hash : t -> int
val equal : t -> t -> bool
val compare : t -> t -> int
(** Usual hash/compare functions *)
val print : Format.formatter -> t -> unit
val prop : ty
val base : ty
(** The type of propositions and individuals *)
val of_id : ttype id -> ty
(** Creates a type from a variable *)
val apply : ttype function_descr id -> ty list -> ty
(** Applies a constant to a list of types *)
val subst : subst -> ty -> ty
(** Substitution over types. *)
end
(** {2 Terms} *)
module Term : sig
type t = term
(** Type alias *)
type subst = (ty id, term) Subst.t
(** The type of substitutions in types. *)
val hash : t -> int
val equal : t -> t -> bool
val compare : t -> t -> int
(** Usual hash/compare functions *)
val print : Format.formatter -> t -> unit
(** Printing functions *)
val of_id : ty id -> term
(** Create a term from a variable *)
val apply : ty function_descr id -> ty list -> term list -> term
(** Applies a constant function to type arguments, then term arguments *)
val subst : Ty.subst -> subst -> term -> term
(** Substitution over types. *)
val replace : term * term -> term -> term
(** [replace (t, t') t''] returns the term [t''] where every occurence of [t]
has been replace by [t']. *)
end
(** {2 Formulas} *)
module Atom : sig
type t = atom
type proof = unit
(** Type alias *)
val hash : t -> int
val equal : t -> t -> bool
val compare : t -> t -> int
(** Usual hash/compare functions *)
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} *)
val pred : term -> atom
(** Create a atom from a term. The given term must have type {!Ty.prop} *)
val neg : atom -> atom
(** Returns the negation of the given atom *)
val norm : atom -> atom * Formula_intf.negated
(** Normalization functions as required by msat. *)
end
module Formula : Msat_tseitin.S with type atom = atom

628
src/smt/type_smt.ml
View file

@ -1,628 +0,0 @@
(* Log&Module Init *)
(* ************************************************************************ *)
module Ast = Dolmen.Term
module Id = Dolmen.Id
module M = Map.Make(Id)
module H = Hashtbl.Make(Id)
module Expr = Expr_smt
(* Types *)
(* ************************************************************************ *)
(* The type of potentially expected result type for parsing an expression *)
type expect =
| Nothing
| Type
| Typed of 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
(* 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;
(* Bound variables (through let constructions) *)
term_lets : Expr.term M.t;
prop_lets : Expr.Formula.t M.t;
(* Typing options *)
expect : expect;
}
(* Exceptions *)
(* ************************************************************************ *)
(* Internal exception *)
exception Found of Ast.t
(* Exception for typing errors *)
exception Typing_error of string * Ast.t
(* Convenience functions *)
let _expected s t = raise (Typing_error (
Format.asprintf "Expected a %s" s, t))
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))
let _fo_term s t = raise (Typing_error (
Format.asprintf "Let-bound variable '%a' is applied to terms" Id.print s, t))
(* Global Environment *)
(* ************************************************************************ *)
(* Global identifier table; stores declared types and aliases. *)
let global_env = H.create 42
let find_global name =
try H.find global_env name
with Not_found -> `Not_found
(* Symbol declarations *)
let decl_ty_cstr id c =
if H.mem global_env id then
Log.debugf 0
(fun k -> k "Symbol '%a' has already been defined, overwriting previous definition" Id.print id);
H.add global_env id (`Ty c);
Log.debugf 1 (fun k -> k "New type constructor : %a" Expr.Print.const_ttype c)
let decl_term id c =
if H.mem global_env id then
Log.debugf 0
(fun k -> k "Symbol '%a' has already been defined, overwriting previous definition" Id.print id);
H.add global_env id (`Term c);
Log.debugf 1 (fun k -> k "New constant : %a" Expr.Print.const_ty c)
(* Symbol definitions *)
let def_ty id args body =
if H.mem global_env id then
Log.debugf 0
(fun k -> k "Symbol '%a' has already been defined, overwriting previous definition" 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
(fun k -> k "Symbol '%a' has already been defined, overwriting previous definition" Id.print id);
H.add global_env id (`Term_alias (ty_args, args, body))
(* Local Environment *)
(* ************************************************************************ *)
(* Make a new empty environment *)
let empty_env ?(expect=Nothing) () = {
type_vars = M.empty;
term_vars = M.empty;
term_lets = M.empty;
prop_lets = M.empty;
expect;
}
(* Generate new fresh names for shadowed variables *)
let new_name pre =
let i = ref 0 in
(fun () -> incr i; pre ^ (string_of_int !i))
let new_ty_name = new_name "ty#"
let new_term_name = new_name "term#"
(* Add local variables to environment *)
let add_type_var env id v =
let v' =
if M.mem id env.type_vars then
Expr.Id.ttype (new_ty_name ())
else
v
in
Log.debugf 1
(fun k -> k "New binding : %a -> %a" Id.print id Expr.Print.id_ttype v');
v', { env with type_vars = M.add id v' env.type_vars }
let add_type_vars env l =
let l', env' = List.fold_left (fun (l, acc) (id, v) ->
let v', acc' = add_type_var acc id v in
v' :: l, acc') ([], env) l in
List.rev l', env'
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)
else
v
in
Log.debugf 1
(fun k -> k "New binding : %a -> %a" Id.print id Expr.Print.id_ty v');
v', { env with term_vars = M.add id v' env.term_vars }
let find_var env name =
try `Ty (M.find name env.type_vars)
with Not_found ->
begin
try
`Term (M.find name env.term_vars)
with Not_found ->
`Not_found
end
(* Add local bound variables to env *)
let add_let_term env id t =
Log.debugf 1
(fun k -> k "New let-binding : %s -> %a" id.Id.name 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
(fun k -> k "New let-binding : %s -> %a" id.Id.name Expr.Formula.print t);
{ env with prop_lets = M.add id t env.prop_lets }
let find_let env name =
try `Term (M.find name env.term_lets)
with Not_found ->
begin
try
`Prop (M.find name env.prop_lets)
with Not_found ->
`Not_found
end
(* Some helper functions *)
(* ************************************************************************ *)
let flat_map f l = List.flatten (List.map f l)
let take_drop n l =
let rec aux acc = function
| 0, res | _, ([] as res) -> List.rev acc, res
| m, x :: r -> aux (x :: acc) (m - 1, r)
in
aux [] (n, l)
let diagonal l =
let rec single x acc = function
| [] -> acc
| y :: r -> single x ((x, y) :: acc) r
and aux acc = function
| [] -> acc
| x :: r -> aux (single x acc r) r
in
aux [] l
(* Wrappers for expression building *)
(* ************************************************************************ *)
let arity f =
List.length Expr.(f.id_type.fun_vars) +
List.length 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
let term_apply _env ast f ty_args t_args =
try
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') ->
_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
| subst ->
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
| 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
| t_subst ->
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
| exception Invalid_argument _ ->
_bad_arity id.Id.name (List.length f_ty_args + List.length f_t_args) ast_term
let make_eq ast_term a b =
try
Expr.Formula.make_atom @@ Expr.Atom.eq a b
with 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') ->
_type_mismatch t ty ty' ast_term
let infer env s args =
match env.expect with
| Nothing -> `Nothing
| Type ->
let n = List.length args in
let res = 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)
in
let res = Expr.Id.term_fun s.Id.name [] (replicate [] n) ty in
decl_term s res;
`Term res
(* Expression parsing *)
(* ************************************************************************ *)
[@@@ocaml.warning "-9"]
let rec parse_expr (env : env) t =
match t with
(* Base Types *)
| { Ast.term = Ast.Builtin Ast.Ttype } ->
Ttype
| { Ast.term = Ast.Symbol { Id.name = "Bool" } } ->
Ty (Expr_smt.Ty.prop)
(* Basic formulas *)
| { Ast.term = Ast.App ({ Ast.term = Ast.Builtin Ast.True }, []) }
| { Ast.term = Ast.Builtin Ast.True } ->
Formula 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
| { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.And}, l) }
| { Ast.term = Ast.App ({Ast.term = Ast.Symbol { Id.name = "and" }}, l) } ->
Formula (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.Symbol { Id.name = "or" }}, l) } ->
Formula (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))
| _ -> _bad_arity "xor" 2 t
end
| ({ Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Imply}, l) } as t)
| ({ Ast.term = Ast.App ({Ast.term = Ast.Symbol { Id.name = "=>" }}, 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_imply f g)
| _ -> _bad_arity "=>" 2 t
end
| { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Equiv}, 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_equiv f g)
| _ -> _bad_arity "<=>" 2 t
end
| ({ Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Not}, l) } as t)
| ({ Ast.term = Ast.App ({Ast.term = Ast.Symbol { Id.name = "not" }}, l) } as t) ->
begin match l with
| [p] ->
Formula (Expr.Formula.make_not (parse_formula env p))
| _ -> _bad_arity "not" 1 t
end
(* (Dis)Equality *)
| ({ Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Eq}, l) } as t)
| ({ Ast.term = Ast.App ({Ast.term = Ast.Symbol { Id.name = "=" }}, l) } as t) ->
begin match l with
| [a; b] ->
Formula (
make_eq t
(parse_term env a)
(parse_term env b)
)
| _ -> _bad_arity "=" 2 t
end
| { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Distinct}, args) } as t ->
let l' = List.map (parse_term env) args in
let l'' = diagonal l' in
Formula (
Expr.Formula.make_and
(List.map (fun (a, b) ->
Expr.Formula.make_not
(make_eq t a b)) l'')
)
(* General case: application *)
| { Ast.term = Ast.Symbol s } as ast ->
parse_app env ast s []
| { Ast.term = Ast.App ({ Ast.term = Ast.Symbol s }, l) } as ast ->
parse_app env ast s l
(* Local bindings *)
| { Ast.term = Ast.Binder (Ast.Let, vars, f) } ->
parse_let env f vars
(* Other cases *)
| ast -> raise (Typing_error ("Couldn't parse the expression", ast))
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)
| _ -> _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)
end
| t -> _expected "(typed) variable" t
and parse_quant_vars env l =
let ttype_vars, typed_vars, env' = List.fold_left (
fun (l1, l2, acc) v ->
match parse_var acc v with
| `Ty (id, v') ->
let v'', acc' = add_type_var acc id v' in
(v'' :: l1, l2, acc')
| `Term (id, v') ->
let v'', acc' = add_term_var acc id v' in
(l1, v'' :: l2, acc')
) ([], [], env) l in
List.rev ttype_vars, List.rev typed_vars, env'
and parse_let env f = function
| [] -> parse_expr env f
| x :: r ->
begin match x with
| { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Eq}, [
{ Ast.term = Ast.Symbol s }; e]) } ->
let t = parse_term env e in
let env' = add_let_term env s t in
parse_let env' f r
| { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Equiv}, [
{ Ast.term = Ast.Symbol s }; e]) } ->
let t = parse_formula env e in
let env' = add_let_prop env s t in
parse_let env' f r
| { Ast.term = Ast.Colon ({ Ast.term = Ast.Symbol s }, e) } ->
begin match parse_expr env e with
| Term t ->
let env' = add_let_term env s t in
parse_let env' f r
| Formula t ->
let env' = add_let_prop env s t in
parse_let env' f r
| _ -> _expected "term of formula" e
end
| t -> _expected "let-binding" t
end
and parse_app env ast s args =
match find_let env s with
| `Term t ->
if args = [] then Term t
else _fo_term s ast
| `Prop p ->
if args = [] then Formula p
else _fo_term s ast
| `Not_found ->
begin match find_var env s with
| `Ty f ->
if args = [] then Ty (Expr.Ty.of_id f)
else _fo_term s ast
| `Term f ->
if args = [] then Term (Expr.Term.of_id f)
else _fo_term s ast
| `Not_found ->
begin match find_global s with
| `Ty f ->
parse_app_ty env ast f args
| `Term f ->
parse_app_term env ast f args
| `Ty_alias (f_args, body) ->
parse_app_subst_ty env ast s args f_args body
| `Term_alias (f_ty_args, f_t_args, body) ->
parse_app_subst_term env ast s args f_ty_args f_t_args body
| `Not_found ->
begin match infer env s args with
| `Ty f -> parse_app_ty env ast f args
| `Term f -> parse_app_term env ast f args
| `Nothing ->
raise (Typing_error (
Format.asprintf "Scoping error: '%a' not found" Id.print s, ast))
end
end
end
and parse_app_ty env ast f args =
let l = List.map (parse_ty env) args in
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 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
Term (term_apply env ast f ty_args t_args)
and parse_app_subst_ty env ast id args f_args body =
let l = List.map (parse_ty env) args in
Ty (ty_subst ast id l f_args body)
and parse_app_subst_term env ast id args f_ty_args f_t_args body =
let n = List.length f_ty_args 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
Term (term_subst ast id ty_args t_args f_ty_args f_t_args body)
and parse_ty env ast =
match parse_expr { env with expect = Type } ast with
| Ty ty -> ty
| _ -> _expected "type" ast
and parse_term env ast =
match parse_expr { env with expect = Typed 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) ->
make_pred ast t
| Formula p -> p
| _ -> _expected "formula" ast
let parse_ttype_var env t =
match parse_var env t with
| `Ty (id, v) -> (id, v)
| `Term _ -> _expected "type variable" t
let rec parse_sig_quant env = function
| { Ast.term = Ast.Binder (Ast.Pi, vars, t) } ->
let ttype_vars = List.map (parse_ttype_var env) vars in
let ttype_vars', env' = add_type_vars env ttype_vars in
let l = List.combine vars ttype_vars' in
parse_sig_arrow l [] env' t
| t ->
parse_sig_arrow [] [] env t
and parse_sig_arrow ttype_vars (ty_args: (Ast.t * res) list) env = function
| { Ast.term = Ast.Binder (Ast.Arrow, args, ret) } ->
let t_args = parse_sig_args env args in
parse_sig_arrow ttype_vars (ty_args @ t_args) env ret
| t ->
begin match parse_expr env t with
| Ttype ->
begin match ttype_vars with
| (h, _) :: _ ->
raise (Typing_error (
"Type constructor signatures cannot have quantified type variables", h))
| [] ->
let aux n = function
| (_, Ttype) -> n + 1
| (ast, _) -> raise (Found ast)
in
begin
match List.fold_left aux 0 ty_args with
| n -> `Ty_cstr n
| exception Found err ->
raise (Typing_error (
Format.asprintf
"Type constructor signatures cannot have non-ttype arguments,", err))
end
end
| Ty ret ->
let aux acc = function
| (_, Ty t) -> t :: acc
| (ast, _) -> raise (Found ast)
in
begin
match List.fold_left aux [] ty_args with
| exception Found err -> _expected "type" err
| l -> `Fun_ty (List.map snd ttype_vars, List.rev l, ret)
end
| _ -> _expected "Ttype of type" t
end
and parse_sig_args env l =
flat_map (parse_sig_arg env) l
and parse_sig_arg env = function
| { Ast.term = Ast.App ({ Ast.term = Ast.Builtin Ast.Product}, l) } ->
List.map (fun x -> x, parse_expr env x) l
| t ->
[t, parse_expr env t]
let parse_sig = parse_sig_quant
let rec parse_fun ty_args t_args env = function
| { Ast.term = Ast.Binder (Ast.Fun, l, ret) } ->
let ty_args', t_args', env' = parse_quant_vars env l in
parse_fun (ty_args @ ty_args') (t_args @ t_args') env' ret
| ast ->
begin match parse_expr env ast with
| Ttype -> raise (Typing_error ("Cannot redefine Ttype", ast))
| Ty body ->
if t_args = [] then `Ty (ty_args, body)
else _expected "term" ast
| Term body -> `Term (ty_args, t_args, body)
| Formula _ -> _expected "type or term" ast
end
[@@@ocaml.warning "+9"]
(* High-level parsing functions *)
(* ************************************************************************ *)
let decl id t =
let env = empty_env () in
Log.debugf 5
(fun k -> k "Typing declaration: %s : %a" 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)
| `Fun_ty (vars, args, ret) ->
decl_term id (Expr.Id.term_fun id.Id.name vars args ret)
end
let def id t =
let env = empty_env () in
Log.debugf 5
(fun k -> k "Typing definition: %s = %a" id.Id.name Ast.print t);
begin match parse_fun [] [] env t with
| `Ty (ty_args, body) -> def_ty id ty_args body
| `Term (ty_args, t_args, body) -> def_term id ty_args t_args body
end
let formula t =
let env = empty_env () in
Log.debugf 5 (fun k -> k "Typing top-level formula: %a" Ast.print t);
parse_formula env t
let assumptions t =
let cnf = Expr.Formula.make_cnf (formula t) in
List.map (function
| [ x ] -> x
| _ -> assert false
) cnf
let antecedent t =
Expr.Formula.make_cnf (formula t)
let consequent t =
Expr.Formula.make_cnf (Expr.Formula.make_not (formula t))

7
src/smt/type_smt.mli
View file

@ -1,7 +0,0 @@
(** Typechecking of terms from Dolmen.Term.t
This module provides functions to parse terms from the untyped syntax tree
defined in Dolmen, and generate formulas as defined in the Expr_smt module. *)
include Minismt.Type.S with type atom := Expr_smt.Atom.t

90
src/smt/unionfind.ml
View file

@ -1,90 +0,0 @@
(*
MSAT is free software, using the Apache license, see file LICENSE
Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
module type OrderedType = sig
type t
val compare : t -> t -> int
end
(* Union-find Module *)
module Make(T : OrderedType) = struct
exception Unsat of T.t * T.t
type var = T.t
module M = Map.Make(T)
(* TODO: better treatment of inequalities *)
type t = {
rank : int M.t;
forbid : ((var * var) list);
mutable parent : var M.t;
}
let empty = {
rank = M.empty;
forbid = [];
parent = M.empty;
}
let find_map m i default =
try
M.find i m
with Not_found ->
default
let rec find_aux f i =
let fi = find_map f i i in
if fi = i then
(f, i)
else
let f, r = find_aux f fi in
let f = M.add i r f in
(f, r)
let find h x =
let f, cx = find_aux h.parent x in
h.parent <- f;
cx
(* Highly inefficient 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
{ rank = M.add cx (rx + 1) h.rank;
parent = M.add cy cx h.parent;
forbid = h.forbid; }
end else
h
let union h x y = possible (union_aux h x y)
let forbid h x y =
let cx = find h x in
let cy = find h y in
if cx = cy then
raise (Unsat (x, y))
else
{ h with forbid = (x, y) :: h.forbid }
end

20
src/smt/unionfind.mli
View file

@ -1,20 +0,0 @@
(*
MSAT is free software, using the Apache license, see file LICENSE
Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
module type OrderedType = sig
type t
val compare : t -> t -> int
end
module Make(T : OrderedType) : sig
type t
exception Unsat of T.t * T.t
val empty : t
val find : t -> T.t -> T.t
val union : t -> T.t -> T.t -> t
val forbid : t -> T.t -> T.t -> t
end

11
src/solver/dune
View file

@ -1,11 +0,0 @@
(library
(name minismt)
(public_name minismt)
(libraries msat dolmen)
(synopsis "minismt")
(flags :standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Msat)
(ocamlopt_flags :standard -O3 -bin-annot
-unbox-closures -unbox-closures-factor 20)
)

15
src/solver/mcsolver.ml
View file

@ -1,15 +0,0 @@
(*
MSAT is free software, using the Apache license, see file LICENSE
Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
module type S = Msat.S
module Make (E : Expr_intf.S)
(Th : Plugin_intf.S with type term = E.Term.t
and type formula = E.Formula.t
and type proof = E.proof)
= Msat.Make (Make_mcsat_expr(E)) (Th)

23
src/solver/mcsolver.mli
View file

@ -1,23 +0,0 @@
(*
MSAT is free software, using the Apache license, see file LICENSE
Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
(** Create McSat solver
This module provides a functor to create an McSAt solver.
*)
module type S = Msat.S
(** The interface exposed by the solver. *)
module Make (E : Expr_intf.S)
(Th : Plugin_intf.S with type term = E.Term.t
and type formula = E.Formula.t
and type proof = E.proof)
: S with type term = E.Term.t
and type formula = E.Formula.t
and type Proof.lemma = E.proof
(** Functor to create a solver parametrised by the atomic formulas and a theory. *)

81
src/solver/solver.ml
View file

@ -1,81 +0,0 @@
(**************************************************************************)
(* *)
(* Alt-Ergo Zero *)
(* *)
(* 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 *)
(* *)
(**************************************************************************)
module type S = Msat.S
module DummyTheory(F : Formula_intf.S) = struct
(* We don't have anything to do since the SAT Solver already
* does propagation and conflict detection *)
type formula = F.t
type proof = F.proof
type level = unit
let dummy = ()
let current_level () = ()
let assume _ = Theory_intf.Sat
let backtrack _ = ()
let if_sat _ = Theory_intf.Sat
end
module Plugin(E : Formula_intf.S)
(Th : Theory_intf.S with type formula = E.t and type proof = E.proof) = struct
type term = E.t
type formula = E.t
type proof = Th.proof
type level = Th.level
let dummy = Th.dummy
let current_level = Th.current_level
let assume_get get =
function i ->
match get i with
| Plugin_intf.Lit f -> f
| _ -> assert false
let assume_propagate propagate =
fun f l proof ->
propagate f (Plugin_intf.Consequence (l, proof))
let mk_slice s = {
Theory_intf.start = s.Plugin_intf.start;
length = s.Plugin_intf.length;
get = assume_get s.Plugin_intf.get;
push = s.Plugin_intf.push;
propagate = assume_propagate s.Plugin_intf.propagate;
}
let assume s = Th.assume (mk_slice s)
let backtrack = Th.backtrack
let if_sat s = Th.if_sat (mk_slice s)
(* McSat specific functions *)
let assign _ = assert false
let iter_assignable _ _ = ()
let eval _ = Plugin_intf.Unknown
end
module Make (E : Formula_intf.S)
(Th : Theory_intf.S with type formula = E.t and type proof = E.proof)
= Msat.Make (Make_smt_expr(E)) (Plugin(E)(Th))

30
src/solver/solver.mli
View file

@ -1,30 +0,0 @@
(*
MSAT is free software, using the Apache license, see file LICENSE
Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
(** Create SAT/SMT Solvers
This module provides a functor to create an SMT solver. Additionally, it also
gives a functor that produce an adequate empty theory that can be given to the [Make]
functor in order to create a pure SAT solver.
*)
module type S = Msat.S
(** The interface of instantiated solvers. *)
module DummyTheory(F : Formula_intf.S) :
Theory_intf.S with type formula = F.t
and type proof = F.proof
(** Simple case where the theory is empty and
the proof type is the one given in the formula interface *)
module Make (F : Formula_intf.S)
(Th : Theory_intf.S with type formula = F.t
and type proof = F.proof)
: S with type formula = F.t
and type Proof.lemma = F.proof
(** Functor to create a SMT Solver parametrised by the atomic
formulas and a theory. *)

28
src/solver/type.ml
View file

@ -1,28 +0,0 @@
(** Typechecking of terms from Dolmen.Term.t
This module defines the requirements for typing expre'ssions from dolmen. *)
module type S = sig
type atom
(** The type of atoms that will be fed to tha sovler. *)
exception Typing_error of string * Dolmen.Term.t
(** Exception raised during typechecking. *)
val decl : Dolmen.Id.t -> Dolmen.Term.t -> unit
(** New declaration, i.e an identifier and its type. *)
val def : Dolmen.Id.t -> Dolmen.Term.t -> unit
(** New definition, i.e an identifier and the term it is equal to. *)
val assumptions : Dolmen.Term.t -> atom list
(** Parse a list of local assumptions. *)
val consequent : Dolmen.Term.t -> atom list list
val antecedent : Dolmen.Term.t -> atom list list
(** Parse a formula, and return a cnf ready to be given to the solver.
Consequent is for hypotheses (left of the sequent), while antecedent
is for goals (i.e formulas on the right of a sequent). *)
end

4
tests/dune
View file

@ -1,8 +1,8 @@
(executable
(name test_api)
(libraries msat msat.tseitin msat.backend minismt.sat minismt.smt minismt.mcsat dolmen)
(flags :standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string)
(libraries msat msat_sat)
(flags :standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Msat)
(ocamlopt_flags :standard -O3 -color always
-unbox-closures -unbox-closures-factor 20)
)

6
tests/run
View file

@ -1,13 +1,13 @@
#!/bin/bash
CURDIR=`dirname $0`
SOLVER="$CURDIR/../msat.exe"
SOLVER="$CURDIR/../msat.sh"
solvertest () {
for f in `find -L $1 -type f -name '*.cnf' -o -name '*.smt2'`
for f in `find -L $1 -type f -name '*.cnf' # -o -name '*.smt2'`
do
echo -ne "\r\033[KTesting $f..."
"$SOLVER" -s $3 -time 30s -size 1G -check $f | grep $2
"$SOLVER" -time 30s -size 1G -check $f | grep $2
RET=$?
if [ $RET -ne 0 ];
then

7
tests/test_api.ml
View file

@ -6,10 +6,7 @@ Copyright 2014 Simon Cruanes
(* Tests that require the API *)
open Msat
module F = Minismt_sat.Expr
module T = Msat_tseitin.Make(F)
module F = Msat_sat.Expr
let (|>) x f = f x
@ -48,7 +45,7 @@ end
let mk_solver (): (module BASIC_SOLVER) =
let module S = struct
include Minismt_sat
include Msat_sat
let create() = create()
let solve st ?assumptions () =
match solve st ?assumptions() with