From 05e25063626086ba3bc09aa0ccf73b03169e0d8f Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 18 Jan 2019 19:39:12 -0600 Subject: [PATCH] refactor: remove `minismt` things, make simple `msat.sh` --- Makefile | 5 +- dune-project | 1 + minismt.opam | 22 - msat.exe | 1 - msat.opam | 2 +- msat.sh | 3 + src/core/Msat.ml | 2 + src/core/Plugin_intf.ml | 19 + src/core/Theory_intf.ml | 12 + src/main/Dimacs_lex.mll | 20 + src/main/Dimacs_parse.mly | 41 ++ src/main/dune | 10 +- src/main/main.ml | 104 +--- src/mcsat/Minismt_mcsat.ml | 13 - src/mcsat/Minismt_mcsat.mli | 8 - src/mcsat/README.md | 68 --- src/mcsat/backtrack.ml | 99 ---- src/mcsat/backtrack.mli | 77 --- src/mcsat/dune | 12 - src/mcsat/eclosure.ml | 232 -------- src/mcsat/eclosure.mli | 60 --- src/mcsat/plugin_mcsat.ml | 200 ------- src/sat/{Minismt_sat.ml => Msat_sat.ml} | 4 +- src/sat/{Minismt_sat.mli => Msat_sat.mli} | 3 +- src/sat/dune | 10 +- src/sat/type_sat.ml | 90 ---- src/sat/type_sat.mli | 12 - src/smt/Minismt_smt.ml | 13 - src/smt/Minismt_smt.mli | 11 - src/smt/dune | 12 - src/smt/expr_smt.ml | 525 ------------------ src/smt/expr_smt.mli | 326 ----------- src/smt/type_smt.ml | 628 ---------------------- src/smt/type_smt.mli | 7 - src/smt/unionfind.ml | 90 ---- src/smt/unionfind.mli | 20 - src/solver/dune | 11 - src/solver/mcsolver.ml | 15 - src/solver/mcsolver.mli | 23 - src/solver/solver.ml | 81 --- src/solver/solver.mli | 30 -- src/solver/type.ml | 28 - tests/dune | 4 +- tests/run | 6 +- tests/test_api.ml | 7 +- 45 files changed, 137 insertions(+), 2830 deletions(-) delete mode 100644 minismt.opam delete mode 120000 msat.exe create mode 100755 msat.sh create mode 100644 src/main/Dimacs_lex.mll create mode 100644 src/main/Dimacs_parse.mly delete mode 100644 src/mcsat/Minismt_mcsat.ml delete mode 100644 src/mcsat/Minismt_mcsat.mli delete mode 100644 src/mcsat/README.md delete mode 100644 src/mcsat/backtrack.ml delete mode 100644 src/mcsat/backtrack.mli delete mode 100644 src/mcsat/dune delete mode 100644 src/mcsat/eclosure.ml delete mode 100644 src/mcsat/eclosure.mli delete mode 100644 src/mcsat/plugin_mcsat.ml rename src/sat/{Minismt_sat.ml => Msat_sat.ml} (58%) rename src/sat/{Minismt_sat.mli => Msat_sat.mli} (80%) delete mode 100644 src/sat/type_sat.ml delete mode 100644 src/sat/type_sat.mli delete mode 100644 src/smt/Minismt_smt.ml delete mode 100644 src/smt/Minismt_smt.mli delete mode 100644 src/smt/dune delete mode 100644 src/smt/expr_smt.ml delete mode 100644 src/smt/expr_smt.mli delete mode 100644 src/smt/type_smt.ml delete mode 100644 src/smt/type_smt.mli delete mode 100644 src/smt/unionfind.ml delete mode 100644 src/smt/unionfind.mli delete mode 100644 src/solver/dune delete mode 100644 src/solver/mcsolver.ml delete mode 100644 src/solver/mcsolver.mli delete mode 100644 src/solver/solver.ml delete mode 100644 src/solver/solver.mli delete mode 100644 src/solver/type.ml diff --git a/Makefile b/Makefile index e5d6c0a7..3391828d 100644 --- a/Makefile +++ b/Makefile @@ -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 diff --git a/dune-project b/dune-project index 7655de07..977e7d75 100644 --- a/dune-project +++ b/dune-project @@ -1 +1,2 @@ (lang dune 1.1) +(using menhir 1.0) diff --git a/minismt.opam b/minismt.opam deleted file mode 100644 index 0f2f75a4..00000000 --- a/minismt.opam +++ /dev/null @@ -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/" - diff --git a/msat.exe b/msat.exe deleted file mode 120000 index cceb9ac3..00000000 --- a/msat.exe +++ /dev/null @@ -1 +0,0 @@ -_build/default/src/main/main.exe \ No newline at end of file diff --git a/msat.opam b/msat.opam index b52afa20..d5c45b44 100644 --- a/msat.opam +++ b/msat.opam @@ -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" diff --git a/msat.sh b/msat.sh new file mode 100755 index 00000000..d111c6b0 --- /dev/null +++ b/msat.sh @@ -0,0 +1,3 @@ +#!/bin/sh + +exec dune exec src/main/main.exe -- $@ diff --git a/src/core/Msat.ml b/src/core/Msat.ml index daa470c2..6b15cf2f 100644 --- a/src/core/Msat.ml +++ b/src/core/Msat.ml @@ -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 diff --git a/src/core/Plugin_intf.ml b/src/core/Plugin_intf.ml index 92d1b2e4..2584eb52 100644 --- a/src/core/Plugin_intf.ml +++ b/src/core/Plugin_intf.ml @@ -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 diff --git a/src/core/Theory_intf.ml b/src/core/Theory_intf.ml index b465f4c9..f0183342 100644 --- a/src/core/Theory_intf.ml +++ b/src/core/Theory_intf.ml @@ -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 diff --git a/src/main/Dimacs_lex.mll b/src/main/Dimacs_lex.mll new file mode 100644 index 00000000..67850c1f --- /dev/null +++ b/src/main/Dimacs_lex.mll @@ -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 } diff --git a/src/main/Dimacs_parse.mly b/src/main/Dimacs_parse.mly new file mode 100644 index 00000000..3ad9341b --- /dev/null +++ b/src/main/Dimacs_parse.mly @@ -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 LIT +%token ZERO +%token P CNF EOF + +%start file +%type 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 } diff --git a/src/main/dune b/src/main/dune index 2c6fd9e9..7b96abd7 100644 --- a/src/main/dune +++ b/src/main/dune @@ -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)) diff --git a/src/main/main.ml b/src/main/main.ml index 008592f2..28400e72 100644 --- a/src/main/main.ml +++ b/src/main/main.ml @@ -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), "[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 diff --git a/src/mcsat/Minismt_mcsat.ml b/src/mcsat/Minismt_mcsat.ml deleted file mode 100644 index a7f01e92..00000000 --- a/src/mcsat/Minismt_mcsat.ml +++ /dev/null @@ -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) - diff --git a/src/mcsat/Minismt_mcsat.mli b/src/mcsat/Minismt_mcsat.mli deleted file mode 100644 index a6de15ae..00000000 --- a/src/mcsat/Minismt_mcsat.mli +++ /dev/null @@ -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 - diff --git a/src/mcsat/README.md b/src/mcsat/README.md deleted file mode 100644 index 80ab1a01..00000000 --- a/src/mcsat/README.md +++ /dev/null @@ -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)$ - diff --git a/src/mcsat/backtrack.ml b/src/mcsat/backtrack.ml deleted file mode 100644 index aff629cc..00000000 --- a/src/mcsat/backtrack.ml +++ /dev/null @@ -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 - diff --git a/src/mcsat/backtrack.mli b/src/mcsat/backtrack.mli deleted file mode 100644 index 6480cf63..00000000 --- a/src/mcsat/backtrack.mli +++ /dev/null @@ -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 diff --git a/src/mcsat/dune b/src/mcsat/dune deleted file mode 100644 index b3556847..00000000 --- a/src/mcsat/dune +++ /dev/null @@ -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) - ) - - diff --git a/src/mcsat/eclosure.ml b/src/mcsat/eclosure.ml deleted file mode 100644 index fb53655d..00000000 --- a/src/mcsat/eclosure.ml +++ /dev/null @@ -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 diff --git a/src/mcsat/eclosure.mli b/src/mcsat/eclosure.mli deleted file mode 100644 index d4d5f32c..00000000 --- a/src/mcsat/eclosure.mli +++ /dev/null @@ -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 - diff --git a/src/mcsat/plugin_mcsat.ml b/src/mcsat/plugin_mcsat.ml deleted file mode 100644 index d1c588c7..00000000 --- a/src/mcsat/plugin_mcsat.ml +++ /dev/null @@ -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 - diff --git a/src/sat/Minismt_sat.ml b/src/sat/Msat_sat.ml similarity index 58% rename from src/sat/Minismt_sat.ml rename to src/sat/Msat_sat.ml index cbb2b082..1fc3d1ee 100644 --- a/src/sat/Minismt_sat.ml +++ b/src/sat/Msat_sat.ml @@ -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)) diff --git a/src/sat/Minismt_sat.mli b/src/sat/Msat_sat.mli similarity index 80% rename from src/sat/Minismt_sat.mli rename to src/sat/Msat_sat.mli index 9dbd63f1..c28f5032 100644 --- a/src/sat/Minismt_sat.mli +++ b/src/sat/Msat_sat.mli @@ -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. *) diff --git a/src/sat/dune b/src/sat/dune index 650ba4c3..c321e17c 100644 --- a/src/sat/dune +++ b/src/sat/dune @@ -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) ) - diff --git a/src/sat/type_sat.ml b/src/sat/type_sat.ml deleted file mode 100644 index b809cb4f..00000000 --- a/src/sat/type_sat.ml +++ /dev/null @@ -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 - diff --git a/src/sat/type_sat.mli b/src/sat/type_sat.mli deleted file mode 100644 index a088602c..00000000 --- a/src/sat/type_sat.mli +++ /dev/null @@ -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 - diff --git a/src/smt/Minismt_smt.ml b/src/smt/Minismt_smt.ml deleted file mode 100644 index 473b12de..00000000 --- a/src/smt/Minismt_smt.ml +++ /dev/null @@ -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) - diff --git a/src/smt/Minismt_smt.mli b/src/smt/Minismt_smt.mli deleted file mode 100644 index f81b5277..00000000 --- a/src/smt/Minismt_smt.mli +++ /dev/null @@ -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 - diff --git a/src/smt/dune b/src/smt/dune deleted file mode 100644 index c2bd637f..00000000 --- a/src/smt/dune +++ /dev/null @@ -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) - ) - - diff --git a/src/smt/expr_smt.ml b/src/smt/expr_smt.ml deleted file mode 100644 index f3b8961f..00000000 --- a/src/smt/expr_smt.ml +++ /dev/null @@ -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 "@[%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 = ""; id_type = Type; } - - let ty = - { ty = TyVar id_ttype; ty_hash = -1; } - - let id = - { index = -2; id_name = ""; 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) - diff --git a/src/smt/expr_smt.mli b/src/smt/expr_smt.mli deleted file mode 100644 index 03f0b07c..00000000 --- a/src/smt/expr_smt.mli +++ /dev/null @@ -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 - diff --git a/src/smt/type_smt.ml b/src/smt/type_smt.ml deleted file mode 100644 index 5dbe3837..00000000 --- a/src/smt/type_smt.ml +++ /dev/null @@ -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)) - diff --git a/src/smt/type_smt.mli b/src/smt/type_smt.mli deleted file mode 100644 index 1613debb..00000000 --- a/src/smt/type_smt.mli +++ /dev/null @@ -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 - diff --git a/src/smt/unionfind.ml b/src/smt/unionfind.ml deleted file mode 100644 index ab81a1ad..00000000 --- a/src/smt/unionfind.ml +++ /dev/null @@ -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 diff --git a/src/smt/unionfind.mli b/src/smt/unionfind.mli deleted file mode 100644 index adf2cd25..00000000 --- a/src/smt/unionfind.mli +++ /dev/null @@ -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 - diff --git a/src/solver/dune b/src/solver/dune deleted file mode 100644 index 31c93320..00000000 --- a/src/solver/dune +++ /dev/null @@ -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) - ) - diff --git a/src/solver/mcsolver.ml b/src/solver/mcsolver.ml deleted file mode 100644 index f6eb0c68..00000000 --- a/src/solver/mcsolver.ml +++ /dev/null @@ -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) - - diff --git a/src/solver/mcsolver.mli b/src/solver/mcsolver.mli deleted file mode 100644 index 51f05b8a..00000000 --- a/src/solver/mcsolver.mli +++ /dev/null @@ -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. *) - diff --git a/src/solver/solver.ml b/src/solver/solver.ml deleted file mode 100644 index d06de2e8..00000000 --- a/src/solver/solver.ml +++ /dev/null @@ -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)) - - diff --git a/src/solver/solver.mli b/src/solver/solver.mli deleted file mode 100644 index 77efd675..00000000 --- a/src/solver/solver.mli +++ /dev/null @@ -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. *) - diff --git a/src/solver/type.ml b/src/solver/type.ml deleted file mode 100644 index 693f35ce..00000000 --- a/src/solver/type.ml +++ /dev/null @@ -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 diff --git a/tests/dune b/tests/dune index 34c62686..6e357a4c 100644 --- a/tests/dune +++ b/tests/dune @@ -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) ) diff --git a/tests/run b/tests/run index 463ab373..a8c33d98 100755 --- a/tests/run +++ b/tests/run @@ -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 diff --git a/tests/test_api.ml b/tests/test_api.ml index 838ceed0..89e8cafb 100644 --- a/tests/test_api.ml +++ b/tests/test_api.ml @@ -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