diff --git a/src/backend/Backend_intf.ml b/src/backend/Backend_intf.ml deleted file mode 100644 index 9cfff729..00000000 --- a/src/backend/Backend_intf.ml +++ /dev/null @@ -1,27 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -(** Backend interface - - This modules defines the interface of the modules providing - export of proofs. -*) - -module type S = sig - (** Proof exporting - - Currently, exporting a proof means printing it into a file - according to the conventions of a given format. - *) - - type t - (** The type of proofs. *) - - val print : Format.formatter -> t -> unit - (** A function for printing proofs in the desired format. *) - -end - diff --git a/src/backend/Dimacs.ml b/src/backend/Dimacs.ml deleted file mode 100644 index 61576ce5..00000000 --- a/src/backend/Dimacs.ml +++ /dev/null @@ -1,50 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -module type S = sig - type st - - type clause - (** The type of clauses *) - - val export : - st -> - Format.formatter -> - clauses:clause Vec.t -> - unit -end - -module Make(St : Sidekick_sat.S) = struct - type st = St.t - - (* Dimacs & iCNF export *) - let export_vec name fmt vec = - Format.fprintf fmt "c %s@,%a@," name (Vec.print ~sep:"" St.Clause.pp_dimacs) vec - - let export_assumption fmt vec = - Format.fprintf fmt "c Local assumptions@,a %a@," St.Clause.pp_dimacs vec - - let map_filter_learnt c = - if St.Clause.is_learnt c then Some c else None - - let filter_vec learnt = - let lemmas = Vec.make (Vec.size learnt) St.Clause.dummy in - Vec.iter (fun c -> - match map_filter_learnt c with - | None -> () - | Some d -> Vec.push lemmas d - ) learnt; - lemmas - - let export st fmt ~clauses : unit = - (* Number of atoms and clauses *) - let n = St.n_vars st in - let m = Vec.size clauses in - Format.fprintf fmt - "@[p cnf %d %d@,%a@]@." n m - (export_vec "Clauses") clauses -end - diff --git a/src/backend/Dimacs.mli b/src/backend/Dimacs.mli deleted file mode 100644 index af94396b..00000000 --- a/src/backend/Dimacs.mli +++ /dev/null @@ -1,32 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -(** Dimacs backend for problems - - This module provides functiosn to export problems to the dimacs and - iCNF formats. -*) - -module type S = sig - type st - - type clause - (** The type of clauses *) - - val export : - st -> - Format.formatter -> - clauses:clause Vec.t -> - unit - (** Export the given clause vectors to the dimacs format. - The arguments should be transmitted directly from the corresponding - function of the {Internal} module. *) - -end - -module Make(St: Sidekick_sat.S) : S with type clause := St.clause and type st = St.t -(** Functor to create a module for exporting probems to the dimacs (& iCNF) formats. *) - diff --git a/src/backend/Dot.ml b/src/backend/Dot.ml deleted file mode 100644 index c33bc9ec..00000000 --- a/src/backend/Dot.ml +++ /dev/null @@ -1,150 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -(** Output interface for the backend *) -module type S = Backend_intf.S - -(** Input module for the backend *) -module type Arg = sig - - type atom - - type hyp - type lemma - type assumption - (** Types for hypotheses, lemmas, and assumptions. *) - - val print_atom : Format.formatter -> atom -> unit - (** Printing function for atoms *) - - val hyp_info : hyp -> string * string option * (Format.formatter -> unit -> unit) list - val lemma_info : lemma -> string * string option * (Format.formatter -> unit -> unit) list - val assumption_info : assumption -> string * string option * (Format.formatter -> unit -> unit) list - (** Functions to return information about hypotheses and lemmas *) - -end - -module Default(S : Sidekick_sat.S) = struct - module Atom = S.Atom - module Clause = S.Clause - module P = S.Proof - - let print_atom = Atom.pp - - let hyp_info c = - "hypothesis", Some "LIGHTBLUE", - [ fun fmt () -> Format.fprintf fmt "%s" @@ Clause.name c] - - let lemma_info c = - "lemma", Some "BLUE", - [ fun fmt () -> Format.fprintf fmt "%s" @@ Clause.name c] - - let assumption_info c = - "assumption", Some "PURPLE", - [ fun fmt () -> Format.fprintf fmt "%s" @@ Clause.name c] - -end - -(** Functor to provide dot printing *) -module Make(S : Sidekick_sat.S)(A : Arg with type atom := S.atom - and type hyp := S.clause - and type lemma := S.clause - and type assumption := S.clause) = struct - module Atom = S.Atom - module Clause = S.Clause - module P = S.Proof - - let node_id n = Clause.name n.P.conclusion - - let res_node_id n = (node_id n) ^ "_res" - - let proof_id p = node_id (P.expand p) - - let print_clause fmt c = - let v = Clause.atoms c in - if Array.length v = 0 then - Format.fprintf fmt "⊥" - else ( - let n = Array.length v in - for i = 0 to n - 1 do - Format.fprintf fmt "%a" A.print_atom (Array.get v i); - if i < n - 1 then - Format.fprintf fmt ", " - done - ) - - let print_edge fmt i j = - Format.fprintf fmt "%s -> %s;@\n" j i - - let print_edges fmt n = - match n.P.step with - | P.Resolution (p1, p2, _) -> - print_edge fmt (res_node_id n) (proof_id p1); - print_edge fmt (res_node_id n) (proof_id p2) - | _ -> () - - let table_options fmt color = - Format.fprintf fmt "BORDER=\"0\" CELLBORDER=\"1\" CELLSPACING=\"0\" BGCOLOR=\"%s\"" color - - let table fmt (c, rule, color, l) = - Format.fprintf fmt "%a" print_clause c; - match l with - | [] -> - Format.fprintf fmt "%s" color rule - | f :: r -> - Format.fprintf fmt "%s%a" - color (List.length l) rule f (); - List.iter (fun f -> Format.fprintf fmt "%a" f ()) r - - let print_dot_node fmt id color c rule rule_color l = - Format.fprintf fmt "%s [shape=plaintext, label=<%a
>];@\n" - id table_options color table (c, rule, rule_color, l) - - let print_dot_res_node fmt id a = - Format.fprintf fmt "%s [label=<%a>];@\n" id A.print_atom a - - let ttify f c = fun fmt () -> f fmt c - - let print_contents fmt n = - match n.P.step with - (* Leafs of the proof tree *) - | P.Hypothesis -> - let rule, color, l = A.hyp_info P.(n.conclusion) in - let color = match color with None -> "LIGHTBLUE" | Some c -> c in - print_dot_node fmt (node_id n) "LIGHTBLUE" P.(n.conclusion) rule color l - | P.Assumption -> - let rule, color, l = A.assumption_info P.(n.conclusion) in - let color = match color with None -> "LIGHTBLUE" | Some c -> c in - print_dot_node fmt (node_id n) "LIGHTBLUE" P.(n.conclusion) rule color l - | P.Lemma _ -> - let rule, color, l = A.lemma_info P.(n.conclusion) in - let color = match color with None -> "YELLOW" | Some c -> c in - print_dot_node fmt (node_id n) "LIGHTBLUE" P.(n.conclusion) rule color l - - (* Tree nodes *) - | P.Duplicate (p, l) -> - print_dot_node fmt (node_id n) "GREY" P.(n.conclusion) "Duplicate" "GREY" - ((fun fmt () -> (Format.fprintf fmt "%s" (node_id n))) :: - List.map (ttify A.print_atom) l); - print_edge fmt (node_id n) (node_id (P.expand p)) - | P.Resolution (_, _, a) -> - print_dot_node fmt (node_id n) "GREY" P.(n.conclusion) "Resolution" "GREY" - [(fun fmt () -> (Format.fprintf fmt "%s" (node_id n)))]; - print_dot_res_node fmt (res_node_id n) a; - print_edge fmt (node_id n) (res_node_id n) - - let print_node fmt n = - print_contents fmt n; - print_edges fmt n - - let print fmt p = - Format.fprintf fmt "digraph proof {@\n"; - P.fold (fun () -> print_node fmt) () p; - Format.fprintf fmt "}@." - -end - -module Simple(S : Sidekick_sat.S) = Make(S)(Default(S)) diff --git a/src/backend/Dot.mli b/src/backend/Dot.mli deleted file mode 100644 index 1fb85eed..00000000 --- a/src/backend/Dot.mli +++ /dev/null @@ -1,67 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -(** Dot backend for proofs - - This module provides functions to export proofs into the dot graph format. - Graphs in dot format can be used to generates images using the graphviz tool. -*) - -module type S = Backend_intf.S -(** Interface for exporting proofs. *) - -module type Arg = sig - (** Term printing for DOT - - This module defines what functions are required in order to export - a proof to the DOT format. - *) - - type atom - (** The type of atomic formuals *) - - type hyp - type lemma - type assumption - (** The type of theory-specifi proofs (also called lemmas). *) - - val print_atom : Format.formatter -> atom -> unit - (** Print the contents of the given atomic formulas. - WARNING: this function should take care to escape and/or not output special - reserved characters for the dot format (such as quotes and so on). *) - - val hyp_info : hyp -> string * string option * (Format.formatter -> unit -> unit) list - val lemma_info : lemma -> string * string option * (Format.formatter -> unit -> unit) list - val assumption_info : assumption -> string * string option * (Format.formatter -> unit -> unit) list - (** Generate some information about the leafs of the proof tree. Currently this backend - print each lemma/assumption/hypothesis as a single leaf of the proof tree. - These function should return a triplet [(rule, color, l)], such that: - - [rule] is a name for the proof (arbitrary, does not need to be unique, but - should rather be descriptive) - - [color] is a color name (optional) understood by DOT - - [l] is a list of printers that will be called to print some additional information - *) - -end - -module Default(S : Sidekick_sat.S) : Arg with type atom := S.atom - and type hyp := S.clause - and type lemma := S.clause - and type assumption := S.clause -(** Provides a reasonnable default to instantiate the [Make] functor, assuming - the original printing functions are compatible with DOT html labels. *) - -module Make(S : Sidekick_sat.S)(A : Arg with type atom := S.atom - and type hyp := S.clause - and type lemma := S.clause - and type assumption := S.clause) : S with type t := S.proof -(** Functor for making a module to export proofs to the DOT format. *) - -module Simple(S : Sidekick_sat.S) : S with type t := S.proof -(** Functor for making a module to export proofs to the DOT format. - The substitution of the hyp type is non-destructive due to a restriction - of destructive substitutions on earlier versions of ocaml. *) - diff --git a/src/backend/dune b/src/backend/dune deleted file mode 100644 index dc6531eb..00000000 --- a/src/backend/dune +++ /dev/null @@ -1,12 +0,0 @@ - -(library - (name Sidekick_backend) - (public_name sidekick.backend) - (synopsis "proof backends for Sidekick") - (libraries sidekick.sat) - (flags :standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string - -open Sidekick_sat -open Sidekick_util) - (ocamlopt_flags :standard -O3 -bin-annot - -unbox-closures -unbox-closures-factor 20) - ) - diff --git a/src/main/dune b/src/main/dune index 81365e06..dc2cb0b7 100644 --- a/src/main/dune +++ b/src/main/dune @@ -4,8 +4,7 @@ (name main) (public_name sidekick) (package sidekick) - (libraries containers sequence result - sidekick.sat sidekick.smt sidekick.smtlib sidekick.backend + (libraries containers sequence result msat sidekick.smt sidekick.smtlib sidekick.dimacs) (flags :standard -w +a-4-42-44-48-50-58-32-60@8 -safe-string -color always -open Sidekick_util) diff --git a/src/main_test/README.md b/src/main_test/README.md deleted file mode 100644 index 80ab1a01..00000000 --- a/src/main_test/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/main_test/dune b/src/main_test/dune deleted file mode 100644 index f3ab53b5..00000000 --- a/src/main_test/dune +++ /dev/null @@ -1,9 +0,0 @@ - -(executable - (name main_test) - (libraries sidekick_sat sidekick.backend sidekick.th_sat dolmen) - (flags :standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Sidekick_sat) - (ocamlopt_flags :standard -O3 -bin-annot - -unbox-closures -unbox-closures-factor 20) - ) - diff --git a/src/main_test/main_test.ml b/src/main_test/main_test.ml deleted file mode 100644 index b82891f8..00000000 --- a/src/main_test/main_test.ml +++ /dev/null @@ -1,251 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -exception Incorrect_model -exception Out_of_time -exception Out_of_space - -let file = ref "" -let p_cnf = ref false -let p_check = ref false -let p_dot_proof = ref "" -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 : CDCL.S) - (Th : sig - include CDCL.Theory_intf.S with type t = S.theory - end) - (T : sig - include Type.S with type atom := S.atom - val create : Th.t -> t - end) - : sig - val do_task : Dolmen.Statement.t -> unit - end = struct - - module D = CDCL_backend.Dot.Make(S.Proof)(CDCL_backend.Dot.Default(S.Proof)) - - let hyps = ref [] - - let st = S.create ~size:`Big () - let th = S.theory st - let t_st = T.create th - - let check_model (CDCL.Sat_state sat) = - let check_clause c = - let l = List.map (function a -> - Log.debugf 99 - (fun k -> k "Checking value of %a" S.Formula.pp a); - sat.eval a) c in - List.exists (fun x -> x) l - in - let l = List.map check_clause !hyps in - List.for_all (fun x -> x) l - - let prove ~assumptions () = - let res = S.solve st ~assumptions () in - let t = Sys.time () in - begin match res with - | S.Sat state -> - if !p_check then - if not (check_model state) then - raise Incorrect_model; - let t' = Sys.time () -. t in - Format.printf "Sat (%f/%f)@." t t' - | S.Unsat (CDCL.Unsat_state us) -> - if !p_check then begin - let p = us.get_proof () in - S.Proof.check p; - if !p_dot_proof <> "" then begin - let fmt = Format.formatter_of_out_channel (open_out !p_dot_proof) in - D.print fmt p - end - end; - let t' = Sys.time () -. t in - Format.printf "Unsat (%f/%f)@." t t' - end - - let do_task s : unit = - match s.Dolmen.Statement.descr with - | Dolmen.Statement.Def (id, t) -> T.def t_st id t - | Dolmen.Statement.Decl (id, t) -> T.decl t_st id t - | Dolmen.Statement.Clause l -> - let cnf = T.antecedent t_st (Dolmen.Term.or_ l) in - hyps := cnf @ !hyps; - S.assume st cnf - | Dolmen.Statement.Consequent t -> - let cnf = T.consequent t_st t in - hyps := cnf @ !hyps; - S.assume st cnf - | Dolmen.Statement.Antecedent t -> - let cnf = T.antecedent t_st 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 t_st f in - prove ~assumptions () - | Dolmen.Statement.Prove -> - 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 -end - -module Sat = Make(CDCL_sat)(CDCL_sat.Th)(Type_sat) - (* -module Smt = Make(Minismt_smt)(CDCL_sat.Th)(Minismt_smt.Type) - *) - -let solver = ref (module Sat : S) -let solver_list = [ - "sat", (module Sat : S); -(* FIXME - "smt", (module Smt : S); -*) -] - -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 - let multiplier m = - let arg1 = String.sub arg 0 (l-1) in - r := m *. (float_of_string arg1) - in - if l = 0 then raise (Arg.Bad "bad numeric argument") - else - try - match arg.[l-1] with - | 'k' -> multiplier 1e3 - | 'M' -> multiplier 1e6 - | 'G' -> multiplier 1e9 - | 'T' -> multiplier 1e12 - | 's' -> multiplier 1. - | 'm' -> multiplier 60. - | 'h' -> multiplier 3600. - | 'd' -> multiplier 86400. - | '0'..'9' -> r := float_of_string arg - | _ -> raise (Arg.Bad "bad numeric argument") - with Failure _ -> raise (Arg.Bad "bad numeric argument") - -let setup_gc_stat () = - at_exit (fun () -> - Gc.print_stat stdout; - ) - -let input_file = fun s -> file := s - -let usage = "Usage : main [options] " -let argspec = Arg.align [ - "-bt", Arg.Unit (fun () -> Printexc.record_backtrace true), - " Enable stack traces"; - "-cnf", Arg.Set p_cnf, - " Prints the cnf used."; - "-check", Arg.Set p_check, - " Build, check and print the proof (if output is set), if unsat"; - "-dot", Arg.Set_string p_dot_proof, - " 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), - "[smhd] Sets the time limit for the sat solver"; - "-v", Arg.Int (fun i -> Log.set_debug i), - " Sets the debug verbose level"; - ] - -(* Limits alarm *) -let check () = - let t = Sys.time () in - let heap_size = (Gc.quick_stat ()).Gc.heap_words in - let s = float heap_size *. float Sys.word_size /. 8. in - if t > !time_limit then - raise Out_of_time - else if s > !size_limit then - raise Out_of_space - - -let main () = - (* Administrative duties *) - Arg.parse argspec input_file usage; - if !file = "" then ( - Arg.usage argspec usage; - exit 2 - ); - 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; - Gc.delete_alarm al; - () - -let () = - try - main () - with - | Out_of_time -> - Format.printf "Timeout@."; - exit 2 - | Out_of_space -> - Format.printf "Spaceout@."; - exit 3 - | Incorrect_model -> - Format.printf "Internal error : incorrect *sat* model@."; - exit 4 - (* FIXME - | Minismt_smt.Type.Typing_error (msg, t) - *) - | Type_sat.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/main_test/solver.ml b/src/main_test/solver.ml deleted file mode 100644 index 70644d58..00000000 --- a/src/main_test/solver.ml +++ /dev/null @@ -1,18 +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 Make (Th : Theory_intf.S) = Msat.Make(Th) - - diff --git a/src/main_test/solver.mli b/src/main_test/solver.mli deleted file mode 100644 index 63ee926d..00000000 --- a/src/main_test/solver.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 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 Make (Th : Theory_intf.S) - : S with type formula = Th.formula - and type Proof.lemma = Th.proof - and type theory = Th.t -(** Functor to create a SMT Solver parametrised by the atomic - formulas and a theory. *) - diff --git a/src/main_test/theory_smt.ml b/src/main_test/theory_smt.ml deleted file mode 100644 index a24fbbcd..00000000 --- a/src/main_test/theory_smt.ml +++ /dev/null @@ -1,709 +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 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 Msat.Same_sign - else Msat.Negated - -end - -module Ts_arg = struct - module Form = Atom - - type t = unit - - let fresh () : Form.t = - let id = Id.ty "fresh" Ty.prop in - Form.pred (Term.of_id id) - -end - - -module Formula = Msat_tseitin.Make(Ts_arg) - -(** {2 Theory} *) - -module E = Eclosure.Make(Term) -module H = Backtrack.Hashtbl(Term) -module M = Hashtbl.Make(Term) - -let uf acts = E.create acts - -let assign t = - match E.find_tag uf t with - | _, None -> t - | _, Some (_, v) -> v - -(* Propositional constants *) - -let true_ = Theory_smt.(Term.of_id (Id.ty "true" Ty.prop)) -let false_ = Theory_smt.(Term.of_id (Id.ty "false" Ty.prop)) - -(* Uninterpreted functions and predicates *) - -let map : Theory_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 - | { Theory_smt.term = Theory_smt.App (f, tys, l);_ } -> - let is_prop = Theory_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 = Theory_smt.Term.apply f tys l' in - begin try - let t', u_v = H.find interpretation u in - if not (Theory_smt.Term.equal t_v u_v) then begin - match t' with - | { Theory_smt.term = Theory_smt.App (_, _, r); _ } when is_prop -> - let eqs = List.map2 (fun a b -> Theory_smt.Atom.neg (Theory_smt.Atom.eq a b)) l r in - if Theory_smt.(Term.equal u_v true_) then begin - let res = Theory_smt.Atom.pred t :: - Theory_smt.Atom.neg (Theory_smt.Atom.pred t') :: eqs in - raise (Absurd res) - end else begin - let res = Theory_smt.Atom.pred t' :: - Theory_smt.Atom.neg (Theory_smt.Atom.pred t) :: eqs in - raise (Absurd res) - end - | { Theory_smt.term = Theory_smt.App (_, _, r); _ } -> - let eqs = List.map2 (fun a b -> Theory_smt.Atom.neg (Theory_smt.Atom.eq a b)) l r in - let res = Theory_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 - | { Theory_smt.term = Theory_smt.Var _; _ } as t -> - Log.debugf 10 (fun k -> k "Adding %a as assignable" Theory_smt.Term.print t); - f t - | { Theory_smt.term = Theory_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" Theory_smt.Term.print t); - f t - -let iter_assignable f = function - | { Theory_smt.atom = Theory_smt.Pred { Theory_smt.term = Theory_smt.Var _;_ }; _ } -> () - | { Theory_smt.atom = Theory_smt.Pred ({ Theory_smt.term = Theory_smt.App (_, _, l);_} as t); _ } -> - if l <> [] then add_watch t (t :: l); - List.iter (iter_aux f) l; - | { Theory_smt.atom = Theory_smt.Equal (a, b);_ } -> - iter_aux f a; iter_aux f b - -let eval = function - | { Theory_smt.atom = Theory_smt.Pred t; _ } -> - begin try - let v = H.find map t in - if Theory_smt.Term.equal v true_ then - Plugin_intf.Valued (true, [t]) - else if Theory_smt.Term.equal v false_ then - Plugin_intf.Valued (false, [t]) - else - Plugin_intf.Unknown - with Not_found -> - Plugin_intf.Unknown - end - | { Theory_smt.atom = Theory_smt.Equal (a, b); sign; _ } -> - begin try - let v_a = H.find map a in - let v_b = H.find map b in - if Theory_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) -> (Theory_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 - | { Theory_smt.atom = Theory_smt.Equal (u, v); sign = true;_ } -> - E.add_eq uf u v - | { Theory_smt.atom = Theory_smt.Equal (u, v); sign = false;_ } -> - E.add_neq uf u v - | { Theory_smt.atom = Theory_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 = Theory_smt.Atom.eq a b :: List.map Theory_smt.Atom.neg (chain_eq l) in - Plugin_intf.Unsat (c, ()) - -let if_sat _ = - Plugin_intf.Sat - diff --git a/src/main_test/theory_smt.mli b/src/main_test/theory_smt.mli deleted file mode 100644 index dd5028e0..00000000 --- a/src/main_test/theory_smt.mli +++ /dev/null @@ -1,323 +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 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 * Msat.negated - (** Normalization functions as required by msat. *) - -end - -module Formula : Msat_tseitin.S with type atom = atom - diff --git a/src/main_test/type.ml b/src/main_test/type.ml deleted file mode 100644 index d33f98ae..00000000 --- a/src/main_test/type.ml +++ /dev/null @@ -1,29 +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 t - - 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 : t -> Dolmen.Id.t -> Dolmen.Term.t -> unit - (** New declaration, i.e an identifier and its type. *) - - val def : t -> Dolmen.Id.t -> Dolmen.Term.t -> unit - (** New definition, i.e an identifier and the term it is equal to. *) - - val assumptions : t -> Dolmen.Term.t -> atom list - (** Parse a list of local assumptions. *) - - val consequent : t -> Dolmen.Term.t -> atom list list - val antecedent : t -> 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/src/main_test/type_sat.ml b/src/main_test/type_sat.ml deleted file mode 100644 index e6124421..00000000 --- a/src/main_test/type_sat.ml +++ /dev/null @@ -1,100 +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 = CDCL_tseitin.Make(CDCL_sat.Th) - -(* Exceptions *) -(* ************************************************************************ *) - -exception Typing_error of string * Dolmen.Term.t - -(* Identifiers *) -(* ************************************************************************ *) - -type t = { - symbols: Formula.atom H.t; - fresh: Formula.fresh_state; - st: Formula.state; -} - -let create th : t = { - symbols = H.create 42; - fresh=th; - st=Formula.create th; -} - -let find_id st id = - try - H.find st.symbols id - with Not_found -> - let res = CDCL_sat.Th.fresh st.fresh in - H.add st.symbols id res; - res - -(* Actual parsing *) -(* ************************************************************************ *) - -[@@@ocaml.warning "-9"] - -let rec parse st = 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 st 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 st 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 st) 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 st) l) - | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Imply }, [p; q]) } -> - Formula.make_imply (parse st p) (parse st q) - | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Equiv }, [p; q]) } -> - Formula.make_equiv (parse st p) (parse st q) - | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Xor }, [p; q]) } -> - Formula.make_xor (parse st p) (parse st 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 st t = - let f = parse st t in - let cnf = Formula.make_cnf st.st f in - List.map (function - | [ x ] -> x - | _ -> assert false - ) cnf - -let antecedent st t = - let f = parse st t in - Formula.make_cnf st.st f - -let consequent st t = - let f = parse st t in - Formula.make_cnf st.st @@ Formula.make_not f - diff --git a/src/main_test/type_sat.mli b/src/main_test/type_sat.mli deleted file mode 100644 index 5f081f16..00000000 --- a/src/main_test/type_sat.mli +++ /dev/null @@ -1,14 +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 Type.S with type atom := CDCL_sat.Th.formula - -val create : CDCL_sat.Th.t -> t - diff --git a/src/main_test/unionfind.ml b/src/main_test/unionfind.ml deleted file mode 100644 index ab81a1ad..00000000 --- a/src/main_test/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/main_test/unionfind.mli b/src/main_test/unionfind.mli deleted file mode 100644 index adf2cd25..00000000 --- a/src/main_test/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/sat/Internal.ml b/src/sat/Internal.ml deleted file mode 100644 index 1759e54a..00000000 --- a/src/sat/Internal.ml +++ /dev/null @@ -1,1580 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - - -module Var_fields = Solver_intf.Var_fields - -let v_field_seen_neg = Var_fields.mk_field() -let v_field_seen_pos = Var_fields.mk_field() -let () = Var_fields.freeze() - -module C_fields = Solver_intf.C_fields - -let c_field_attached = C_fields.mk_field () (* watching literals? *) -let c_field_dead = C_fields.mk_field () (* been removed once? *) -let c_field_visited = C_fields.mk_field () (* used during propagation and proof generation. *) - -module Make (Th : Theory_intf.S) = struct - type formula = Th.Form.t - type lemma = Th.proof - - type var = { - v_id : int; - v_pa : atom; - v_na : atom; - mutable v_fields : Var_fields.t; - mutable v_level : int; - mutable v_idx: int; (** position in heap *) - mutable v_weight : float; (** Weight (for the heap), tracking activity *) - mutable reason : reason option; - } - - and atom = { - a_id : int; - var : var; - neg : atom; - lit : formula; - mutable is_true : bool; - mutable watched : clause Vec.t; - } - - and clause = { - name : int; - tag : int option; - atoms : atom array; - mutable c_premise : premise; - mutable activity : float; - mutable c_flags : C_fields.t - } - - and reason = - | Decision - | Bcp of clause - | Local of clause - - and premise = - | Hyp - | Lemma of lemma - | Simplified of clause - | History of clause list - - type proof = clause - - let rec dummy_var = - { v_id = -101; - v_pa = dummy_atom; - v_na = dummy_atom; - v_fields = Var_fields.empty; - v_level = -1; - v_weight = -1.; - v_idx= -1; - reason = None; - } - and dummy_atom = - { var = dummy_var; - lit = Th.Form.dummy; - watched = Obj.magic 0; - (* should be [Vec.make_empty dummy_clause] - but we have to break the cycle *) - neg = dummy_atom; - is_true = false; - a_id = -102; - } - let dummy_clause = - { name = -1; - tag = None; - atoms = [| |]; - activity = -1.; - c_flags = C_fields.empty; - c_premise = History []; - } - - let () = dummy_atom.watched <- Vec.make_empty dummy_clause - - (* Constructors *) - module MF = Hashtbl.Make(Th.Form) - - let rec name_of_clause c = match c.c_premise with - | Hyp -> "H" ^ string_of_int c.name - | Lemma _ -> "T" ^ string_of_int c.name - | History _ -> "C" ^ string_of_int c.name - | Simplified d -> name_of_clause d - - module H = Heap.Make(struct - type t = var - let[@inline] cmp i j = j.v_weight < i.v_weight (* comparison by weight *) - let dummy = dummy_var - let[@inline] idx v = v.v_idx - let[@inline] set_idx v i = v.v_idx <- i - end) - - exception Sat - exception Unsat - exception UndecidedLit - exception Restart - exception Conflict of clause - - let var_decay : float = 1. /. 0.95 - (* inverse of the activity factor for variables. Default 1/0.999 *) - - let clause_decay : float = 1. /. 0.999 - (* inverse of the activity factor for clauses. Default 1/0.95 *) - - let restart_first : int = 100 - (* intial restart limit *) - - let learntsize_factor : float = 1. /. 3. - (* initial limit for the number of learnt clauses, 1/3 of initial - number of clauses by default *) - - let restart_inc : float = 1.5 - (* multiplicative factor for restart limit, default 1.5 *) - - let learntsize_inc : float = 1.1 - (* multiplicative factor for [learntsize_factor] at each restart, default 1.1 *) - - (* Singleton type containing the current state *) - type t = { - f_map: var MF.t; - vars: var Vec.t; - mutable cpt_mk_var: int; - mutable cpt_mk_clause: int; - - th: Th.t lazy_t; - - clauses: clause Vec.t; - - mutable unsat_conflict : clause option; - (* conflict clause at [base_level], if any *) - mutable next_decision : atom option; - (* When the last conflict was a semantic one, this stores the next decision to make *) - - trail : atom Vec.t; - (* decision stack + propagated elements (atoms or assignments). *) - - elt_levels : int Vec.t; - (* decision levels in [trail] *) - - backtrack_levels : int Vec.t; - (* user levels in [backtrack] *) - - backtrack : (unit -> unit) Vec.t; - (** Actions to call when backtracking *) - - to_redo_after_backtrack: (unit -> unit) Vec.t; - (** Actions to re-do after backtracking *) - - mutable th_head : int; - (* Start offset in the queue {!trail} of - unit facts not yet seen by the theory. *) - mutable elt_head : int; - (* Start offset in the queue {!trail} of - unit facts to propagate, within the trail *) - - (* invariant: - - during propagation, th_head <= elt_head - - then, once elt_head reaches length trail, Th.assume is - called so that th_head can catch up with elt_head - - this is repeated until a fixpoint is reached; - - before a decision (and after the fixpoint), - th_head = elt_head = length trail - *) - - order : H.t; - (* Heap ordered by variable activity *) - - mutable var_incr : float; - (* increment for variables' activity *) - - mutable clause_incr : float; - (* increment for clauses' activity *) - - tmp_vec_seen : atom Vec.t; - (* temporary vector used for conflict resolution *) - - to_add : (bool * clause) Vec.t; - (* clauses to add, from the user *) - } - - (* Starting environment. *) - let create_ ~size_map ~size_vars ~size_trail ~size_lvl th : t = { - f_map = MF.create size_map; - vars = Vec.make size_vars dummy_var; - cpt_mk_var = 0; - cpt_mk_clause = 0; - th; - unsat_conflict = None; - next_decision = None; - - clauses = Vec.make 0 dummy_clause; - - th_head = 0; - elt_head = 0; - - trail = Vec.make size_trail dummy_atom; - elt_levels = Vec.make size_lvl (-1); - backtrack_levels = Vec.make size_lvl (-1); - backtrack = Vec.make size_lvl (fun () -> ()); - to_redo_after_backtrack = Vec.make 10 (fun () -> ()); - - order = H.create(); - to_add = Vec.make_empty (true, dummy_clause); - tmp_vec_seen = Vec.make_empty dummy_atom; - - var_incr = 1.; - clause_incr = 1.; - } - - type state = t - - let[@inline] n_vars st = Vec.size st.vars - let[@inline] get_var st i = Vec.get st.vars i - - module Var = struct - type t = var - let dummy = dummy_var - let[@inline] level v = v.v_level - let[@inline] pos v = v.v_pa - let[@inline] neg v = v.v_na - let[@inline] reason v = v.reason - let[@inline] weight v = v.v_weight - - let[@inline] id v = v.v_id - let[@inline] level v = v.v_level - let[@inline] idx v = v.v_idx - - let[@inline] set_level v lvl = v.v_level <- lvl - let[@inline] set_idx v i = v.v_idx <- i - let[@inline] set_weight v w = v.v_weight <- w - - let[@inline] in_heap v = v.v_idx >= 0 - - let make (st:state) (t:formula) : var * Theory_intf.negated = - let lit, negated = Th.Form.norm t in - try - MF.find st.f_map lit, negated - with Not_found -> - let cpt_double = st.cpt_mk_var lsl 1 in - let rec var = - { v_id = st.cpt_mk_var; - v_pa = v_pa; - v_na = v_na; - v_fields = Var_fields.empty; - v_level = -1; - v_idx= -1; - v_weight = 0.; - reason = None; - } - and v_pa = - { var = var; - lit = lit; - watched = Vec.make 10 dummy_clause; - neg = v_na; - is_true = false; - a_id = cpt_double (* a_id = v_id*2 *) } - and v_na = - { var = var; - lit = Th.Form.neg lit; - watched = Vec.make 10 dummy_clause; - neg = v_pa; - is_true = false; - a_id = cpt_double + 1 (* a_id = v_id*2+1 *) } in - MF.add st.f_map lit var; - st.cpt_mk_var <- st.cpt_mk_var + 1; - Vec.push st.vars var; - var, negated - - (* Marking helpers *) - let[@inline] clear v = - v.v_fields <- Var_fields.empty - - let[@inline] seen_both v = - Var_fields.get v_field_seen_pos v.v_fields && - Var_fields.get v_field_seen_neg v.v_fields - - let pp out (v:t) = Th.Form.print out v.v_pa.lit - end - - module Atom = struct - type t = atom - let dummy = dummy_atom - let[@inline] level a = a.var.v_level - let[@inline] var a = a.var - let[@inline] neg a = a.neg - let[@inline] abs a = a.var.v_pa - let[@inline] get_formula a = a.lit - let[@inline] equal a b = a == b - let[@inline] is_pos a = a == abs a - let[@inline] compare a b = Pervasives.compare a.a_id b.a_id - let[@inline] reason a = Var.reason a.var - let[@inline] id a = a.a_id - let[@inline] is_true a = a.is_true - let[@inline] is_false a = a.neg.is_true - - let[@inline] seen a = - let pos = equal a (abs a) in - if pos - then Var_fields.get v_field_seen_pos a.var.v_fields - else Var_fields.get v_field_seen_neg a.var.v_fields - - let[@inline] mark a = - let pos = equal a (abs a) in - if pos - then a.var.v_fields <- Var_fields.set v_field_seen_pos true a.var.v_fields - else a.var.v_fields <- Var_fields.set v_field_seen_neg true a.var.v_fields - - let[@inline] make st lit = - let var, negated = Var.make st lit in - match negated with - | Theory_intf.Negated -> var.v_na - | Theory_intf.Same_sign -> var.v_pa - - let pp fmt a = Th.Form.print fmt a.lit - - let pp_a fmt v = - if Array.length v = 0 then ( - Format.fprintf fmt "∅" - ) else ( - pp fmt v.(0); - if (Array.length v) > 1 then begin - for i = 1 to (Array.length v) - 1 do - Format.fprintf fmt " ∨ %a" pp v.(i) - done - end - ) - - (* Complete debug printing *) - let sign a = if a == a.var.v_pa then "+" else "-" - - let debug_reason fmt = function - | n, _ when n < 0 -> - Format.fprintf fmt "%%" - | n, None -> - Format.fprintf fmt "%d" n - | n, Some Local _ -> - Format.fprintf fmt "L%d" n - | n, Some Decision -> - Format.fprintf fmt "@@%d" n - | n, Some Bcp c -> - Format.fprintf fmt "->%d/%s" n (name_of_clause c) - - let pp_level fmt a = - debug_reason fmt (a.var.v_level, a.var.reason) - - let debug_value out a = - if a.is_true then ( - Format.fprintf out "[T%a]" pp_level a - ) else if a.neg.is_true then ( - Format.fprintf out "[F%a]" pp_level a - ) else ( - CCFormat.string out "[?]" - ) - - let debug out a = - Format.fprintf out "@[@[%a@]%a@]" Th.Form.print a.lit debug_value a - - let debug_a out vec = - Array.iteri (fun i a -> if i>0 then Format.fprintf out "@ "; debug out a) vec - - module Set = CCSet.Make(struct type t = atom let compare = compare end) - end - - module Clause = struct - type t = clause - let dummy = dummy_clause - - let make = - let n = ref 0 in - fun ?tag atoms premise -> - let name = !n in - incr n; - { name; - tag = tag; - atoms = atoms; - c_flags = C_fields.empty; - activity = 0.; - c_premise = premise; - } - - let make_l ?tag l pr = make ?tag (Array.of_list l) pr - - let[@inline] copy (c:t) : t = make ?tag:c.tag c.atoms c.c_premise - - let empty = make [| |] (History []) - let name = name_of_clause - let[@inline] equal c1 c2 = c1==c2 - let[@inline] atoms c = c.atoms - let[@inline] atoms_l c = Array.to_list c.atoms - let[@inline] tag c = c.tag - let hash cl = Array.fold_left (fun i a -> Hashtbl.hash (a.a_id, i)) 0 cl.atoms - - let[@inline] premise c = c.c_premise - let[@inline] set_premise c p = c.c_premise <- p - - (* a dead clause is a clause that has been removed. It should never - be added again *) - let[@inline] dead c = C_fields.get c_field_dead c.c_flags - let[@inline] mark_dead c = c.c_flags <- C_fields.set c_field_dead true c.c_flags - - let[@inline] visited c = C_fields.get c_field_visited c.c_flags - let[@inline] set_visited c b = c.c_flags <- C_fields.set c_field_visited b c.c_flags - - let[@inline] attached c = C_fields.get c_field_attached c.c_flags - let[@inline] set_attached c b = c.c_flags <- C_fields.set c_field_attached b c.c_flags - - let[@inline] activity c = c.activity - let[@inline] set_activity c w = c.activity <- w - - let rec is_learnt c = - match c.c_premise with - | Simplified c' -> is_learnt c' - | History _ -> true - | Hyp | Lemma _ -> false - - module Tbl = Hashtbl.Make(struct - type t = clause - let hash = hash - let equal = equal - end) - - let pp fmt c = Format.fprintf fmt "%s : %a" (name c) Atom.pp_a c.atoms - - let rec debug_premise out = function - | Hyp -> Format.fprintf out "hyp" - | Lemma _ -> Format.fprintf out "th_lemma" - | Simplified d -> debug_premise out d.c_premise - | History v -> - Format.fprintf out "[@[%a@]]" - (Util.pp_list @@ CCFormat.of_to_string name_of_clause) v - - let debug out ({atoms=arr; c_premise=cp;_}as c) = - Format.fprintf out "%s@[{@[%a@]}@ c_premise={@[%a@]}@]" - (name c) Atom.debug_a arr debug_premise cp - - let pp_dimacs fmt {atoms;_} = - let aux fmt a = - Array.iter (fun p -> - Format.fprintf fmt "%s%d " - (if p == p.var.v_pa then "-" else "") - (p.var.v_id+1) - ) a - in - Format.fprintf fmt "%a0" aux atoms - end - - module Formula = struct - include Th.Form - let pp = print - end - - (* TODO: simplify this *) - module Proof = struct - type t = proof - - exception Resolution_error of string - exception Insufficient_hyps - (** Raised when a complete resolution derivation cannot be found using the current hypotheses. *) - - let equal_atoms = Atom.equal - let compare_atoms = Atom.compare - - let merge = List.merge compare_atoms - - let _c = ref 0 - let fresh_pcl_name () = incr _c; "R" ^ (string_of_int !_c) - - (* Compute resolution of 2 clauses *) - let resolve (l:atom list) : atom list * atom list = - let rec aux resolved acc = function - | [] -> resolved, acc - | [a] -> resolved, a :: acc - | a :: b :: r -> - if equal_atoms a b then - aux resolved (a :: acc) r - else if equal_atoms a.neg b then - aux ((a.var.v_pa) :: resolved) acc r - else - aux resolved (a :: acc) (b :: r) - in - let resolved, new_clause = aux [] [] l in - resolved, List.rev new_clause - - let to_list c = List.sort Atom.compare @@ Array.to_list c.atoms - - (* TODO: use sets instead of lists, simplify this *) - let analyze (cl:atom list) = - let rec aux duplicates free = function - | [] -> duplicates, free - | [ x ] -> duplicates, x :: free - | x :: ((y :: r) as l) -> - if Atom.equal x y then - count duplicates (x :: free) x [y] r - else - aux duplicates (x :: free) l - and count duplicates free x acc = function - | (y :: r) when Atom.equal x y -> - count duplicates free x (y :: acc) r - | l -> - aux (acc :: duplicates) free l - in - let doublons, acc = aux [] [] cl in - doublons, List.rev acc - - - (* Comparison of clauses *) - let cmp_cl c d = - Atom.Set.compare (Atom.Set.of_list c) (Atom.Set.of_list d) - - let[@inline] prove conclusion = - assert (conclusion.c_premise <> History []); - conclusion - - let rec set_atom_proof a = - let aux acc b = - if equal_atoms a.neg b then acc - else set_atom_proof b :: acc - in - assert (a.var.v_level >= 0); - match (a.var.reason) with - | Some Bcp c -> - Log.debugf 5 (fun k->k "Analysing: @[%a@ %a@]" Atom.debug a Clause.debug c); - if Array.length c.atoms = 1 then ( - Log.debugf 5 (fun k -> k "Old reason: @[%a@]" Atom.debug a); - c - ) else ( - assert (a.neg.is_true); - let r = History (c :: (Array.fold_left aux [] c.atoms)) in - let c' = Clause.make [| a.neg |] r in - a.var.reason <- Some (Bcp c'); - Log.debugf 5 - (fun k -> k "New reason: @[%a@ %a@]" Atom.debug a Clause.debug c'); - c' - ) - | _ -> - Log.debugf 1 (fun k -> k "Error while proving atom %a" Atom.debug a); - raise (Resolution_error "Cannot prove atom") - - let prove_atom a = - if (a.is_true && a.var.v_level = 0) then - Some (set_atom_proof a) - else - None - - (* Interface exposed *) - type node = { - conclusion : clause; - step : step; - } - and step = - | Hypothesis - | Assumption - | Lemma of lemma - | Duplicate of proof * atom list - | Resolution of proof * proof * atom - - let rec chain_res (c, cl) = function - | d :: r -> - Log.debugf 5 - (fun k -> k "(@[sat.proof.resolving@ :c1 %a@ :c2 %a@])" Clause.debug c Clause.debug d); - let dl = to_list d in - begin match resolve (merge cl dl) with - | [a], res -> - begin match r with - | [] -> res, c, d, a - | _ -> - let new_clause = Clause.make_l res (History [c; d]) in - chain_res (new_clause, res) r - end - | pivots, _ -> - Log.debugf 1 - (fun k -> k "(@[err While resolving clauses:@ %a@ %a@ :pivots %a@])" - Clause.debug c Clause.debug d (CCFormat.Dump.list Atom.debug) pivots); - raise (Resolution_error "Clause mismatch") - end - | [] -> - Log.debugf 1 - (fun k -> k "*@[err While resolving clause:@ %a@])" Clause.debug c); - raise (Resolution_error "Bad history") - - let[@inline] conclusion (p:proof) : clause = p - - let expand conclusion = - Log.debugf 5 (fun k -> k "(@[proof.expand@ @[%a@]@])" Clause.debug conclusion); - match conclusion.c_premise with - | Lemma l -> - {conclusion; step = Lemma l; } - | Hyp -> - { conclusion; step = Hypothesis; } - | History [] -> - Log.debugf 1 (fun k -> k "(@[proof.empty_history@ %a@]" Clause.debug conclusion); - raise (Resolution_error "Empty history") - | Simplified c - | History ([c]) -> - let duplicates, res = analyze (to_list c) in - assert (cmp_cl res (to_list conclusion) = 0); - { conclusion; step = Duplicate (c, List.concat duplicates) } - | History ( c :: ([_] as r)) -> - let (l, c', d', a) = chain_res (c, to_list c) r in - assert (cmp_cl l (to_list conclusion) = 0); - { conclusion; step = Resolution (c', d', a); } - | History ( c :: r ) -> - let (l, c', d', a) = chain_res (c, to_list c) r in - conclusion.c_premise <- History [c'; d']; - assert (cmp_cl l (to_list conclusion) = 0); - { conclusion; step = Resolution (c', d', a); } - - let[@inline] step p = (expand p).step - - (* Proof nodes manipulation *) - let is_leaf = function - | Hypothesis - | Assumption - | Lemma _ -> true - | Duplicate _ - | Resolution _ -> false - - let parents = function - | Hypothesis - | Assumption - | Lemma _ -> [] - | Duplicate (p, _) -> [p] - | Resolution (p, p', _) -> [p; p'] - - let expl = function - | Hypothesis -> "hypothesis" - | Assumption -> "assumption" - | Lemma _ -> "lemma" - | Duplicate _ -> "duplicate" - | Resolution _ -> "resolution" - - (* Compute unsat-core - TODO: replace visited bool by a int unique to each call - of unsat_core, so that the cleanup can be removed ? *) - let unsat_core proof = - let rec aux res acc = function - | [] -> res, acc - | c :: r -> - if not (Clause.visited c) then ( - Clause.set_visited c true; - match c.c_premise with - | Hyp | Lemma _ -> aux (c :: res) acc r - | Simplified c -> aux res acc [c] - | History h -> - let l = List.fold_left (fun acc c -> - if not (Clause.visited c) then c :: acc else acc) r h in - aux res (c :: acc) l - ) else ( - aux res acc r - ) - in - let res, tmp = aux [] [] [proof] in - List.iter (fun c -> Clause.set_visited c false) res; - List.iter (fun c -> Clause.set_visited c false) tmp; - res - - module Tbl = Clause.Tbl - - type task = - | Enter of proof - | Leaving of proof - - let spop s = try Some (Stack.pop s) with Stack.Empty -> None - - let rec fold_aux s h f acc = - match spop s with - | None -> acc - | Some (Leaving c) -> - Tbl.add h c true; - fold_aux s h f (f acc (expand c)) - | Some (Enter c) -> - if not (Tbl.mem h c) then begin - Stack.push (Leaving c) s; - let node = expand c in - begin match node.step with - | Duplicate (p1, _) -> - Stack.push (Enter p1) s - | Resolution (p1, p2, _) -> - Stack.push (Enter p2) s; - Stack.push (Enter p1) s - | Hypothesis | Assumption | Lemma _ -> () - end - end; - fold_aux s h f acc - - let fold f acc p = - let h = Tbl.create 42 in - let s = Stack.create () in - Stack.push (Enter p) s; - fold_aux s h f acc - - let check p = fold (fun () _ -> ()) () p - end - - let[@inline] theory st = Lazy.force st.th - let[@inline] nb_clauses st = Vec.size st.clauses - let[@inline] decision_level st = Vec.size st.elt_levels - let[@inline] base_level st = if decision_level st > 0 then 1 else 0 (* first level=assumptions *) - - let[@inline] at_level_0 st : bool = Vec.is_empty st.backtrack_levels - let[@inline] on_backtrack st f : unit = - if not (at_level_0 st) then ( - Vec.push st.backtrack f - ) - - (* [redo_down_to_level_0 f ~undo] performs [f] now. Upon backtracking - before current level, some undo actions scheduled by [f] - might run; - later [f] will be called again - to re-perform the action, and this cycle [f(); backtrack; f(); …] is - done until we backtrack at level 0. - Once at level 0, [f()] is called and will never be undone again. - *) - let rec redo_down_to_level_0 (st:t) (f:unit->unit) : unit = - if not (at_level_0 st) then ( - on_backtrack st - (fun () -> - Vec.push st.to_redo_after_backtrack - (fun () -> redo_down_to_level_0 st f)) - ); - f() - - (* Are the assumptions currently unsat ? *) - let[@inline] is_unsat st = - match st.unsat_conflict with - | Some _ -> true - | None -> false - - (* Variable and literal activity. - Activity is used to decide on which variable to decide when propagation - is done. Uses a heap (implemented in {!Heap}), to keep track of variable activity. - *) - let insert_var_order st (v:var) : unit = - if not (Var.in_heap v) && Var.level v < 0 then ( - (* new variable that is not assigned, add to heap and to theory. *) - H.insert st.order v; - ) - - (* attach an atom by deciding on its variable, if needed *) - let attach_atom (st:t) (a:atom) : unit = - insert_var_order st a.var; - Th.add_formula (Lazy.force st.th) a.lit; - Th.add_formula (Lazy.force st.th) a.neg.lit - - (* Rather than iterate over all the heap when we want to decrease all the - variables/literals activity, we instead increase the value by which - we increase the activity of 'interesting' var/lits. *) - let[@inline] var_decay_activity st = - st.var_incr <- st.var_incr *. var_decay - - let[@inline] clause_decay_activity st = - st.clause_incr <- st.clause_incr *. clause_decay - - (* increase activity of [v] *) - let var_bump_activity st v = - v.v_weight <- v.v_weight +. st.var_incr; - if v.v_weight > 1e100 then ( - Vec.iter - (fun v -> Var.set_weight v (Var.weight v *. 1e-100)) - st.vars; - st.var_incr <- st.var_incr *. 1e-100; - ); - if H.in_heap v then ( - H.decrease st.order v - ) - - (* increase activity of clause [c] *) - let clause_bump_activity st (c:clause) : unit = - c.activity <- c.activity +. st.clause_incr; - if c.activity > 1e20 then ( - Vec.iter - (fun c -> c.activity <- c.activity *. 1e-20) - st.clauses; - st.clause_incr <- st.clause_incr *. 1e-20 - ) - - exception Trivial - - (* [arr_to_list a i] converts [a.(i), ... a.(length a-1)] into a list *) - let array_slice_to_list arr i : _ list = - if i >= Array.length arr then [] - else Array.to_list (Array.sub arr i (Array.length arr - i)) - - (* Eliminates atom doublons in clauses *) - let eliminate_duplicates clause : clause = - let trivial = ref false in - let duplicates = ref [] in - let res = ref [] in - Array.iter - (fun a -> - if Atom.seen a then duplicates := a :: !duplicates - else ( - Atom.mark a; - res := a :: !res - )) - clause.atoms; - List.iter - (fun a -> - if Var.seen_both a.var then trivial := true; - Var.clear a.var) - !res; - if !trivial then ( - raise Trivial - ) else if !duplicates = [] then ( - clause - ) else ( - Clause.make_l !res (Simplified clause) - ) - - (* Making a decision. - Before actually creatig a new decision level, we check that - all propagations have been done and propagated to the theory, - i.e that the theoriy state indeed takes into account the whole - stack of literals - i.e we have indeed reached a propagation fixpoint before making - a new decision *) - let new_decision_level st = - assert (st.th_head = Vec.size st.trail); - assert (st.elt_head = Vec.size st.trail); - Vec.push st.elt_levels (Vec.size st.trail); - Vec.push st.backtrack_levels (Vec.size st.backtrack); (* save the current theory state *) - () - - let[@inline] internalize_atoms (self:t) (c:clause) : unit = - Array.iter (attach_atom self) c.atoms - - (* Attach a clause. - A clause is attached (to its watching lits) when it is first added, - either because it is assumed or learnt. - *) - let attach_clause (self:t) (c:clause) : unit = - assert (not @@ Clause.dead c); - if Array.length c.atoms >= 2 && not (Clause.attached c) then ( - Log.debugf 5 (fun k -> k "(@[sat.attach_clause@ %a@])" Clause.debug c); - Vec.push c.atoms.(0).neg.watched c; - Vec.push c.atoms.(1).neg.watched c; - Clause.set_attached c true; - internalize_atoms self c; - ) - - (* perform all backtracking actions down to level [l]. - To be called only from [cancel_until] *) - let backtrack_down_to (st:t) (lvl:int): unit = - Log.debugf 2 (fun k->k "(@[@{sat.backtrack@} now at stack depth %d@])" lvl); - let done_sth = Vec.size st.backtrack > lvl in - while Vec.size st.backtrack > lvl do - let f = Vec.pop_last st.backtrack in - f() - done; - if done_sth then ( - Th.post_backtrack (theory st); - ); - (* now re-do permanent actions that were backtracked *) - while not (Vec.is_empty st.to_redo_after_backtrack) do - let f = Vec.pop_last st.to_redo_after_backtrack in - f() - done; - () - - (* Backtracking. - Used to backtrack, i.e cancel down to [lvl] excluded, - i.e we want to go back to the state the solver was in - when decision level [lvl] was created. *) - let cancel_until st lvl = - Log.debugf 5 - (fun k -> k "(@[@{sat.cancel_until@}@ :lvl %d :cur-decision-lvl %d@])" lvl @@ decision_level st); - assert (lvl >= base_level st); - (* Nothing to do if we try to backtrack to a non-existent level. *) - if decision_level st <= lvl then ( - ) else ( - (* We set the head of the solver and theory queue to what it was. *) - let head = ref (Vec.get st.elt_levels lvl) in - st.elt_head <- !head; - st.th_head <- !head; - (* Now we need to cleanup the vars that are not valid anymore - (i.e to the right of elt_head in the queue. *) - for c = st.elt_head to Vec.size st.trail - 1 do - let a = Vec.get st.trail c in - (* A literal is unassigned, we nedd to add it back to - the heap of potentially assignable literals, unless it has - a level lower than [lvl], in which case we just move it back. *) - assert (a.var.v_level > lvl); - if a.var.v_level <= lvl then ( - (* It is a late propagation, which has a level - lower than where we backtrack, so we just move it to the head - of the queue, to be theory-propagated again (BCP will be fine). *) - Vec.set st.trail !head a; - head := !head + 1 - ) else ( - (* it is a result of bolean propagation, or a semantic propagation - with a level higher than the level to which we backtrack, - in that case, we simply unset its value and reinsert it into the heap. *) - a.is_true <- false; - a.neg.is_true <- false; - a.var.v_level <- -1; - a.var.reason <- None; - insert_var_order st a.var - ) - done; - let b_lvl = Vec.get st.backtrack_levels lvl in - (* Resize the vectors according to their new size. *) - Vec.shrink st.trail !head; - Vec.shrink st.elt_levels lvl; - Vec.shrink st.backtrack_levels lvl; - (* Recover the right theory state. *) - backtrack_down_to st b_lvl; - ); - assert (Vec.size st.elt_levels = Vec.size st.backtrack_levels); - Log.debugf 15 (fun k->k "(@[sat.trail@,%a@])" (Vec.print ~sep:" " Atom.debug) st.trail); - () - - (* Unsatisfiability is signaled through an exception, since it can happen - in multiple places (adding new clauses, or solving for instance). *) - let report_unsat st confl : _ = - Log.debugf 3 (fun k -> k "(@[sat.unsat_conflict@ %a@])" Clause.debug confl); - st.unsat_conflict <- Some confl; - raise Unsat - - (* Boolean propagation. - Wrapper function for adding a new propagated formula. *) - let enqueue_bool st a reason : unit = - if a.neg.is_true then ( - Error.errorf "(@[sat.enqueue_bool.1@ :false-literal %a@])" Atom.debug a - ); - let level = decision_level st in - Log.debugf 5 - (fun k->k "(@[sat.enqueue_bool@ :lvl %d@ %a@ :reason %a@])" - level Atom.debug a Atom.debug_reason (level,Some reason)); - (* backtrack assignment if needed. Trail is backtracked automatically. *) - assert (not a.is_true && a.var.v_level < 0 && a.var.reason = None); - a.is_true <- true; - a.var.v_level <- level; - a.var.reason <- Some reason; - Vec.push st.trail a; - () - - (* swap elements of array *) - let[@inline] swap_arr a i j = - if i<>j then ( - let tmp = a.(i) in - a.(i) <- a.(j); - a.(j) <- tmp; - ) - - (* move true atoms first, - else move atoms that are not assigned first, - else put atoms assigned at high levels first *) - let put_high_level_atoms_first (arr:atom array) : unit = - (* move [a] in front of [b]? *) - let[@inline] put_before a b = - if Atom.is_true a then not (Atom.is_true b) || Atom.level a>Atom.level b - else if Atom.level a < 0 then Atom.level b >= 0 - else (Atom.level b >= 0 && Atom.level a > Atom.level b) - in - Array.iteri - (fun i a -> - if i>0 && put_before a arr.(0) then ( - (* move first to second, [i]-th to first, second to [i] *) - if i=1 then ( - swap_arr arr 0 1; - ) else ( - let tmp = arr.(1) in - arr.(1) <- arr.(0); - arr.(0) <- arr.(i); - arr.(i) <- tmp; - ); - ) else if i>1 && put_before a arr.(1) then ( - swap_arr arr 1 i; - )) - arr - - (* find which level to backtrack to, given a conflict clause - and a boolean stating whether it is - a UIP ("Unique Implication Point") - precond: the atom list is sorted by decreasing decision level *) - let backtrack_lvl st : atom list -> int * bool = function - | [] | [_] -> - 0, true - | a :: b :: _ -> - assert(a.var.v_level > base_level st); - if a.var.v_level > b.var.v_level then ( - (* backtrack below [a], so we can propagate [not a] *) - b.var.v_level, true - ) else ( - assert (a.var.v_level = b.var.v_level); - assert (a.var.v_level >= base_level st); - max (a.var.v_level - 1) (base_level st), false - ) - - (* result of conflict analysis, containing the learnt clause and some - additional 2. - - invariant: cr_history's order matters, as its head is later used - during pop operations to determine the origin of a clause/conflict - (boolean conflict i.e hypothesis, or theory lemma) *) - type conflict_res = { - cr_backtrack_lvl : int; (* level to backtrack to *) - cr_learnt: atom list; (* lemma learnt from conflict *) - cr_history: clause list; (* justification *) - cr_is_uip: bool; (* conflict is UIP? *) - } - - let[@inline] get_atom st i = Vec.get st.trail i - - (* conflict analysis for SAT - Same idea as the mcsat analyze function (without semantic propagations), - except we look the the Last UIP (TODO: check ?), and do it in an imperative - and efficient manner. *) - let analyze_sat st c_clause : conflict_res = - let path_c = ref 0 in - let learnt = ref [] in - let cond = ref true in - let blevel = ref 0 in - let seen = st.tmp_vec_seen in - Vec.clear seen; - let c = ref c_clause in - let tr_ind = ref (Vec.size st.trail - 1) in - let history = ref [] in - assert (decision_level st > 0); - let conflict_level = - Array.fold_left (fun acc p -> max acc p.var.v_level) 0 c_clause.atoms - in - Log.debugf 5 - (fun k -> k "(@[sat.analyzing-conflict :lvl %d@ :clause %a@])" conflict_level Clause.debug c_clause); - while !cond do - let clause = !c in - Log.debugf 5 (fun k->k"(@[sat.resolving-clause@ %a@])" Clause.debug clause); - begin match clause.c_premise with - | History _ | Simplified _ -> clause_bump_activity st clause - | Hyp | Lemma _ -> () - end; - history := clause :: !history; - (* visit the current predecessors *) - for j = 0 to Array.length clause.atoms - 1 do - let q = clause.atoms.(j) in - assert (q.is_true || q.neg.is_true && q.var.v_level >= 0); (* unsure? *) - if q.var.v_level <= 0 then ( - assert (q.neg.is_true); - match q.var.reason with - | Some Bcp cl -> history := cl :: !history - | _ -> assert false - ); - if not (Var.seen_both q.var) then ( - Atom.mark q; - Atom.mark q.neg; - Vec.push seen q; - if q.var.v_level > 0 then ( - var_bump_activity st q.var; - if q.var.v_level >= conflict_level then ( - incr path_c; - ) else ( - learnt := q :: !learnt; - blevel := max !blevel q.var.v_level - ) - ) - ) - done; - - (* look for the next node to expand *) - while - let a = Vec.get st.trail !tr_ind in - Log.debugf 5 (fun k -> k "(@[sat.conflict.looking-at@ %a@])" Atom.debug a); - (not (Var.seen_both a.var)) || (a.var.v_level < conflict_level) - do - decr tr_ind; - done; - let p = get_atom st !tr_ind in - decr path_c; - decr tr_ind; - match !path_c, p.var.reason with - | 0, _ -> - cond := false; - learnt := p.neg :: (List.rev !learnt) - | n, Some Bcp cl -> - assert (n > 0); - assert (p.var.v_level >= conflict_level); - c := cl - | _ -> assert false - done; - Vec.iter (fun q -> Var.clear q.var) seen; - Vec.clear seen; - let l = List.fast_sort (fun p q -> compare q.var.v_level p.var.v_level) !learnt in - let level, is_uip = backtrack_lvl st l in - { cr_backtrack_lvl = level; - cr_learnt = l; - cr_history = List.rev !history; - cr_is_uip = is_uip; - } - - let[@inline] analyze st c_clause : conflict_res = - analyze_sat st c_clause - - (* Add clause, accounting for backtracking semantics. - - always add literals to queue if not decided yet - - if clause is already true, probably just do nothing - - if clause is unit, propagate lit immediately (with clause as justification) - but do not add clause - - if clause is false, raise Conflict - - permanent stuff: just re-add it on backtrack - *) - let add_clause_ st (c0:clause) : unit = - Log.debugf 5 - (fun k -> k "(@[@{sat.add_clause@}@ %a@])" Clause.debug c0); - assert (not @@ Clause.dead c0); - match eliminate_duplicates c0 with - | exception Trivial -> - Log.debugf 3 (fun k->k "(@[sat.add_clause.ignore-trivial@ %a@])" Clause.debug c0) - | c -> - if c != c0 then ( - Log.debugf 5 (fun k -> k "(@[sat.add_clause.after-eliminate-dups@ %a@])" Clause.debug c); - ); - (* update order of atoms to put the two highest-level/unassigned ones first, - so that watch literals are correct *) - put_high_level_atoms_first c.atoms; - Log.debugf 3 (fun k->k "(@[sat.add_clause.new_clause@ %a@])" Clause.debug c); - match c.atoms with - | [||] -> - (* report Unsat immediately *) - report_unsat st c - | [|a|] -> - if a.neg.is_true then ( - Log.debug 5 "(sat.add_clause: false unit clause, report unsat)"; - report_unsat st c - ) else if a.is_true then ( - (* ignore clause, will never be useful *) - Log.debug 5 "(sat.add_clause: true unit clause, ignore)"; - assert (a.var.v_level >= base_level st); - ) else ( - Log.debugf 5 - (fun k->k "(@[sat.add_clause.unit_clause@ :propagating %a@])" Atom.debug a); - enqueue_bool st a (Bcp c) - ) - | _ -> - Vec.push st.clauses c; - attach_clause st c; - let a = c.atoms.(0) in - let b = c.atoms.(1) in - if a.neg.is_true then ( - (* conflict, even the last literal is false *) - raise (Conflict c) - ) else if b.neg.is_true && not a.is_true && not a.neg.is_true then ( - enqueue_bool st a (Bcp c) - ) - - (* Add a new clause, simplifying, propagating, and backtracking if - the clause is false in the current trail *) - let add_clause ~permanent st (c:clause) : unit = - add_clause_ st c; - if permanent then ( - (* need to re-internalize *) - redo_down_to_level_0 st (fun () -> internalize_atoms st c) - ) else ( - (* kill clause on backtrack *) - on_backtrack st (fun () -> Clause.mark_dead c) - ) - - (* process a conflict: - - learn clause - - backtrack - - report unsat if conflict at level 0 - *) - let add_boolean_conflict st (confl:clause): unit = - Log.debugf 3 - (fun k -> k "(@[@{sat.boolean-conflict@}@ %a@ :decision-lvl %d@])" - Clause.debug confl (decision_level st)); - st.next_decision <- None; - assert (decision_level st >= base_level st); - if decision_level st = base_level st || - Array.for_all (fun a -> a.var.v_level <= base_level st) confl.atoms then ( - (* Top-level conflict *) - report_unsat st confl; - ); - (* compute learnt clause with conflict resolution *) - let cr = analyze st confl in - let confl = Clause.make_l cr.cr_learnt (History cr.cr_history) in - Log.debugf 5 (fun k->k "(@[sat.conflict-clause@ %a@])" Clause.debug confl); - cancel_until st (max cr.cr_backtrack_lvl (base_level st)); - (* make some progress *) - var_decay_activity st; - clause_decay_activity st; - (* add the clause *) - add_clause ~permanent:true st confl - - let[@inline] add_clause_user ~permanent st (c:clause): unit = - Vec.push st.to_add (permanent,c) - - type watch_res = - | Watch_kept - | Watch_removed - - exception Exn_remove_watch - - (* boolean propagation. - [a] is the false atom, one of [c]'s two watch literals - [i] is the index of [c] in [a.watched] - @return whether [c] was removed from [a.watched] - *) - let propagate_in_clause st (a:atom) (c:clause) : watch_res = - let atoms = c.atoms in - let first = atoms.(0) in - if first == a.neg then ( - (* false lit must be at index 1 *) - atoms.(0) <- atoms.(1); - atoms.(1) <- first - ) else ( - assert (a.neg == atoms.(1)); - ); - let first = atoms.(0) in - if first.is_true - then Watch_kept (* true clause, keep it in watched *) - else ( - try (* look for another watch lit *) - for k = 2 to Array.length atoms - 1 do - let ak = atoms.(k) in - if not (ak.neg.is_true) then ( - (* watch lit found: update and exit *) - Array.unsafe_set atoms 1 ak; - Array.unsafe_set atoms k a.neg; - (* remove [c] from [a.watched], add it to [ak.neg.watched] *) - Vec.push ak.neg.watched c; - raise Exn_remove_watch - ) - done; - (* no watch lit found *) - if first.neg.is_true then ( - (* clause is false *) - st.elt_head <- Vec.size st.trail; - raise (Conflict c) - ) else ( - enqueue_bool st first (Bcp c) - ); - Watch_kept - with Exn_remove_watch -> - Watch_removed - ) - - (* propagate atom [a], which was just decided. This checks every - clause watching [a] to see if the clause is false, unit, or has - other possible watches - @param res the optional conflict clause that the propagation might trigger *) - let propagate_atom st a : unit = - let watched = a.watched in - let i = ref 0 in - while !i < Vec.size watched do - let c = Vec.get watched !i in - if not (Clause.attached c) then ( - Vec.fast_remove watched !i (* remove *) - ) else ( - match propagate_in_clause st a c with - | Watch_kept -> incr i - | Watch_removed -> - Vec.fast_remove watched !i; - (* remove clause [c] from watches, then look again at [!i] - since it's now another clause *) - ) - done - - let slice_iter st (hd:int) (last:int) (f:_ -> unit) : unit = - for i = hd to last-1 do - let a = Vec.get st.trail i in - f a.lit - done - - let act_push_ ~permanent st (l:formula IArray.t) (lemma:lemma): unit = - let atoms = IArray.to_array_map (Atom.make st) l in - let c = Clause.make atoms (Lemma lemma) in - Log.debugf 3 - (fun k->k "(@[sat.push_clause_from_theory@ :permanent %B@ %a@])" - permanent Clause.debug c); - add_clause ~permanent st c; - () - - let act_push_local = act_push_ ~permanent:false - let act_push_persistent = act_push_ ~permanent:true - - let act_propagate (st:t) f causes proof : unit = - let l = List.rev_map (Atom.make st) causes in - assert ( - if not @@ List.for_all Atom.is_true l then ( - Error.errorf "(@[sat.act_propagate.invalid_guard@ :guard %a@ \ - :1 all lits are not true@])" - (Util.pp_list Atom.debug) l - ); true); - let p = Atom.make st f in - if p.is_true then ( - ) else if p.neg.is_true then ( - (* we got ourself a wee conflict clause *) - let c = Clause.make_l (p :: List.rev_map Atom.neg l) (Lemma proof) in - raise (Conflict c) - ) else ( - let c = Clause.make_l (p :: List.rev_map Atom.neg l) (Lemma proof) in - insert_var_order st p.var; - enqueue_bool st p (Bcp c); - ) - - let current_slice st head : formula Theory_intf.slice_actions = - let module A = struct - type form = formula - let slice_iter = slice_iter st head (Vec.size st.trail) - end in - (module A) - - (* full slice, for [if_sat] final check *) - let full_slice st : formula Theory_intf.slice_actions = - let module A = struct - type form = formula - let slice_iter = slice_iter st 0 (Vec.size st.trail) - end in - (module A) - - let actions st: (formula,lemma) Theory_intf.actions = - let module A = struct - type nonrec formula = formula - type proof = lemma - let push_persistent = act_push_persistent st - let push_local = act_push_local st - let on_backtrack = on_backtrack st - let propagate = act_propagate st - end in - (module A) - - let create ?(size=`Big) () : t = - let size_map, size_vars, size_trail, size_lvl = match size with - | `Tiny -> 8, 0, 0, 0 - | `Small -> 16, 0, 32, 16 - | `Big -> 4096, 128, 600, 50 - in - let rec solver = lazy ( - create_ ~size_map ~size_vars ~size_trail ~size_lvl th - ) and th = lazy ( - Th.create (actions (Lazy.force solver)) - ) in - Lazy.force solver - - let[@inline] propagation_fixpoint (st:t) : bool = - st.elt_head = Vec.size st.trail && - st.th_head = st.elt_head - - (* some boolean literals were decided/propagated within the solver. Now we - need to inform the theory of those assumptions, so it can do its job. - @return the conflict clause, if the theory detects unsatisfiability *) - let rec theory_propagate st : clause option = - assert (st.elt_head = Vec.size st.trail); - assert (st.th_head <= st.elt_head); - if st.th_head = st.elt_head then ( - None (* fixpoint/no propagation *) - ) else ( - let slice = current_slice st st.th_head in - st.th_head <- st.elt_head; (* catch up *) - match Th.assume (theory st) slice with - | Theory_intf.Sat -> - propagate st - | Theory_intf.Unsat (l, p) -> - (* conflict *) - let l = List.rev_map (Atom.make st) l in - let c = Clause.make_l l (Lemma p) in - Some c - ) - - (* fixpoint between boolean propagation and theory propagation - @return a conflict clause, if any *) - and propagate (st:t) : clause option = - (* Now, check that the situation is sane *) - assert (st.elt_head <= Vec.size st.trail); - while st.elt_head < Vec.size st.trail do - let a = Vec.get st.trail st.elt_head in - Log.debugf 5 (fun k->k "(@[sat.bcp.propagate_atom_on_trail@ %a@])" Atom.pp a); - propagate_atom st a; - st.elt_head <- st.elt_head + 1; - done; - theory_propagate st - - (* remove some learnt clauses - NOTE: so far we do not forget learnt clauses. We could, as long as - lemmas from the theory itself are kept. *) - let reduce_db (_:t) = () - - (* Decide on a new literal, and enqueue it into the trail *) - let rec pick_branch_aux st atom : unit = - let v = atom.var in - if v.v_level >= 0 then ( - assert (v.v_pa.is_true || v.v_na.is_true); - pick_branch_lit st - ) else ( - new_decision_level st; - enqueue_bool st atom Decision - ) - - and pick_branch_lit st = - match st.next_decision with - | Some atom -> - st.next_decision <- None; - pick_branch_aux st atom - | None -> - begin match H.remove_min st.order with - | v -> pick_branch_aux st v.v_pa - | exception Not_found -> raise Sat - end - - let[@inline] check_invariants (st:t) = - if Util._CHECK_INVARIANTS then ( - Th.check_invariants @@ theory st; - (* TODO: also check internal invariants? *) - ) - - (* do some amount of search, until the number of conflicts or clause learnt - reaches the given parameters *) - let search ~restarts (st:t) n_of_conflicts n_of_learnts : unit = - let conflictC = ref 0 in - while true do - check_invariants st; - match propagate st with - | Some confl -> (* Conflict *) - incr conflictC; - add_boolean_conflict st confl - - | None -> (* No Conflict *) - assert (st.elt_head = Vec.size st.trail); - assert (st.elt_head = st.th_head); - if Vec.size st.trail = n_vars st then raise Sat; - if restarts && n_of_conflicts > 0 && !conflictC >= n_of_conflicts then ( - Log.debug 2 "(sat.restarting)"; - cancel_until st (base_level st); - raise Restart - ); - (* if decision_level() = 0 then simplify (); *) - - if n_of_learnts >= 0 && - Vec.size st.clauses - Vec.size st.trail >= n_of_learnts then ( - reduce_db st; - ); - - pick_branch_lit st - done - - let eval_level (st:t) lit = - let var, negated = Var.make st lit in - if not var.v_pa.is_true && not var.v_na.is_true - then raise UndecidedLit - else assert (var.v_level >= 0); - let truth = var.v_pa.is_true in - let value = match negated with - | Theory_intf.Negated -> not truth - | Theory_intf.Same_sign -> truth - in - value, var.v_level - - let[@inline] eval st lit = fst (eval_level st lit) - let[@inline] unsat_conflict st = st.unsat_conflict - - let pp_trail st = - Log.debugf 5 - (fun k -> k "(@[sat.current_trail:@ %a@])" - (Vec.print ~sep:"" Atom.debug) st.trail) - - (* Add local hyps to the current decision level *) - let local (st:t) (assumptions:formula list) : unit = - let add_lit lit : unit = - let a = Atom.make st lit in - Log.debugf 3 (fun k-> k "(@[sat.local_assumption@ %a@])" Atom.debug a); - assert (decision_level st = base_level st); - let c = Clause.make [|a|] Hyp in - if not a.is_true then ( - if a.neg.is_true then ( - (* conflict between assumptions: UNSAT *) - report_unsat st c; - ) else ( - (* make a decision, propagate *) - enqueue_bool st a (Local c); - ) - ) - in - match st.unsat_conflict with - | None -> - Log.debug 3 "(sat.adding_local_assumptions)"; - List.iter add_lit assumptions - | Some _ -> - Log.debug 2 "(sat.local_assumptions.1: already unsat)" - - (* fixpoint of propagation and decisions until a model is found, or a - conflict is reached *) - let solve ?(restarts=true) ?(assumptions=[]) (st:t) : unit = - Log.debug 5 "(sat.solve)"; - if is_unsat st then raise Unsat; - let n_of_conflicts = ref (float_of_int restart_first) in - let n_of_learnts = ref ((float_of_int (nb_clauses st)) *. learntsize_factor) in - (* add clauses that are waiting in [to_add] *) - let rec add_clauses () = - match - Vec.filter_in_place (fun (permanent,c) -> add_clause ~permanent st c; false) st.to_add - with - | () -> call_solve() - | exception Conflict c -> - add_boolean_conflict st c; - call_solve() - and call_solve() = - match search ~restarts st (int_of_float !n_of_conflicts) (int_of_float !n_of_learnts) with - | () -> () - | exception Restart -> - n_of_conflicts := !n_of_conflicts *. restart_inc; - n_of_learnts := !n_of_learnts *. learntsize_inc; - check_invariants st; - call_solve() - | exception Conflict c -> - add_boolean_conflict st c; - call_solve() - | exception Sat -> - assert (st.elt_head = Vec.size st.trail); - check_invariants st; - begin match Th.if_sat (theory st) (full_slice st) with - | Theory_intf.Sat -> - (* if no propagation is to be done, exit; - otherwise continue loop *) - if propagation_fixpoint st then ( - pp_trail st; - raise Sat - ) else ( - add_clauses () - ) - | Theory_intf.Unsat (l, p) -> - let atoms = List.rev_map (Atom.make st) l in - let c = Clause.make_l atoms (Lemma p) in - Log.debugf 3 - (fun k -> k "(@[@{sat.theory_conflict_clause@}@ %a@])" Clause.debug c); - (* must backtrack *) - add_boolean_conflict st c - end - in - try - cancel_until st 0; - (* push decision level before calling [local] *) - new_decision_level st; - local st assumptions; - add_clauses() - with Sat -> () - - let assume ~permanent st ?tag cnf = - List.iter - (fun atoms -> - let atoms = List.rev_map (Atom.make st) atoms in - let c = Clause.make_l ?tag atoms Hyp in - add_clause_user st ~permanent c) - cnf - - (* Unsafe access to internal data *) - - let trail st = st.trail - - let check_model st : unit = - Log.debug 5 "(sat.check-model)"; - Vec.iter - (fun c -> - if not (Array.exists Atom.is_true c.atoms) then ( - Error.errorf "(@[sat.check-model.invalid-model@ :clause %a@])" Clause.debug c - )) - st.clauses -end -[@@inline] - diff --git a/src/sat/Sidekick_sat.ml b/src/sat/Sidekick_sat.ml deleted file mode 100644 index fdfea3fa..00000000 --- a/src/sat/Sidekick_sat.ml +++ /dev/null @@ -1,45 +0,0 @@ - -(** Main API *) - -module Theory_intf = Theory_intf - -module type S = Solver_intf.S - -type negated = Theory_intf.negated = - | Negated - | Same_sign - -type ('formula, 'proof) res = ('formula, 'proof) Theory_intf.res = - | Sat - (** The current set of assumptions is satisfiable. *) - | Unsat of 'formula list * 'proof - (** The current set of assumptions is *NOT* satisfiable, and here is a - theory tautology (with its proof), for which every literal is false - under the current assumptions. *) -(** Type returned by the theory. Formulas in the unsat clause must come from the - current set of assumptions, i.e must have been encountered in a slice. *) - -type 'form sat_state = 'form Solver_intf.sat_state = Sat_state of { - eval : 'form -> bool; - eval_level : 'form -> bool * int; - iter_trail : ('form -> unit) -> unit; -} - -type ('clause, 'proof) unsat_state = ('clause, 'proof) Solver_intf.unsat_state = Unsat_state of { - unsat_conflict : unit -> 'clause; - get_proof : unit -> 'proof; -} - -type 'clause export = 'clause Solver_intf.export = { - clauses : 'clause Vec.t; -} - -type ('form, 'proof) actions = ('form,'proof) Theory_intf.actions -type 'form slice_actions = 'form Theory_intf.slice_actions - -module Make = Solver.Make - -(**/**) -module Vec = Vec -module Log = Log -(**/**) diff --git a/src/sat/Sidekick_sat.mld b/src/sat/Sidekick_sat.mld deleted file mode 100644 index aaa7b537..00000000 --- a/src/sat/Sidekick_sat.mld +++ /dev/null @@ -1,75 +0,0 @@ -{1 mSAT} - -{2 License} - -This code is free, under the {{:https://github.com/c-cube/cdcl/blob/master/LICENSE}Apache 2.0 license}. - -{2 Contents} - -An ocaml library to implement CDCL(T) solvers. - -Most modules in CDCL actually define functors. These functors usually take one -or two arguments, usually an implementation of Terms and formulas used, and an implementation -of the theory used during solving. - -{4 Solver creation} - -The following modules allow to easily create a SAT or SMT solver (remark: a SAT solver is -simply an SMT solver with an empty theory). - -{!modules: -CDCL -} - -Finally, mSAT also provides an implementation of Tseitin's CNF conversion: - -{!modules: -CDCL_tseitin -} - -{4 Proof Management} - -CDCL solvers are able to provide detailed proofs when an unsat state is reached. To do -so, it require the provided theory to give proofs of the tautologies it gives the solver. -These proofs will be called lemmas. The type of lemmas is defined by the theory and can -very well be [unit]. - -In this context a proof is a resolution tree, whose conclusion (i.e. root) is the -empty clause, effectively allowing to deduce [false] from the hypotheses. -A resolution tree is a binary tree whose nodes are clauses. Inner nodes' clauses are -obtained by performing resolution between the two clauses of the children nodes, while -leafs of the tree are either hypotheses, or tautologies (i.e. conflicts returned by -the theory). - -{!modules: -CDCL__Res -CDCL__Res_intf -} - -Backends for exporting proofs to different formats: - -{!modules: -Dot -Coq -Dedukti -Backend_intf -} - -{4 Internal modules} - -WARNING: for advanced users only ! These modules expose a lot of unsafe functions -that must be used with care to not break the required invariants. Additionally, these -interfaces are not part of the main API and so are subject to a lot more breaking changes -than the safe modules above. - -{!modules: -Dimacs -Internal -External -Solver_types -Solver_types_intf -} - -{2 Index} - -{!indexlist} diff --git a/src/sat/Solver.ml b/src/sat/Solver.ml deleted file mode 100644 index 1c3bee8f..00000000 --- a/src/sat/Solver.ml +++ /dev/null @@ -1,121 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2016 Guillaume Bury -Copyright 2016 Simon Cruanes -*) - -module type S = Solver_intf.S - -open Solver_intf - -module Make (Th : Theory_intf.S) = struct - module S = Internal.Make(Th) - - module Proof = S.Proof - - exception UndecidedLit = S.UndecidedLit - - type formula = S.formula - type atom = S.atom - type clause = S.clause - type theory = Th.t - type proof = S.proof - type lemma = S.lemma - type premise = S.premise = - | Hyp - | Lemma of lemma - | Simplified of clause - | History of clause list - - type t = S.t - type solver = t - - let[@inline] create ?size () : t = S.create ?size () - - (* Result type *) - type res = - | Sat of formula sat_state - | Unsat of (clause,proof) unsat_state - - let pp_all st lvl status = - Log.debugf lvl - (fun k -> k - "@[%s - Full resume:@,@[Trail:@\n%a@]@,\ - @[Clauses:@\n%a@]@]@." - status - (Vec.print ~sep:"" S.Atom.debug) (S.trail st) - (Vec.print ~sep:"" S.Clause.debug) st.S.clauses - ) - - let mk_sat (st:S.t) : _ sat_state = - pp_all st 99 "SAT"; - let iter f : unit = Vec.iter (fun a -> f a.S.lit) (S.trail st) in - Sat_state { - eval = S.eval st; - eval_level = S.eval_level st; - iter_trail = iter; - } - - let mk_unsat (st:S.t) : (_,_) unsat_state = - pp_all st 99 "UNSAT"; - let unsat_conflict () = - match S.unsat_conflict st with - | None -> assert false - | Some c -> c - in - let get_proof () = unsat_conflict () in - Unsat_state { unsat_conflict; get_proof; } - - let theory = S.theory - - (* Wrappers around internal functions*) - let[@inline] assume ?(permanent=true) st ?tag cls : unit = - S.assume ~permanent st ?tag cls - - let[@inline] add_clause ~permanent st c : unit = - S.add_clause_user ~permanent st c - - let solve ?(restarts=true) (st:t) ?(assumptions=[]) () = - try - S.solve ~restarts ~assumptions st; - Sat (mk_sat st) - with S.Unsat -> - Unsat (mk_unsat st) - - let n_vars = S.n_vars - let unsat_core = S.Proof.unsat_core - - let true_at_level0 st a = - try - let b, lev = S.eval_level st a in - b && lev = 0 - with S.UndecidedLit -> false - - let[@inline] get_tag cl = S.(cl.tag) - - let actions = S.actions - - let export (st:t) : S.clause export = - let clauses = st.S.clauses in - {clauses} - - let check_model = S.check_model - - module Atom = S.Atom - - module Clause = struct - include S.Clause - - let forms c = atoms c |> IArray.of_array_map Atom.get_formula - let forms_l c = atoms_l c |> List.map Atom.get_formula - - let[@inline] make ?tag (a:atom array) : t = S.Clause.make ?tag a S.Hyp - let[@inline] make_l ?tag l : t = S.Clause.make_l ?tag l S.Hyp - - let of_formulas st ?tag l = - let l = List.map (Atom.make st) l in - make_l ?tag l - end - - module Formula = S.Formula -end diff --git a/src/sat/Solver.mli b/src/sat/Solver.mli deleted file mode 100644 index 4176bb3b..00000000 --- a/src/sat/Solver.mli +++ /dev/null @@ -1,22 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -(** SAT safe interface - - This module defines a safe interface for the core solver. - It is the basis of the {!module:Solver} and {!module:Mcsolver} modules. -*) - -module type S = Solver_intf.S -(** Safe external interface of solvers. *) - -module Make(Th : Theory_intf.S) - : S with type formula = Th.formula - and type theory = Th.t - and type lemma = Th.proof -(** Functor to make a safe external interface. *) - - diff --git a/src/sat/Solver_intf.ml b/src/sat/Solver_intf.ml deleted file mode 100644 index 3eda89bf..00000000 --- a/src/sat/Solver_intf.ml +++ /dev/null @@ -1,279 +0,0 @@ -(** Interface for Solvers - - This modules defines the safe external interface for solvers. - Solvers that implements this interface can be obtained using the [Make] - functor in {!Solver} or {!Mcsolver}. -*) - -module Var_fields = BitField.Make() -module C_fields = BitField.Make() - -type 'a printer = Format.formatter -> 'a -> unit - -type 'form sat_state = Sat_state of { - eval: 'form -> bool; - (** Returns the valuation of a formula in the current state - of the sat solver. - @raise UndecidedLit if the literal is not decided *) - eval_level: 'form -> bool * int; - (** Return the current assignement of the literals, as well as its - decision level. If the level is 0, then it is necessary for - the atom to have this value; otherwise it is due to choices - that can potentially be backtracked. - @raise UndecidedLit if the literal is not decided *) - iter_trail : ('form -> unit) -> unit; - (** Iter through the formulas and terms in order of decision/propagation - (starting from the first propagation, to the last propagation). *) -} -(** The type of values returned when the solver reaches a SAT state. *) - -type ('clause, 'proof) unsat_state = Unsat_state of { - unsat_conflict : unit -> 'clause; - (** Returns the unsat clause found at the toplevel *) - get_proof : unit -> 'proof; - (** returns a persistent proof of the empty clause from the Unsat result. *) -} -(** The type of values returned when the solver reaches an UNSAT state. *) - -type 'clause export = { - clauses: 'clause Vec.t; -} -(** Export internal state *) - -(** The external interface implemented by safe solvers, such as the one - created by the {!Solver.Make} and {!Mcsolver.Make} functors. *) -module type S = sig - (** {2 Internal modules} - These are the internal modules used, you should probably not use them - if you're not familiar with the internals of mSAT. *) - - type formula - (** The type of atoms given by the module argument for formulas. - An atom is a user-defined atomic formula whose truth value is - picked by Msat. *) - - - type atom (** SAT solver literals *) - - type clause (** SAT solver clauses *) - - type theory (** user theory *) - - type proof - (** Lazy type for proof trees. Proofs are persistent objects, and can be - extended to proof nodes using functions defined later. *) - - type lemma (** A theory lemma, used to justify a theory conflict clause *) - - type premise = - | Hyp - | Lemma of lemma - | Simplified of clause - | History of clause list - - type t - (** Main solver type, containing all state for solving. *) - - val create : ?size:[`Tiny|`Small|`Big] -> unit -> t - (** Create new solver - @param size the initial size of internal data structures. The bigger, - the faster, but also the more RAM it uses. *) - - (** {2 Types} *) - - (** Result type for the solver *) - type res = - | Sat of formula sat_state (** Returned when the solver reaches SAT, with a model *) - | Unsat of (clause,proof) unsat_state (** Returned when the solver reaches UNSAT, with a proof *) - - exception UndecidedLit - (** Exception raised by the evaluating functions when a literal - has not yet been assigned a value. *) - - (** {2 Base operations} *) - - val n_vars : t -> int - - val theory : t -> theory - - val assume : ?permanent:bool -> t -> ?tag:int -> formula list list -> unit - (** Add the list of clauses to the current set of assumptions. - Modifies the sat solver state in place. - @param permanent if true, kept after backtracking (default true) *) - - val add_clause : permanent:bool -> t -> clause -> unit - (** Lower level addition of clauses. See {!Clause} to create clauses. - @param permanent if true, kept after backtracking *) - - val solve : ?restarts:bool -> t -> ?assumptions:formula list -> unit -> res - (** Try and solves the current set of clauses. - @param assumptions additional atomic assumptions to be temporarily added. - The assumptions are just used for this call to [solve], they are - not saved in the solver's state. *) - - val unsat_core : proof -> clause list - (** Returns the unsat core of a given proof, ie a subset of all the added - clauses that is sufficient to establish unsatisfiability. *) - - val true_at_level0 : t -> formula -> bool - (** [true_at_level0 a] returns [true] if [a] was proved at level0, i.e. - it must hold in all models *) - - val get_tag : clause -> int option - (** Recover tag from a clause, if any *) - - (* FIXME - val push : t -> unit - (** Push a new save point. Clauses added after this call to [push] will - be added as normal, but the corresponding call to [pop] will - remove these clauses. *) - - val pop : t -> unit - (** Return to last save point, discarding clauses added since last - call to [push] *) - *) - - val actions : t -> (formula,lemma) Theory_intf.actions - (** Obtain actions *) - - val export : t -> clause export - - val check_model : t -> unit - - (** {2 Re-export some functions} *) - - type solver = t - - module Atom : sig - type t = atom - val is_pos : t -> bool - val neg : t -> t - val abs : t -> t - val compare : t -> t -> int - val equal : t -> t -> bool - val get_formula : t -> formula - val is_true : t -> bool - - val dummy : t - val make : solver -> formula -> t - - val pp : t printer - end - - (** A module to manipulate proofs. *) - module Proof : sig - type t = proof - - type node = { - conclusion : clause; (** The conclusion of the proof *) - step : step; (** The reasoning step used to prove the conclusion *) - } - (** A proof can be expanded into a proof node, which show the first step of the proof. *) - - (** The type of reasoning steps allowed in a proof. *) - and step = - | Hypothesis - (** The conclusion is a user-provided hypothesis *) - | Assumption - (** The conclusion has been locally assumed by the user *) - | Lemma of lemma - (** The conclusion is a tautology provided by the theory, with associated proof *) - | Duplicate of proof * atom list - (** The conclusion is obtained by eliminating multiple occurences of the atom in - the conclusion of the provided proof. *) - | Resolution of proof * proof * atom - (** The conclusion can be deduced by performing a resolution between the conclusions - of the two given proofs. The atom on which to perform the resolution is also given. *) - - exception Insufficient_hyps - (** Raised when a complete resolution derivation cannot be found using the current hypotheses. *) - - (** {3 Proof building functions} *) - - val prove : clause -> t - (** Given a clause, return a proof of that clause. - @raise Insuficient_hyps if it does not succeed. *) - - val prove_atom : atom -> t option - (** Given an atom [a], returns a proof of the clause [[a]] if [a] is true at level 0 *) - - (** {3 Proof Nodes} *) - - val is_leaf : step -> bool - (** Returns wether the the proof node is a leaf, i.e. an hypothesis, - an assumption, or a lemma. - [true] if and only if {parents} returns the empty list. *) - - val expl : step -> string - (** Returns a short string description for the proof step; for instance - ["hypothesis"] for a [Hypothesis] - (it currently returns the variant name in lowercase). *) - - val parents : step -> t list - (** Returns the parents of a proof node. *) - - (** {3 Proof Manipulation} *) - - val expand : proof -> node - (** Return the proof step at the root of a given proof. *) - - val step : proof -> step - - val conclusion : proof -> clause - (** What is proved at the root of the clause *) - - val fold : ('a -> node -> 'a) -> 'a -> t -> 'a - (** [fold f acc p], fold [f] over the proof [p] and all its node. It is guaranteed that - [f] is executed exactly once on each proof node in the tree, and that the execution of - [f] on a proof node happens after the execution on the parents of the nodes. *) - - val unsat_core : t -> clause list - (** Returns the unsat_core of the given proof, i.e the lists of conclusions - of all leafs of the proof. - More efficient than using the [fold] function since it has - access to the internal representation of proofs *) - - (** {3 Misc} *) - - val check : t -> unit - (** Check the contents of a proof. Mainly for internal use *) - - module Tbl : Hashtbl.S with type key = t - end - - module Clause : sig - type t = clause - - val atoms : t -> atom array (** do not modify *) - val atoms_l : t -> atom list - val forms : t -> formula IArray.t - val forms_l : t -> formula list - val tag : t -> int option - val equal : t -> t -> bool - - val make : ?tag:int -> atom array -> t - (** Make a clause from this array of SAT literals. - The array's ownership is transferred to the clause, do not mutate it *) - - val make_l : ?tag:int -> atom list -> t - - val of_formulas : solver -> ?tag:int -> formula list -> t - - val premise : t -> premise - val is_learnt : t -> bool - - val name : t -> string - val pp : t printer - val pp_dimacs : t printer - - val dummy : t - - module Tbl : Hashtbl.S with type key = t - end - - module Formula : sig - type t = formula - val pp : t printer - end -end - diff --git a/src/sat/Theory_intf.ml b/src/sat/Theory_intf.ml deleted file mode 100644 index 1155cbbf..00000000 --- a/src/sat/Theory_intf.ml +++ /dev/null @@ -1,142 +0,0 @@ -(**************************************************************************) -(* *) -(* Cubicle *) -(* Combining model checking algorithms and SMT solvers *) -(* *) -(* Sylvain Conchon, Evelyne Contejean *) -(* Francois Bobot, Mohamed Iguernelala, Alain Mebsout *) -(* CNRS, Universite Paris-Sud 11 *) -(* *) -(* Copyright 2011. This file is distributed under the terms of the *) -(* Apache Software License version 2.0 *) -(* *) -(**************************************************************************) -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2016 Guillaume Bury -Copyright 2016 Simon Cruanes -*) - -(** SMT Theory - - This module defines what a theory must implement in order to - be used in an SMT solver. -*) - -(** This type is used during the normalisation of formulas. - See {!val:Expr_intf.S.norm} for more details. *) -type negated = - | Negated (** changed sign *) - | Same_sign (** kept sign *) - -(** Type returned by the theory. Formulas in the unsat clause must come from the - current set of assumptions, i.e must have been encountered in a slice. *) -type ('formula, 'proof) res = - | Sat - (** The current set of assumptions is satisfiable. *) - | Unsat of 'formula list * 'proof - (** The current set of assumptions is *NOT* satisfiable, and here is a - theory tautology (with its proof), for which every literal is false - under the current assumptions. *) - -module type ACTIONS = sig - type formula - type proof - - val push_persistent : formula IArray.t -> proof -> unit - (** Allows to add a persistent clause to the solver. *) - - val push_local : formula IArray.t -> proof -> unit - (** Allows to add a local clause to the solver. The clause - will be removed after backtracking. *) - - val on_backtrack: (unit -> unit) -> unit - (** [on_backtrack f] calls [f] when the main solver backtracks *) - - val propagate : formula -> formula list -> proof -> unit - (** [propagate lit causes proof] informs the solver to propagate [lit], with the reason - that the clause [causes => lit] is a theory tautology. It is faster than pushing - the associated clause but the clause will not be remembered by the sat solver, - i.e it will not be used by the solver to do boolean propagation. *) -end - -(** Actions given to the theory during initialization, to be used - at any time *) -type ('form, 'proof) actions = - (module ACTIONS with type formula = 'form and type proof = 'proof) - -module type SLICE_ACTIONS = sig - type form - - val slice_iter : (form -> unit) -> unit - (** iterate on the slice of the trail *) -end - -type 'form slice_actions = (module SLICE_ACTIONS with type form = 'form) -(** The type for a slice. Slices are some kind of view of the current - propagation queue. They allow to look at the propagated literals, - and to add new clauses to the solver. *) - -(** {2 Signature for theories to be given to the Solver.} *) -module type S = sig - type t - (** State of the theory *) - - type formula - (** The type of formulas. Should be compatble with Formula_intf.S *) - - type proof - (** A custom type for the proofs of lemmas produced by the theory. *) - - module Form : sig - type t = formula - (** The type of atomic formulas. *) - - val equal : t -> t -> bool - (** Equality over formulas. *) - - val hash : t -> int - (** Hashing function for formulas. Should be such that two formulas equal according - to {!val:Expr_intf.S.equal} have the same hash. *) - - val print : Format.formatter -> t -> unit - (** Printing function used among other thing for debugging. *) - - val dummy : t - (** Formula constant. A valid formula should never be physically equal to [dummy] *) - - val neg : t -> t - (** Formula negation. Should be an involution, i.e. [equal a (neg neg a)] should - always hold. *) - - val norm : t -> t * negated - (** Returns a 'normalized' form of the formula, possibly negated - (in which case return [Negated]). This function is used to recognize - the link between a formula [a] and its negation [neg a], so the goal is - that [a] and [neg a] normalise to the same formula, - but one returns [Same_sign] and the other one returns [Negated] *) - end - - val create : (formula, proof) actions -> t - (** Create a new instance of the theory *) - - val assume : t -> formula slice_actions -> (formula, proof) res - (** Assume the formulas in the slice, possibly pushing new formulas to be propagated, - and returns the result of the new assumptions. *) - - val add_formula : t -> formula -> unit - (** Internalize formula for later use *) - - val if_sat : t -> formula slice_actions -> (formula, proof) res - (** Called at the end of the search in case a model has been found. If no new clause is - pushed, then 'sat' is returned, else search is resumed. *) - - val post_backtrack : t -> unit - (** After backtracking, this is called (can be used to invalidate - caches, reset task lists, etc.) *) - - (**/**) - val check_invariants : t -> unit - (**/**) -end - diff --git a/src/sat/dune b/src/sat/dune deleted file mode 100644 index eb992a93..00000000 --- a/src/sat/dune +++ /dev/null @@ -1,11 +0,0 @@ - -(library - (name Sidekick_sat) - (public_name sidekick.sat) - (synopsis "core SAT solver for Sidekick") - (libraries sidekick.util) - (flags :standard -w +a-4-42-44-48-50-58-32-60@8 - -color always -safe-string -open Sidekick_util) - (ocamlopt_flags :standard -O3 -bin-annot - -unbox-closures -unbox-closures-factor 20) - ) diff --git a/src/smt/Config.ml b/src/smt/Config.ml index 0e9b59ea..fa53d9e1 100644 --- a/src/smt/Config.ml +++ b/src/smt/Config.ml @@ -3,9 +3,9 @@ type 'a sequence = ('a -> unit) -> unit -module Key = Het_map.Key +module Key = CCHet.Key -type pair = Het_map.pair = +type pair = CCHet.pair = | Pair : 'a Key.t * 'a -> pair -include Het_map.Map +include CCHet.Map diff --git a/src/smt/Congruence_closure.ml b/src/smt/Congruence_closure.ml index a5a2b709..d84eb32c 100644 --- a/src/smt/Congruence_closure.ml +++ b/src/smt/Congruence_closure.ml @@ -1,6 +1,4 @@ -module Vec = Sidekick_sat.Vec -module Log = Sidekick_sat.Log open Solver_types module N = Equiv_class @@ -18,27 +16,14 @@ end module Sig_tbl = CCHashtbl.Make(Signature) -module type ACTIONS = sig - val on_backtrack: (unit -> unit) -> unit - (** Register a callback to be invoked upon backtracking below the current level *) - - val on_merge: repr -> repr -> explanation -> unit - (** Call this when two classes are merged *) - - val raise_conflict: conflict -> 'a - (** Report a conflict *) - - val propagate: Lit.t -> Lit.t list -> unit - (** Propagate a literal *) -end - -type actions = (module ACTIONS) - type explanation_thunk = explanation lazy_t +type combine_task = + | CT_merge of node * node * explanation_thunk + | CT_distinct of node list * int * explanation + type t = { tst: Term.state; - acts: actions; tbl: node Term.Tbl.t; (* internalization [term -> node] *) signatures_tbl : node Sig_tbl.t; @@ -50,14 +35,15 @@ type t = { that have the same "shape" (including head symbol) have the same signature *) pending: node Vec.t; - combine: (node * node * explanation_thunk) Vec.t; - on_backtrack:(unit->unit)->unit; + combine: combine_task Vec.t; + undo: (unit -> unit) Backtrack_stack.t; + on_merge: (repr -> repr -> explanation -> unit) option; mutable ps_lits: Lit.Set.t; (* proof state *) ps_queue: (node*node) Vec.t; (* pairs to explain *) - mutable true_ : node; - mutable false_ : node; + true_ : node lazy_t; + false_ : node lazy_t; } (* TODO: an additional union-find to keep track, for each term, of the terms they are known to be equal to, according @@ -65,18 +51,18 @@ type t = { several times. See "fast congruence closure and extensions", Nieuwenhis&al, page 14 *) -let[@inline] on_backtrack cc f : unit = cc.on_backtrack f let[@inline] is_root_ (n:node) : bool = n.n_root == n let[@inline] size_ (r:repr) = r.n_size +let[@inline] true_ cc = Lazy.force cc.true_ +let[@inline] false_ cc = Lazy.force cc.false_ + +let[@inline] on_backtrack cc f : unit = + Backtrack_stack.push_if_nonzero_level cc.undo f (* check if [t] is in the congruence closure. Invariant: [in_cc t ∧ do_cc t => forall u subterm t, in_cc u] *) let[@inline] mem (cc:t) (t:term): bool = Term.Tbl.mem cc.tbl t -let[@inline] post_backtrack cc = - Vec.clear cc.pending; - Vec.clear cc.combine - (* find representative, recursively *) let rec find_rec cc (n:node) : repr = if n==n.n_root then ( @@ -95,9 +81,6 @@ let iter_class_ (n:node) : node Sequence.t = in aux n -let[@inline] true_ cc = cc.true_ -let[@inline] false_ cc = cc.false_ - (* get term that should be there *) let[@inline] get_ cc (t:term) : node = try Term.Tbl.find cc.tbl t @@ -179,7 +162,7 @@ let push_combine cc t u e : unit = Log.debugf 5 (fun k->k "(@[cc.push_combine@ :t1 %a@ :t2 %a@ :expl %a@])" N.pp t N.pp u Explanation.pp (Lazy.force e)); - Vec.push cc.combine (t,u,e) + Vec.push cc.combine @@ CT_merge (t,u,e) (* re-root the explanation tree of the equivalence class of [n] so that it points to [n]. @@ -194,13 +177,12 @@ let rec reroot_expl (cc:t) (n:node): unit = n.n_expl <- E_none; end -let raise_conflict (cc:t) (e:conflict): _ = - let (module A) = cc.acts in +let raise_conflict (cc:t) (acts:sat_actions) (e:conflict): _ = (* clear tasks queue *) Vec.iter (N.set_field N.field_is_pending false) cc.pending; Vec.clear cc.pending; Vec.clear cc.combine; - A.raise_conflict e + acts.Msat.acts_raise_conflict e Proof_default let[@inline] all_classes cc : repr Sequence.t = Term.Tbl.values cc.tbl @@ -240,11 +222,6 @@ let find_common_ancestor (a:node) (b:node) : node = let[@inline] ps_add_obligation (cc:t) a b = Vec.push cc.ps_queue (a,b) let[@inline] ps_add_lit ps l = ps.ps_lits <- Lit.Set.add l ps.ps_lits -and ps_add_obligation_t cc (t1:term) (t2:term) = - let n1 = get_ cc t1 in - let n2 = get_ cc t2 in - ps_add_obligation cc n1 n2 - let ps_clear (cc:t) = cc.ps_lits <- Lit.Set.empty; Vec.clear cc.ps_queue; @@ -276,7 +253,7 @@ let rec explain_along_path ps (a:node) (parent_a:node) : unit = (* find explanation *) let explain_loop (cc : t) : Lit.Set.t = while not (Vec.is_empty cc.ps_queue) do - let a, b = Vec.pop_last cc.ps_queue in + let a, b = Vec.pop cc.ps_queue in Log.debugf 5 (fun k->k "(@[cc.explain_loop.at@ %a@ =?= %a@])" N.pp a N.pp b); assert (N.equal (find cc a) (find cc b)); @@ -292,12 +269,6 @@ let explain_eq_n ?(init=Lit.Set.empty) cc (n1:node) (n2:node) : Lit.Set.t = ps_add_obligation cc n1 n2; explain_loop cc -let explain_eq_t ?(init=Lit.Set.empty) cc (t1:term) (t2:term) : Lit.Set.t = - ps_clear cc; - cc.ps_lits <- init; - ps_add_obligation_t cc t1 t2; - explain_loop cc - let explain_unfold ?(init=Lit.Set.empty) cc (e:explanation) : Lit.Set.t = ps_clear cc; cc.ps_lits <- init; @@ -329,13 +300,22 @@ let relevant_subterms (t:Term.t) : Term.t Sequence.t = yield b; yield c +(* Checks if [ra] and [~into] have compatible normal forms and can + be merged w.r.t. the theories. + Side effect: also pushes sub-tasks *) +let notify_merge cc (ra:repr) ~into:(rb:repr) (e:explanation): unit = + assert (is_root_ rb); + match cc.on_merge with + | Some f -> f ra rb e + | None -> () + (* main CC algo: add terms from [pending] to the signature table, check for collisions *) -let rec update_tasks (cc:t): unit = +let rec update_tasks (cc:t) (acts:sat_actions) : unit = while not (Vec.is_empty cc.pending && Vec.is_empty cc.combine) do Vec.iter (task_pending_ cc) cc.pending; Vec.clear cc.pending; - Vec.iter (task_combine_ cc) cc.combine; + Vec.iter (task_combine_ cc acts) cc.combine; Vec.clear cc.combine; done @@ -356,7 +336,7 @@ and task_pending_ cc n = | App_cst (f1, a1), App_cst (f2, a2) -> assert (Cst.equal f1 f2); assert (IArray.length a1 = IArray.length a2); - Explanation.mk_merges @@ IArray.map2 (fun u1 u2 -> add_ cc u1, add_ cc u2) a1 a2 + Explanation.mk_merges @@ IArray.map2 (fun u1 u2 -> add_term_rec_ cc u1, add_term_rec_ cc u2) a1 a2 | If _, _ | App_cst _, _ | Bool _, _ -> assert false ) in @@ -368,9 +348,13 @@ and task_pending_ cc n = *) () +and[@inline] task_combine_ cc acts = function + | CT_merge (a,b,e_ab) -> task_merge_ cc acts a b e_ab + | CT_distinct (l,tag,e) -> task_distinct_ cc acts l tag e + (* main CC algo: merge equivalence classes in [st.combine]. @raise Exn_unsat if merge fails *) -and task_combine_ cc (a,b,e_ab) : unit = +and task_merge_ cc acts a b e_ab : unit = let ra = find cc a in let rb = find cc b in if not (N.equal ra rb) then ( @@ -387,15 +371,15 @@ and task_combine_ cc (a,b,e_ab) : unit = else ra, rb in (* check we're not merging [true] and [false] *) - if (N.equal ra cc.true_ && N.equal rb cc.false_) || - (N.equal rb cc.true_ && N.equal ra cc.false_) then ( + if (N.equal ra (true_ cc) && N.equal rb (false_ cc)) || + (N.equal rb (true_ cc) && N.equal ra (false_ cc)) then ( Log.debugf 5 (fun k->k "(@[cc.merge.true_false_conflict@ @[:r1 %a@]@ @[:r2 %a@]@ :e_ab %a@])" N.pp ra N.pp rb Explanation.pp e_ab); let lits = explain_unfold cc e_ab in let lits = explain_eq_n ~init:lits cc a ra in let lits = explain_eq_n ~init:lits cc b rb in - raise_conflict cc @@ Lit.Set.elements lits + raise_conflict cc acts @@ Lit.Set.elements lits ); (* update set of tags the new node cannot be equal to *) let new_tags = @@ -413,13 +397,16 @@ and task_combine_ cc (a,b,e_ab) : unit = let lits = explain_unfold ~init:lits cc e_ab in let lits = explain_eq_n ~init:lits cc a n1 in let lits = explain_eq_n ~init:lits cc b n2 in - raise_conflict cc @@ Lit.Set.elements lits) + raise_conflict cc acts @@ Lit.Set.elements lits) ra.n_tags rb.n_tags in (* when merging terms with [true] or [false], possibly propagate them to SAT *) let merge_bool r1 t1 r2 t2 = - if N.equal r1 cc.true_ then propagate_bools cc r2 t2 r1 t1 e_ab true - else if N.equal r1 cc.false_ then propagate_bools cc r2 t2 r1 t1 e_ab false + if N.equal r1 (true_ cc) then ( + propagate_bools cc acts r2 t2 r1 t1 e_ab true + ) else if N.equal r1 (false_ cc) then ( + propagate_bools cc acts r2 t2 r1 t1 e_ab false + ) in merge_bool ra a rb b; merge_bool rb b ra a; @@ -471,12 +458,28 @@ and task_combine_ cc (a,b,e_ab) : unit = notify_merge cc r_from ~into:r_into e_ab; ) +and task_distinct_ cc acts (l:node list) tag expl : unit = + let l = List.map (fun n -> n, find cc n) l in + let coll = + Sequence.diagonal_l l + |> Sequence.find_pred (fun ((_,r1),(_,r2)) -> N.equal r1 r2) + in + begin match coll with + | Some ((n1,_r1),(n2,_r2)) -> + (* two classes are already equal *) + Log.debugf 5 (fun k->k "(@[cc.distinct.conflict@ %a = %a@])" N.pp n1 N.pp n2); + let lits = explain_unfold cc expl in + acts.Msat.acts_raise_conflict (Lit.Set.to_list lits) Proof_default + | None -> + (* put a tag on all equivalence classes, that will make their merge fail *) + List.iter (fun (_,n) -> add_tag_n cc n tag expl) l + end + (* we are merging [r1] with [r2==Bool(sign)], so propagate each term [u1] in the equiv class of [r1] that is a known literal back to the SAT solver and which is not the one initially merged. We can explain the propagation with [u1 = t1 =e= t2 = r2==bool] *) -and propagate_bools cc r1 t1 r2 t2 (e_12:explanation) sign : unit = - let (module A) = cc.acts in +and propagate_bools cc acts r1 t1 r2 t2 (e_12:explanation) sign : unit = (* explanation for [t1 =e= t2 = r2] *) let half_expl = lazy ( let expl = explain_unfold cc e_12 in @@ -494,17 +497,10 @@ and propagate_bools cc r1 t1 r2 t2 (e_12:explanation) sign : unit = Log.debugf 5 (fun k->k "(@[cc.bool_propagate@ %a@])" Lit.pp lit); (* complete explanation with the [u1=t1] chunk *) let expl = explain_eq_n ~init:(Lazy.force half_expl) cc u1 t1 in - A.propagate lit (Lit.Set.to_list expl) + let reason = Msat.Consequence (Lit.Set.to_list expl, Proof_default) in + acts.Msat.acts_propagate lit reason )) -(* Checks if [ra] and [~into] have compatible normal forms and can - be merged w.r.t. the theories. - Side effect: also pushes sub-tasks *) -and notify_merge cc (ra:repr) ~into:(rb:repr) (e:explanation): unit = - assert (is_root_ rb); - let (module A) = cc.acts in - A.on_merge ra rb e - (* add [t] to [cc] when not present already *) and add_new_term_ cc (t:term) : node = assert (not @@ mem cc t); @@ -518,7 +514,7 @@ and add_new_term_ cc (t:term) : node = in (* add sub-term to [cc], and register [n] to its parents *) let add_sub_t (u:term) : unit = - let n_u = add_ cc u in + let n_u = add_term_rec_ cc u in add_to_parents_of_sub_node n_u in (* register sub-terms, add [t] to their parent list *) @@ -535,16 +531,16 @@ and add_new_term_ cc (t:term) : node = n (* add a term *) -and[@inline] add_ cc t : node = +and[@inline] add_term_rec_ cc t : node = try Term.Tbl.find cc.tbl t with Not_found -> add_new_term_ cc t let check_invariants_ (cc:t) = Log.debug 5 "(cc.check-invariants)"; Log.debugf 15 (fun k-> k "%a" pp_full cc); - assert (Term.equal (Term.true_ cc.tst) cc.true_.n_term); - assert (Term.equal (Term.false_ cc.tst) cc.false_.n_term); - assert (not @@ same_class cc cc.true_ cc.false_); + assert (Term.equal (Term.true_ cc.tst) (true_ cc).n_term); + assert (Term.equal (Term.false_ cc.tst) (false_ cc).n_term); + assert (not @@ same_class cc (true_ cc) (false_ cc)); assert (Vec.is_empty cc.combine); assert (Vec.is_empty cc.pending); (* check that subterms are internalized *) @@ -576,15 +572,23 @@ let check_invariants_ (cc:t) = let[@inline] check_invariants (cc:t) : unit = if Util._CHECK_INVARIANTS then check_invariants_ cc -let add cc t : node = - let n = add_ cc t in - update_tasks cc; - n +let[@inline] add cc t : node = add_term_rec_ cc t let add_seq cc seq = - seq (fun t -> ignore @@ add_ cc t); - update_tasks cc + seq (fun t -> ignore @@ add_term_rec_ cc t); + () +let[@inline] push_level (self:t) : unit = + Backtrack_stack.push_level self.undo + +let pop_levels (self:t) n : unit = + Backtrack_stack.pop_levels self.undo n ~f:(fun f -> f()); + Vec.clear self.pending; + Vec.clear self.combine; + () + +(* TODO: if a lit is [= a b], merge [a] and [b]; + if it's [distinct a1…an], make them distinct, etc. etc. *) (* assert that this boolean literal holds *) let assert_lit cc lit : unit = let t = Lit.view lit in @@ -593,69 +597,59 @@ let assert_lit cc lit : unit = let sign = Lit.sign lit in (* equate t and true/false *) let rhs = if sign then true_ cc else false_ cc in - let n = add_ cc t in + let n = add_term_rec_ cc t in (* TODO: ensure that this is O(1). basically, just have [n] point to true/false and thus acquire the corresponding value, so its superterms (like [ite]) can evaluate properly *) - push_combine cc n rhs (Lazy.from_val @@ E_lit lit); - update_tasks cc + push_combine cc n rhs (Lazy.from_val @@ E_lit lit) + +let[@inline] assert_lits cc lits : unit = + Sequence.iter (assert_lit cc) lits let assert_eq cc (t:term) (u:term) e : unit = - let n1 = add_ cc t in - let n2 = add_ cc u in + let n1 = add_term_rec_ cc t in + let n2 = add_term_rec_ cc u in if not (same_class cc n1 n2) then ( let e = Lazy.from_val @@ Explanation.E_lits e in push_combine cc n1 n2 e; - ); - update_tasks cc + ) let assert_distinct cc (l:term list) ~neq (lit:Lit.t) : unit = assert (match l with[] | [_] -> false | _ -> true); let tag = Term.id neq in Log.debugf 5 (fun k->k "(@[cc.assert_distinct@ (@[%a@])@ :tag %d@])" (Util.pp_list Term.pp) l tag); - let l = List.map (fun t -> t, add cc t |> find cc) l in - let coll = - Sequence.diagonal_l l - |> Sequence.find_pred (fun ((_,n1),(_,n2)) -> N.equal n1 n2) - in - begin match coll with - | Some ((t1,_n1),(t2,_n2)) -> - (* two classes are already equal *) - Log.debugf 5 (fun k->k "(@[cc.assert_distinct.conflict@ %a = %a@])" Term.pp t1 Term.pp t2); - let lits = Lit.Set.singleton lit in - let lits = explain_eq_t ~init:lits cc t1 t2 in - raise_conflict cc @@ Lit.Set.to_list lits - | None -> - (* put a tag on all equivalence classes, that will make their merge fail *) - List.iter (fun (_,n) -> add_tag_n cc n tag @@ Explanation.lit lit) l - end + let l = List.map (add cc) l in + Vec.push cc.combine @@ CT_distinct (l, tag, Explanation.lit lit) -let create ?(size=2048) ~actions (tst:Term.state) : t = - let nd = N.dummy in - let (module A : ACTIONS) = actions in - let cc = { +let create ?on_merge ?(size=`Big) (tst:Term.state) : t = + let size = match size with `Small -> 128 | `Big -> 2048 in + let rec cc = { tst; - acts=actions; tbl = Term.Tbl.create size; signatures_tbl = Sig_tbl.create size; - pending=Vec.make_empty N.dummy; - combine=Vec.make_empty (N.dummy,N.dummy,Lazy.from_val Explanation.dummy); + on_merge; + pending=Vec.create(); + combine=Vec.create(); ps_lits=Lit.Set.empty; - on_backtrack=A.on_backtrack; - ps_queue=Vec.make_empty (nd,nd); - true_ = N.dummy; - false_ = N.dummy; - } in - cc.true_ <- add_ cc (Term.true_ tst); - cc.false_ <- add_ cc (Term.false_ tst); - update_tasks cc; + undo=Backtrack_stack.create(); + ps_queue=Vec.create(); + true_; + false_; + } and true_ = lazy ( + add_term_rec_ cc (Term.true_ tst) + ) and false_ = lazy ( + add_term_rec_ cc (Term.false_ tst) + ) + in + ignore (Lazy.force true_ : node); + ignore (Lazy.force false_ : node); cc -let final_check cc : unit = - Log.debug 5 "(CC.final_check)"; - update_tasks cc +let[@inline] check cc acts : unit = + Log.debug 5 "(CC.check)"; + update_tasks cc acts (* model: map each uninterpreted equiv class to some ID *) let mk_model (cc:t) (m:Model.t) : Model.t = @@ -671,8 +665,8 @@ let mk_model (cc:t) (m:Model.t) : Model.t = let v = match Model.eval m t with | Some v -> v | None -> - if same_class cc r cc.true_ then Value.true_ - else if same_class cc r cc.false_ then Value.false_ + if same_class cc r (true_ cc) then Value.true_ + else if same_class cc r (false_ cc) then Value.false_ else ( Value.mk_elt (ID.makef "v_%d" @@ Term.id t) diff --git a/src/smt/Congruence_closure.mli b/src/smt/Congruence_closure.mli index adec138e..dbcbe985 100644 --- a/src/smt/Congruence_closure.mli +++ b/src/smt/Congruence_closure.mli @@ -13,25 +13,9 @@ type repr = Equiv_class.t type conflict = Theory.conflict -module type ACTIONS = sig - val on_backtrack: (unit -> unit) -> unit - (** Register a callback to be invoked upon backtracking below the current level *) - - val on_merge: repr -> repr -> explanation -> unit - (** Call this when two classes are merged *) - - val raise_conflict: conflict -> 'a - (** Report a conflict *) - - val propagate: Lit.t -> Lit.t list -> unit - (** Propagate a literal *) -end - -type actions = (module ACTIONS) - val create : - ?size:int -> - actions:actions -> + ?on_merge:(repr -> repr -> explanation -> unit) -> + ?size:[`Small | `Big] -> Term.state -> t (** Create a new congruence closure. @@ -55,6 +39,8 @@ val assert_lit : t -> Lit.t -> unit (** Given a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked. *) +val assert_lits : t -> Lit.t Sequence.t -> unit + val assert_eq : t -> term -> term -> Lit.t list -> unit val assert_distinct : t -> term list -> neq:term -> Lit.t -> unit @@ -62,9 +48,13 @@ val assert_distinct : t -> term list -> neq:term -> Lit.t -> unit with explanation [e] precond: [u = distinct l] *) -val final_check : t -> unit +val check : t -> sat_actions -> unit +(** Perform all pending operations done via {!assert_eq}, {!assert_lit}, etc. + Will use the [sat_actions] to propagate literals, declare conflicts, etc. *) -val post_backtrack : t -> unit +val push_level : t -> unit + +val pop_levels : t -> int -> unit val mk_model : t -> Model.t -> Model.t (** Enrich a model by mapping terms to their representative's value, diff --git a/src/smt/Equiv_class.ml b/src/smt/Equiv_class.ml index 6800cba4..bdcb9583 100644 --- a/src/smt/Equiv_class.ml +++ b/src/smt/Equiv_class.ml @@ -38,21 +38,14 @@ let set_payload ?(can_erase=fun _->false) n e = n.n_payload <- aux n.n_payload let payload_find ~f:p n = - begin match n.n_payload with + let[@unroll 2] rec aux = function | [] -> None | e1 :: tail -> - match p e1, tail with - | Some _ as res, _ -> res - | None, [] -> None - | None, e2 :: tail2 -> - match p e2, tail2 with - | Some _ as res, _ -> res - | None, [] -> None - | None, e3 :: tail3 -> - match p e3 with - | Some _ as res -> res - | None -> CCList.find_map p tail3 - end + match p e1 with + | Some _ as res -> res + | None -> aux tail + in + aux n.n_payload let payload_pred ~f:p n = begin match n.n_payload with @@ -71,5 +64,3 @@ module Tbl = CCHashtbl.Make(struct let equal = equal let hash = hash end) - -let dummy = make Term.dummy diff --git a/src/smt/Equiv_class.mli b/src/smt/Equiv_class.mli index 6d10d982..a2f03aa6 100644 --- a/src/smt/Equiv_class.mli +++ b/src/smt/Equiv_class.mli @@ -59,7 +59,3 @@ val get_field : Node_bits.field -> t -> bool val set_field : Node_bits.field -> bool -> t -> unit module Tbl : CCHashtbl.S with type key = t - -(**/**) -val dummy : t -(**/**) diff --git a/src/smt/Explanation.ml b/src/smt/Explanation.ml index 72e485b9..b1e1ee06 100644 --- a/src/smt/Explanation.ml +++ b/src/smt/Explanation.ml @@ -17,7 +17,6 @@ let mk_lit l : t = E_lit l let mk_lits = function [x] -> mk_lit x | l -> E_lits l let mk_reduction : t = E_reduction -let dummy = E_lit Lit.dummy let[@inline] lit l : t = E_lit l module Set = CCSet.Make(struct diff --git a/src/smt/Het_map.ml b/src/smt/Het_map.ml deleted file mode 100644 index 183a296f..00000000 --- a/src/smt/Het_map.ml +++ /dev/null @@ -1,191 +0,0 @@ - -(* This file is free software, part of containers. See file "license" for more details. *) - -(** {1 Associative containers with Heterogenerous Values} *) - -(*$R - let k1 : int Key.t = Key.create() in - let k2 : int Key.t = Key.create() in - let k3 : string Key.t = Key.create() in - let k4 : float Key.t = Key.create() in - - let tbl = Tbl.create () in - - Tbl.add tbl k1 1; - Tbl.add tbl k2 2; - Tbl.add tbl k3 "k3"; - - assert_equal (Some 1) (Tbl.find tbl k1); - assert_equal (Some 2) (Tbl.find tbl k2); - assert_equal (Some "k3") (Tbl.find tbl k3); - assert_equal None (Tbl.find tbl k4); - assert_equal 3 (Tbl.length tbl); - - Tbl.add tbl k1 10; - assert_equal (Some 10) (Tbl.find tbl k1); - assert_equal 3 (Tbl.length tbl); - assert_equal None (Tbl.find tbl k4); - - Tbl.add tbl k4 0.0; - assert_equal (Some 0.0) (Tbl.find tbl k4); - - () - - -*) - -type 'a sequence = ('a -> unit) -> unit -type 'a gen = unit -> 'a option - -module type KEY_IMPL = sig - type t - exception Store of t - val id : int -end - -module Key = struct - type 'a t = (module KEY_IMPL with type t = 'a) - - let _n = ref 0 - - let create (type k) () = - incr _n; - let id = !_n in - let module K = struct - type t = k - let id = id - exception Store of k - end in - (module K : KEY_IMPL with type t = k) - - let id (type k) (module K : KEY_IMPL with type t = k) = K.id - - let equal - : type a b. a t -> b t -> bool - = fun (module K1) (module K2) -> K1.id = K2.id -end - -type pair = - | Pair : 'a Key.t * 'a -> pair - -type exn_pair = - | E_pair : 'a Key.t * exn -> exn_pair - -let pair_of_e_pair (E_pair (k,e)) = - let module K = (val k) in - match e with - | K.Store v -> Pair (k,v) - | _ -> assert false - -module Tbl = struct - module M = Hashtbl.Make(struct - type t = int - let equal (i:int) j = i=j - let hash (i:int) = Hashtbl.hash i - end) - - type t = exn_pair M.t - - let create ?(size=16) () = M.create size - - let mem t k = M.mem t (Key.id k) - - let find_exn (type a) t (k : a Key.t) : a = - let module K = (val k) in - let E_pair (_, v) = M.find t K.id in - match v with - | K.Store v -> v - | _ -> assert false - - let find t k = - try Some (find_exn t k) - with Not_found -> None - - let add_pair_ t p = - let Pair (k,v) = p in - let module K = (val k) in - let p = E_pair (k, K.Store v) in - M.replace t K.id p - - let add t k v = add_pair_ t (Pair (k,v)) - - let length t = M.length t - - let iter f t = M.iter (fun _ pair -> f (pair_of_e_pair pair)) t - - let to_seq t yield = iter yield t - - let to_list t = M.fold (fun _ p l -> pair_of_e_pair p::l) t [] - - let add_list t l = List.iter (add_pair_ t) l - - let add_seq t seq = seq (add_pair_ t) - - let of_list l = - let t = create() in - add_list t l; - t - - let of_seq seq = - let t = create() in - add_seq t seq; - t -end - -module Map = struct - module M = Map.Make(struct - type t = int - let compare (i:int) j = Pervasives.compare i j - end) - - type t = exn_pair M.t - - let empty = M.empty - - let mem k t = M.mem (Key.id k) t - - let find_exn (type a) (k : a Key.t) t : a = - let module K = (val k) in - let E_pair (_, e) = M.find K.id t in - match e with - | K.Store v -> v - | _ -> assert false - - let find k t = - try Some (find_exn k t) - with Not_found -> None - - let add_e_pair_ p t = - let E_pair ((module K),_) = p in - M.add K.id p t - - let add_pair_ p t = - let Pair ((module K) as k,v) = p in - let p = E_pair (k, K.Store v) in - M.add K.id p t - - let add (type a) (k : a Key.t) v t = - let module K = (val k) in - add_e_pair_ (E_pair (k, K.Store v)) t - - let cardinal t = M.cardinal t - - let length = cardinal - - let iter f t = M.iter (fun _ p -> f (pair_of_e_pair p)) t - - let to_seq t yield = iter yield t - - let to_list t = M.fold (fun _ p l -> pair_of_e_pair p::l) t [] - - let add_list t l = List.fold_right add_pair_ l t - - let add_seq t seq = - let t = ref t in - seq (fun pair -> t := add_pair_ pair !t); - !t - - let of_list l = add_list empty l - - let of_seq seq = add_seq empty seq -end diff --git a/src/smt/Het_map.mli b/src/smt/Het_map.mli deleted file mode 100644 index 4b876906..00000000 --- a/src/smt/Het_map.mli +++ /dev/null @@ -1,85 +0,0 @@ - -(* This file is free software, part of containers. See file "license" for more details. *) - -(** {1 Associative containers with Heterogenerous Values} *) - -type 'a sequence = ('a -> unit) -> unit -type 'a gen = unit -> 'a option - -module Key : sig - type 'a t - - val create : unit -> 'a t - - val equal : 'a t -> 'a t -> bool - (** Compare two keys that have compatible types *) -end - -type pair = - | Pair : 'a Key.t * 'a -> pair - -(** {2 Imperative table indexed by {!Key}} *) -module Tbl : sig - type t - - val create : ?size:int -> unit -> t - - val mem : t -> _ Key.t -> bool - - val add : t -> 'a Key.t -> 'a -> unit - - val length : t -> int - - val find : t -> 'a Key.t -> 'a option - - val find_exn : t -> 'a Key.t -> 'a - (** @raise Not_found if the key is not in the table *) - - val iter : (pair -> unit) -> t -> unit - - val to_seq : t -> pair sequence - - val of_seq : pair sequence -> t - - val add_seq : t -> pair sequence -> unit - - val add_list : t -> pair list -> unit - - val of_list : pair list -> t - - val to_list : t -> pair list -end - -(** {2 Immutable map} *) -module Map : sig - type t - - val empty : t - - val mem : _ Key.t -> t -> bool - - val add : 'a Key.t -> 'a -> t -> t - - val length : t -> int - - val cardinal : t -> int - - val find : 'a Key.t -> t -> 'a option - - val find_exn : 'a Key.t -> t -> 'a - (** @raise Not_found if the key is not in the table *) - - val iter : (pair -> unit) -> t -> unit - - val to_seq : t -> pair sequence - - val of_seq : pair sequence -> t - - val add_seq : t -> pair sequence -> t - - val add_list : t -> pair list -> t - - val of_list : pair list -> t - - val to_list : t -> pair list -end diff --git a/src/util/ID.ml b/src/smt/ID.ml similarity index 100% rename from src/util/ID.ml rename to src/smt/ID.ml diff --git a/src/util/ID.mli b/src/smt/ID.mli similarity index 100% rename from src/util/ID.mli rename to src/smt/ID.mli diff --git a/src/smt/Lit.ml b/src/smt/Lit.ml index c2cae168..2554ea7c 100644 --- a/src/smt/Lit.ml +++ b/src/smt/Lit.ml @@ -6,8 +6,7 @@ type t = lit = { lit_sign : bool } -let neg l = {l with lit_sign=not l.lit_sign} - +let[@inline] neg l = {l with lit_sign=not l.lit_sign} let[@inline] sign t = t.lit_sign let[@inline] view (t:t): term = t.lit_term @@ -15,8 +14,6 @@ let[@inline] abs t: t = {t with lit_sign=true} let make ~sign t = {lit_sign=sign; lit_term=t} -let dummy = make ~sign:true Term.dummy - let atom ?(sign=true) (t:term) : t = let t, sign' = Term.abs t in let sign = if not sign' then not sign else sign in @@ -31,7 +28,7 @@ let pp = pp_lit let print = pp let norm l = - if l.lit_sign then l, Sidekick_sat.Same_sign else neg l, Sidekick_sat.Negated + if l.lit_sign then l, Msat.Solver_intf.Same_sign else neg l, Msat.Solver_intf.Negated module Set = CCSet.Make(struct type t = lit let compare=compare end) module Tbl = CCHashtbl.Make(struct type t = lit let equal=equal let hash=hash end) diff --git a/src/smt/Lit.mli b/src/smt/Lit.mli index 055fa373..073dbf05 100644 --- a/src/smt/Lit.mli +++ b/src/smt/Lit.mli @@ -12,14 +12,13 @@ val abs : t -> t val sign : t -> bool val view : t -> term val as_atom : t -> term * bool -val dummy : t val atom : ?sign:bool -> term -> t val hash : t -> int val compare : t -> t -> int val equal : t -> t -> bool val print : t Fmt.printer val pp : t Fmt.printer -val norm : t -> t * Sidekick_sat.negated +val norm : t -> t * Msat.Solver_intf.negated module Set : CCSet.S with type elt = t module Tbl : CCHashtbl.S with type key = t diff --git a/src/smt/Solver.ml b/src/smt/Solver.ml index 66a2888c..d5bec64f 100644 --- a/src/smt/Solver.ml +++ b/src/smt/Solver.ml @@ -11,10 +11,10 @@ let get_time : unit -> float = Sys.time (** {2 The Main Solver} *) -module Sat_solver = Sidekick_sat.Make(Theory_combine) +module Sat_solver = Msat.Make_cdcl_t(Theory_combine) let[@inline] clause_of_mclause (c:Sat_solver.clause): Lit.t IArray.t = - Sat_solver.Clause.forms c + Sat_solver.Clause.atoms c |> Array.map Sat_solver.Atom.formula |> IArray.of_array_unsafe module Proof = struct type t = Sat_solver.Proof.t @@ -59,13 +59,14 @@ let stats self = self.stat let[@inline] tst self = Theory_combine.tst (th_combine self) let create ?size ?(config=Config.empty) ~theories () : t = + let th_combine = Theory_combine.create() in let self = { - solver=Sat_solver.create ?size (); + solver=Sat_solver.create ?size th_combine; stat=Stat.create (); config; } in (* now add the theories *) - Theory_combine.add_theory_l (th_combine self) theories; + Theory_combine.add_theory_l th_combine theories; self (** {2 Sat Solver} *) @@ -193,8 +194,8 @@ let do_on_exit ~on_exit = let assume (self:t) (c:Lit.t IArray.t) : unit = let sat = solver self in - let c = Sat_solver.Clause.make (IArray.to_array_map (Sat_solver.Atom.make sat) c) in - Sat_solver.add_clause ~permanent:true sat c + let c = IArray.to_array_map (Sat_solver.make_atom sat) c in + Sat_solver.add_clause_a sat c Proof_default let[@inline] assume_eq self t u expl : unit = Congruence_closure.assert_eq (cc self) t u [expl] @@ -202,18 +203,22 @@ let[@inline] assume_eq self t u expl : unit = let[@inline] assume_distinct self l ~neq lit : unit = Congruence_closure.assert_distinct (cc self) l lit ~neq -let check_model (s:t) : unit = +let check_model (_s:t) : unit = Log.debug 1 "(smt.solver.check-model)"; + (* TODO Sat_solver.check_model s.solver + *) + () (* TODO: main loop with iterative deepening of the unrolling limit (not the value depth limit) *) -let solve ?restarts ?on_exit:(_=[]) ?check:(_=true) ~assumptions (self:t) : res = - let r = Sat_solver.solve ?restarts ~assumptions (solver self) () in +let solve ?on_exit:(_=[]) ?check:(_=true) ~assumptions (self:t) : res = + let r = Sat_solver.solve ~assumptions (solver self) in match r with - | Sat_solver.Sat (Sidekick_sat.Sat_state st) -> + | Sat_solver.Sat st -> Log.debugf 0 (fun k->k "SAT"); - let m = Theory_combine.mk_model (th_combine self) st.iter_trail in + let lits f = st.iter_trail f (fun _ -> ()) in + let m = Theory_combine.mk_model (th_combine self) lits in Sat m (* let env = Ast.env_empty in @@ -221,7 +226,7 @@ let solve ?restarts ?on_exit:(_=[]) ?check:(_=true) ~assumptions (self:t) : res … Unknown U_incomplete (* TODO *) *) - | Sat_solver.Unsat (Sidekick_sat.Unsat_state us) -> + | Sat_solver.Unsat us -> let pr = us.get_proof () in Unsat pr diff --git a/src/smt/Solver.mli b/src/smt/Solver.mli index f9b7887f..68fdc4e8 100644 --- a/src/smt/Solver.mli +++ b/src/smt/Solver.mli @@ -5,8 +5,8 @@ The solving algorithm, based on MCSat *) -module Sat_solver : Sidekick_sat.S - with type formula = Lit.t +module Sat_solver : Msat.S + with module Formula = Lit and type theory = Theory_combine.t and type lemma = Theory_combine.proof diff --git a/src/smt/Solver_types.ml b/src/smt/Solver_types.ml index 5b0e53ab..b0e80a1d 100644 --- a/src/smt/Solver_types.ml +++ b/src/smt/Solver_types.ml @@ -1,4 +1,7 @@ +module Vec = Msat.Vec +module Log = Msat.Log + module Fmt = CCFormat module Node_bits = CCBitField.Make(struct end) @@ -135,6 +138,10 @@ and value = and value_custom_view = .. +type proof = Proof_default + +type sat_actions = (Msat.void, lit, value, proof) Msat.acts + let[@inline] term_equal_ (a:term) b = a==b let[@inline] term_hash_ a = a.term_id let[@inline] term_cmp_ a b = CCInt.compare a.term_id b.term_id diff --git a/src/smt/Term.ml b/src/smt/Term.ml index d9ea0669..4dafbb5a 100644 --- a/src/smt/Term.ml +++ b/src/smt/Term.ml @@ -113,9 +113,3 @@ let as_cst_undef (t:term): (cst * Ty.Fun.t) option = | _ -> None let pp = Solver_types.pp_term - -let dummy : t = { - term_id= -1; - term_ty=Ty.prop; - term_view=Term_cell.true_; -} diff --git a/src/smt/Term.mli b/src/smt/Term.mli index 2d83f07a..a8a4feeb 100644 --- a/src/smt/Term.mli +++ b/src/smt/Term.mli @@ -56,7 +56,3 @@ val as_cst_undef : t -> (cst * Ty.Fun.t) option module Tbl : CCHashtbl.S with type key = t module Map : CCMap.S with type key = t - -(**/**) -val dummy : t -(**/**) diff --git a/src/smt/Theory.ml b/src/smt/Theory.ml index 9be25be6..9e282515 100644 --- a/src/smt/Theory.ml +++ b/src/smt/Theory.ml @@ -1,5 +1,5 @@ -module Clause : sig +module Th_clause : sig type t = Lit.t IArray.t val pp : t CCFormat.printer end = struct @@ -14,35 +14,6 @@ end = struct ) end -module type STATE = sig - type t - - val state : t - - val on_merge: t -> Equiv_class.t -> Equiv_class.t -> Explanation.t -> unit - (** Called when two classes are merged *) - - val on_assert: t -> Lit.t -> unit - (** Called when a literal becomes true *) - - val final_check: t -> Lit.t Sequence.t -> unit - (** Final check, must be complete (i.e. must raise a conflict - if the set of literals is not satisfiable) *) - - val mk_model : t -> Lit.t Sequence.t -> Model.t - (** Make a model for this theory's terms *) - - val post_backtrack : t -> unit - - (**/**) - val check_invariants : t -> unit - (**/**) -end - - -(** Runtime state of a theory, with all the operations it provides. *) -type state = (module STATE) - (** Unsatisfiable conjunction. Its negation will become a conflict clause *) type conflict = Lit.t list @@ -83,31 +54,63 @@ end type actions = (module ACTIONS) -type t = { - name: string; - make: Term.state -> actions -> state; -} +module type S = sig + type t -let make ~name ~make () : t = {name;make} + val name : string + (** Name of the theory *) -let make_st + val create : Term.state -> t + (** Instantiate the theory's state *) + + val on_merge: t -> actions -> Equiv_class.t -> Equiv_class.t -> Explanation.t -> unit + (** Called when two classes are merged *) + + val partial_check : t -> actions -> Lit.t Sequence.t -> unit + (** Called when a literal becomes true *) + + val final_check: t -> actions -> Lit.t Sequence.t -> unit + (** Final check, must be complete (i.e. must raise a conflict + if the set of literals is not satisfiable) *) + + val mk_model : t -> Lit.t Sequence.t -> Model.t + (** Make a model for this theory's terms *) + + val push_level : t -> unit + + val pop_levels : t -> int -> unit + + (**/**) + val check_invariants : t -> unit + (**/**) +end + +type t = (module S) + +type 'a t1 = (module S with type t = 'a) + +let make (type st) ?(check_invariants=fun _ -> ()) - ?(on_merge=fun _ _ _ _ -> ()) - ?(on_assert=fun _ _ -> ()) + ?(on_merge=fun _ _ _ _ _ -> ()) + ?(partial_check=fun _ _ _ -> ()) ?(mk_model=fun _ _ -> Model.empty) - ?(post_backtrack=fun _ -> ()) + ?(push_level=fun _ -> ()) + ?(pop_levels=fun _ _ -> ()) + ~name ~final_check - ~st - () : state = + ~create + () : t = let module A = struct type nonrec t = st - let state = st + let name = name + let create = create let on_merge = on_merge - let on_assert = on_assert + let partial_check = partial_check let final_check = final_check let mk_model = mk_model - let post_backtrack = post_backtrack let check_invariants = check_invariants + let push_level = push_level + let pop_levels = pop_levels end in - (module A : STATE) + (module A : S) diff --git a/src/smt/Theory_combine.ml b/src/smt/Theory_combine.ml index 090b46d2..bb726c89 100644 --- a/src/smt/Theory_combine.ml +++ b/src/smt/Theory_combine.ml @@ -3,13 +3,12 @@ (** Combine the congruence closure with a number of plugins *) -module Sat_solver = Sidekick_sat module C_clos = Congruence_closure open Solver_types module Proof = struct - type t = Proof - let default = Proof + type t = Solver_types.proof + let default = Proof_default end module Form = Lit @@ -18,60 +17,64 @@ type formula = Lit.t type proof = Proof.t type conflict = Theory.conflict -(* raise upon conflict *) -exception Exn_conflict of conflict +type theory_state = + | Th_state : ('a Theory.t1 * 'a) -> theory_state (* TODO: first-class module instead *) type t = { - cdcl_acts: (formula,proof) Sat_solver.actions; - (** actions provided by the SAT solver *) tst: Term.state; (** state for managing terms *) cc: C_clos.t lazy_t; (** congruence closure *) - mutable theories : Theory.state list; + mutable theories : theory_state list; (** Set of theories *) } let[@inline] cc t = Lazy.force t.cc let[@inline] tst t = t.tst -let[@inline] theories (self:t) : Theory.state Sequence.t = +let[@inline] theories (self:t) : theory_state Sequence.t = fun k -> List.iter k self.theories (** {2 Interface with the SAT solver} *) -(* handle a literal assumed by the SAT solver *) -let assume_lit (self:t) (lit:Lit.t) : unit = - Sat_solver.Log.debugf 2 - (fun k->k "(@[<1>@{th_combine.assume_lit@}@ @[%a@]@])" Lit.pp lit); - (* check consistency first *) - begin match Lit.view lit with - | {term_view=Bool true; _} -> () - | {term_view=Bool false; _} -> () - | _ -> - (* transmit to theories. *) - C_clos.assert_lit (cc self) lit; - theories self (fun (module Th) -> Th.on_assert Th.state lit); - end +module Plugin = struct -let with_conflict_catch f = +(* handle a literal assumed by the SAT solver *) +let assert_lits (self:t) acts (lits:Lit.t Sequence.t) : unit = + Msat.Log.debugf 2 + (fun k->k "(@[<1>@{th_combine.assume_lits@}@ @[%a@]@])" (Fmt.seq Lit.pp) lits); + (* transmit to theories. *) + C_clos.assert_lits (cc self) lits; + C_clos.check (cc self) acts; + theories self (fun (Th_state ((module Th),st)) -> Th.partial_check st acts lits); + () + +(* TODO: remove +let with_conflict_catch acts f = try f (); - Sat_solver.Sat with Exn_conflict lit_set -> let conflict_clause = IArray.of_list_map Lit.neg lit_set in - Sat_solver.Log.debugf 3 + Msat.Log.debugf 3 (fun k->k "(@[<1>@{th_combine.conflict@}@ :clause %a@])" Theory.Clause.pp conflict_clause); - Sat_solver.Unsat (IArray.to_list conflict_clause, Proof.default) + acts.Msat.acts_raise_conflict (IArray.to_list conflict_clause) Proof.default + *) + +let[@inline] iter_atoms_ acts : _ Sequence.t = + fun f -> + acts.Msat.acts_iter_assumptions + (function + | Msat.Lit a -> f a + | Msat.Assign _ -> assert false) (* propagation from the bool solver *) -let assume_real (self:t) (slice:Lit.t Sat_solver.slice_actions) = +let check_ (self:t) (acts:_ Msat.acts) = + let iter = iter_atoms_ acts in (* TODO if Config.progress then print_progress(); *) - let (module SA) = slice in - Log.debugf 5 (fun k->k "(th_combine.assume :len %d)" (Sequence.length @@ SA.slice_iter)); - with_conflict_catch - (fun () -> SA.slice_iter (assume_lit self)) + Msat.Log.debugf 5 (fun k->k "(th_combine.assume :len %d)" (Sequence.length iter)); + iter (assume_lit self); + Congruence_closure.check (cc self) acts let add_formula (self:t) (lit:Lit.t) = let t = Lit.view lit in @@ -81,19 +84,17 @@ let add_formula (self:t) (lit:Lit.t) = () (* propagation from the bool solver *) -let[@inline] assume (self:t) (slice:_ Sat_solver.slice_actions) = - assume_real self slice +let[@inline] partial_check (self:t) (acts:_ Msat.acts) = + check_ self acts (* perform final check of the model *) -let if_sat (self:t) (slice:Lit.t Sat_solver.slice_actions) : _ Sat_solver.res = +let final_check (self:t) (acts:_ Msat.acts) : unit = (* all formulas in the SAT solver's trail *) - let (module SA) = slice in - with_conflict_catch - (fun () -> - (* final check for CC + each theory *) - C_clos.final_check (cc self); - theories self - (fun (module Th) -> Th.final_check Th.state SA.slice_iter)) + let iter = iter_atoms_ acts in + (* final check for CC + each theory *) + Congruence_closure.check (cc self) acts; + theories self + (fun (module Th) -> Th.final_check Th.state iter) let mk_model (self:t) lits : Model.t = let m = @@ -107,44 +108,31 @@ let mk_model (self:t) lits : Model.t = (** {2 Various helpers} *) (* forward propagations from CC or theories directly to the SMT core *) -let act_propagate (self:t) f guard : unit = - let (module A) = self.cdcl_acts in - Sat_solver.Log.debugf 2 +let act_propagate acts f guard : unit = + Msat.Log.debugf 2 (fun k->k "(@[@{th.propagate@}@ %a@ :guard %a@])" Lit.pp f (Util.pp_list Lit.pp) guard); - A.propagate f guard Proof.default + let reason = Msat.Consequence (guard,Proof.default) in + acts.Msat.acts_propagate f reason (** {2 Interface to Congruence Closure} *) -let act_raise_conflict e = raise (Exn_conflict e) - (* when CC decided to merge [r1] and [r2], notify theories *) let on_merge_from_cc (self:t) r1 r2 e : unit = theories self (fun (module Th) -> Th.on_merge Th.state r1 r2 e) -let mk_cc_actions (self:t) : C_clos.actions = - let (module A) = self.cdcl_acts in - let module R = struct - let on_backtrack = A.on_backtrack - let on_merge = on_merge_from_cc self - let raise_conflict = act_raise_conflict - let propagate = act_propagate self - end in - (module R) - (** {2 Main} *) (* create a new theory combination *) -let create (cdcl_acts:_ Sat_solver.actions) : t = - Sat_solver.Log.debug 5 "th_combine.create"; +let create () : t = + Log.debug 5 "th_combine.create"; let rec self = { - cdcl_acts; tst=Term.create ~size:1024 (); cc = lazy ( (* lazily tie the knot *) - let actions = mk_cc_actions self in - C_clos.create ~size:1024 ~actions self.tst; + let on_merge = on_merge_from_cc self in + C_clos.create ~on_merge ~size:`Big self.tst; ); theories = []; } in @@ -165,17 +153,18 @@ let act_find self t = C_clos.add (cc self) t |> C_clos.find (cc self) +(* TODO: remove let act_add_local_axiom self c : unit = - Sat_solver.Log.debugf 5 (fun k->k "(@[<2>th_combine.push_local_lemma@ %a@])" Theory.Clause.pp c); - let (module A) = self.cdcl_acts in + Log.debugf 5 (fun k->k "(@[<2>th_combine.push_local_lemma@ %a@])" Theory.Clause.pp c); A.push_local c Proof.default (* push one clause into [M], in the current level (not a lemma but an axiom) *) let act_add_persistent_axiom self c : unit = - Sat_solver.Log.debugf 5 (fun k->k "(@[<2>th_combine.push_persistent_lemma@ %a@])" Theory.Clause.pp c); + Log.debugf 5 (fun k->k "(@[<2>th_combine.push_persistent_lemma@ %a@])" Theory.Clause.pp c); let (module A) = self.cdcl_acts in A.push_persistent c Proof.default + *) let check_invariants (self:t) = if Util._CHECK_INVARIANTS then ( diff --git a/src/smt/Theory_combine.mli b/src/smt/Theory_combine.mli index e78c766f..f8490ebc 100644 --- a/src/smt/Theory_combine.mli +++ b/src/smt/Theory_combine.mli @@ -4,16 +4,22 @@ (** Combine the congruence closure with a number of plugins *) module Proof : sig - type t = Proof + type t = Solver_types.proof (* dummy proofs, for now *) end -include Sidekick_sat.Theory_intf.S - with type formula = Lit.t +include Msat.Solver_intf.PLUGIN_CDCL_T + with module Formula = Lit and type proof = Proof.t +val create : unit -> t + val cc : t -> Congruence_closure.t val tst : t -> Term.state -val theories : t -> Theory.state Sequence.t + +type theory_state = + | Th_state : ('a Theory.t1 * 'a) -> theory_state + +val theories : t -> theory_state Sequence.t val mk_model : t -> Lit.t Sequence.t -> Model.t diff --git a/src/smt/dune b/src/smt/dune index 9ee87676..d3ded68d 100644 --- a/src/smt/dune +++ b/src/smt/dune @@ -2,8 +2,8 @@ (library (name Sidekick_smt) (public_name sidekick.smt) - (libraries containers containers.data sequence sidekick.util sidekick.sat zarith) - (flags :standard -w +a-4-44-48-58-60@8 + (libraries containers containers.data sequence sidekick.util msat zarith) + (flags :standard -warn-error -a+8 -color always -safe-string -short-paths -open Sidekick_util) (ocamlopt_flags :standard -O3 -color always -unbox-closures -unbox-closures-factor 20)) diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml index 94f47f11..621c7e7e 100644 --- a/src/smtlib/Process.ml +++ b/src/smtlib/Process.ml @@ -9,7 +9,7 @@ module E = CCResult module A = Ast module Form = Sidekick_th_bool module Fmt = CCFormat -module Dot = Sidekick_backend.Dot.Simple(Solver.Sat_solver) +module Dot = Msat_backend.Dot.Simple(Solver.Sat_solver) module Subst = struct type 'a t = 'a ID.Map.t diff --git a/src/smtlib/Typecheck.ml b/src/smtlib/Typecheck.ml index 36238be0..c96bc106 100644 --- a/src/smtlib/Typecheck.ml +++ b/src/smtlib/Typecheck.ml @@ -3,8 +3,10 @@ (** {1 Preprocessing AST} *) +module ID = Sidekick_smt.ID module Loc = Locations module Fmt = CCFormat +module Log = Msat.Log module A = Sidekick_smt.Ast module PA = Parse_ast @@ -324,7 +326,7 @@ let rec conv_term ctx (t:PA.term) : A.term = match t with errorf_ctx ctx "unsupported term %a" PA.pp_term t let find_file_ name ~dir : string option = - Sidekick_sat.Log.debugf 2 (fun k->k "search %s in %s" name dir); + Log.debugf 2 (fun k->k "search %s in %s" name dir); let abs_path = Filename.concat dir name in if Sys.file_exists abs_path then Some abs_path diff --git a/src/smtlib/dune b/src/smtlib/dune index 796f7983..d581cf95 100644 --- a/src/smtlib/dune +++ b/src/smtlib/dune @@ -2,8 +2,8 @@ (library (name sidekick_smtlib) (public_name sidekick.smtlib) - (libraries containers zarith sidekick.smt sidekick.util - sidekick.smt.th-bool sidekick.backend) + (libraries containers zarith msat sidekick.smt sidekick.util + sidekick.smt.th-bool msat.backend) (flags :standard -w +a-4-42-44-48-50-58-32-60@8 -safe-string -color always -open Sidekick_util) (ocamlopt_flags :standard -O3 -color always -bin-annot diff --git a/src/smt/th_bool/Sidekick_th_bool.ml b/src/th-bool/Sidekick_th_bool.ml similarity index 92% rename from src/smt/th_bool/Sidekick_th_bool.ml rename to src/th-bool/Sidekick_th_bool.ml index cd5d5551..e269cda5 100644 --- a/src/smt/th_bool/Sidekick_th_bool.ml +++ b/src/th-bool/Sidekick_th_bool.ml @@ -4,8 +4,6 @@ open Sidekick_smt open Solver_types -module Fmt = CCFormat - type term = Term.t (* TODO (long term): relevancy propagation *) @@ -168,12 +166,11 @@ end type t = { tst: Term.state; - acts: Theory.actions; } -let tseitin (self:t) (lit:Lit.t) (lit_t:term) (v:term view) : unit = +let tseitin (_self:t) (acts:Theory.actions) (lit:Lit.t) (lit_t:term) (v:term view) : unit = + let (module A) = acts in Log.debugf 5 (fun k->k "(@[th_bool.tseitin@ %a@])" Lit.pp lit); - let (module A) = self.acts in match v with | B_atom _ -> () | B_not _ -> assert false (* normalized *) @@ -236,23 +233,21 @@ let tseitin (self:t) (lit:Lit.t) (lit_t:term) (v:term view) : unit = guard ) -let on_assert (self:t) (lit:Lit.t) = - let t = Lit.view lit in - begin match view t with - | B_atom _ -> () - | v -> tseitin self lit t v - end +let partial_check (self:t) acts (lits:Lit.t Sequence.t) = + lits + (fun lit -> + let t = Lit.view lit in + match view t with + | B_atom _ -> () + | v -> tseitin self acts lit t v) -let final_check _ _ : unit = () +let final_check _ _ _ : unit = () let th = - let make tst acts = - let st = {tst;acts} in - Theory.make_st - ~on_assert - ~final_check - ?mk_model:None (* entirely interpreted *) - ~st - () - in - Theory.make ~name:"boolean" ~make () + Theory.make + ~partial_check + ~final_check + ~name:"boolean" + ~create:(fun tst -> {tst}) + ?mk_model:None (* entirely interpreted *) + () diff --git a/src/smt/th_bool/Sidekick_th_bool.mli b/src/th-bool/Sidekick_th_bool.mli similarity index 100% rename from src/smt/th_bool/Sidekick_th_bool.mli rename to src/th-bool/Sidekick_th_bool.mli diff --git a/src/smt/th_bool/dune b/src/th-bool/dune similarity index 100% rename from src/smt/th_bool/dune rename to src/th-bool/dune diff --git a/src/util/Backtrack_stack.ml b/src/util/Backtrack_stack.ml new file mode 100644 index 00000000..b4d955da --- /dev/null +++ b/src/util/Backtrack_stack.ml @@ -0,0 +1,35 @@ + +module Vec = Msat.Vec + +type 'a t = { + vec: 'a Vec.t; + lvls: int Vec.t; +} + +let create() : _ t = {vec=Vec.create(); lvls=Vec.create()} + +let[@inline] n_levels self : int = Vec.size self.vec + +let[@inline] push self x : unit = + Vec.push self.vec x + +let[@inline] push_if_nonzero_level self x : unit = + if n_levels self > 0 then ( + Vec.push self.vec x; + ) + +let[@inline] push_level (self:_ t) : unit = + Vec.push self.lvls (Vec.size self.vec) + + +let pop_levels (self:_ t) (n:int) ~f : unit = + if n > n_levels self then invalid_arg "Backtrack_stack.pop_levels"; + if n > 0 then ( + let new_lvl = n_levels self - n in + let i = Vec.get self.lvls new_lvl in + while Vec.size self.vec > i do + let x = Vec.pop self.vec in + f x + done; + Vec.shrink self.lvls i + ) diff --git a/src/util/Backtrack_stack.mli b/src/util/Backtrack_stack.mli new file mode 100644 index 00000000..e7125138 --- /dev/null +++ b/src/util/Backtrack_stack.mli @@ -0,0 +1,21 @@ + +(** {1 A backtracking stack} *) + +type 'a t + +val create : unit -> 'a t + +val push : 'a t -> 'a -> unit +(** Push an element onto the stack *) + +val push_if_nonzero_level : 'a t -> 'a -> unit +(** Push an element onto the stack if level > 0 *) + +val n_levels : _ t -> int +(** Number of levels *) + +val push_level : _ t -> unit +(** Push a backtracking point *) + +val pop_levels : 'a t -> int -> f:('a -> unit) -> unit +(** [pop_levels st n ~f] removes [n] levels, calling [f] on every removed item *) diff --git a/src/util/BitField.ml b/src/util/BitField.ml deleted file mode 100644 index 697320a8..00000000 --- a/src/util/BitField.ml +++ /dev/null @@ -1,135 +0,0 @@ -(* This file is free software, part of containers. See file "license" for more details. *) - -(** {1 Bit Field} *) - -exception TooManyFields -exception Frozen - -let max_width = Sys.word_size - 2 - -(*$R - let module B = CCBitField.Make(struct end) in - let x = B.mk_field () in - let y = B.mk_field () in - let z = B.mk_field () in - - let f = B.empty |> B.set x true |> B.set y true in - - assert_bool "z_false" (not (B.get z f)) ; - - assert_bool "z_true" (f |> B.set z true |> B.get z); -*) - -(*$R - let module B = CCBitField.Make(struct end) in - let _ = B.mk_field () in - B.freeze(); - assert_bool "must raise" - (try ignore (B.mk_field()); false with Frozen -> true); - -*) - -(*$R - let module B = CCBitField.Make(struct end) in - - let x = B.mk_field () in - let y = B.mk_field () in - let z = B.mk_field () in - let u = B.mk_field () in - B.freeze(); - - let f = B.empty - |> B.set y true - |> B.set z true - in - - assert_equal ~printer:CCInt.to_string 6 (f :> int) ; - - assert_equal false (B.get x f) ; - assert_equal true (B.get y f) ; - assert_equal true (B.get z f); - - let f' = B.set u true f in - - assert_equal false (B.get x f') ; - assert_equal true (B.get y f') ; - assert_equal true (B.get z f'); - assert_equal true (B.get u f'); - - () -*) - - -module type S = sig - type t = private int - (** Generative type of bitfields. Each instantiation of the functor - should create a new, incompatible type *) - - val empty : t - (** Empty bitfields (all bits 0) *) - - type field - - val get : field -> t -> bool - (** Get the value of this field *) - - val set : field -> bool -> t -> t - (** Set the value of this field *) - - val mk_field : unit -> field - (** Make a new field *) - - val freeze : unit -> unit - (** Prevent new fields from being added. From now on, creating - a field will raise Frozen *) - - val total_width : unit -> int - (** Current width of the bitfield *) -end - -(* all bits from 0 to w-1 set to true *) -let rec all_bits_ acc w = - if w=0 then acc - else - let acc = acc lor (1 lsl w-1) in - all_bits_ acc (w-1) - -(*$T - all_bits_ 0 1 = 1 - all_bits_ 0 2 = 3 - all_bits_ 0 3 = 7 - all_bits_ 0 4 = 15 -*) - -(* increment and return previous value *) -let get_then_incr n = - let x = !n in - incr n; - x - -module Make() : S = struct - type t = int - - let empty = 0 - - let width_ = ref 0 - let frozen_ = ref false - - type field = int (* a mask *) - - let[@inline] get field x = (x land field) <> 0 - - let[@inline] set field b x = - if b then x lor field else x land (lnot field) - - let mk_field () = - if !frozen_ then raise Frozen; - let n = get_then_incr width_ in - if n > max_width then raise TooManyFields; - let mask = 1 lsl n in - mask - - let freeze () = frozen_ := true - - let total_width () = !width_ -end diff --git a/src/util/BitField.mli b/src/util/BitField.mli deleted file mode 100644 index ac92ffd8..00000000 --- a/src/util/BitField.mli +++ /dev/null @@ -1,69 +0,0 @@ -(* This file is free software, part of containers. See file "license" for more details. *) - -(** {1 Bit Field} - - This module defines efficient bitfields - up to 30 or 62 bits (depending on the architecture) in - a relatively type-safe way. - - {[ - module B = CCBitField.Make(struct end);; - - #install_printer B.pp;; - - let x = B.mk_field () - let y = B.mk_field () - let z = B.mk_field () - - let f = B.empty |> B.set x true |> B.set y true;; - - assert (not (B.get z f)) ;; - - assert (f |> B.set z true |> B.get z);; - - ]} -*) - -exception TooManyFields -(** Raised when too many fields are packed into one bitfield *) - -exception Frozen -(** Raised when a frozen bitfield is modified *) - -val max_width : int -(** System-dependent maximum width for a bitfield, typically 30 or 62 *) - -(** {2 Bitfield Signature} *) -module type S = sig - type t = private int - (** Generative type of bitfields. Each instantiation of the functor - should create a new, incompatible type *) - - val empty : t - (** Empty bitfields (all bits 0) *) - - type field - - val get : field -> t -> bool - (** Get the value of this field *) - - val set : field -> bool -> t -> t - (** Set the value of this field *) - - val mk_field : unit -> field - (** Make a new field *) - - val freeze : unit -> unit - (** Prevent new fields from being added. From now on, creating - a field will raise Frozen *) - - val total_width : unit -> int - (** Current width of the bitfield *) -end - -(** Create a new bitfield type *) -module Make() : S - -(**/**) -val all_bits_ : int -> int -> int -(**/**) diff --git a/src/util/Heap.ml b/src/util/Heap.ml deleted file mode 100644 index 1709ce11..00000000 --- a/src/util/Heap.ml +++ /dev/null @@ -1,149 +0,0 @@ - -module type RANKED = Heap_intf.RANKED - -module type S = Heap_intf.S - -module Make(Elt : RANKED) = struct - type elt = Elt.t - - type t = { - heap : elt Vec.t; - } - - let _absent_index = -1 - - let create () = - { heap = Vec.make_empty Elt.dummy; } - - let[@inline] left i = (i lsl 1) + 1 (* i*2 + 1 *) - let[@inline] right i = (i + 1) lsl 1 (* (i+1)*2 *) - let[@inline] parent i = (i - 1) asr 1 (* (i-1) / 2 *) - - (* - let rec heap_property cmp ({heap=heap} as s) i = - i >= (Vec.size heap) || - ((i = 0 || not(cmp (Vec. get heap i) (Vec.get heap (parent i)))) - && heap_property cmp s (left i) && heap_property cmp s (right i)) - - let heap_property cmp s = heap_property cmp s 1 - *) - - (* [elt] is above or at its expected position. Move it up the heap - (towards the root) to restore the heap property *) - let percolate_up {heap} (elt:Elt.t) : unit = - let pi = ref (parent (Elt.idx elt)) in - let i = ref (Elt.idx elt) in - while !i <> 0 && Elt.cmp elt (Vec.get heap !pi) do - Vec.set heap !i (Vec.get heap !pi); - Elt.set_idx (Vec.get heap !i) !i; - i := !pi; - pi := parent !i - done; - Vec.set heap !i elt; - Elt.set_idx elt !i - - (* move [elt] towards the leaves of the heap to restore the heap - property *) - let percolate_down {heap} (elt:Elt.t): unit = - let sz = Vec.size heap in - let li = ref (left (Elt.idx elt)) in - let ri = ref (right (Elt.idx elt)) in - let i = ref (Elt.idx elt) in - begin - try - while !li < sz do - let child = - if !ri < sz && Elt.cmp (Vec.get heap !ri) (Vec.get heap !li) - then !ri - else !li - in - if not (Elt.cmp (Vec.get heap child) elt) then raise Exit; - Vec.set heap !i (Vec.get heap child); - Elt.set_idx (Vec.get heap !i) !i; - i := child; - li := left !i; - ri := right !i - done; - with Exit -> () - end; - Vec.set heap !i elt; - Elt.set_idx elt !i - - let[@inline] in_heap x = Elt.idx x >= 0 - - let[@inline] decrease s x = - assert (in_heap x); - percolate_up s x - - (* - let increase cmp s n = - assert (in_heap s n); percolate_down cmp s (V.get s.indices n) - *) - - let filter s filt = - let j = ref 0 in - let lim = Vec.size s.heap in - for i = 0 to lim - 1 do - if filt (Vec.get s.heap i) then ( - Vec.set s.heap !j (Vec.get s.heap i); - Elt.set_idx (Vec.get s.heap i) !j; - incr j; - ) else ( - Elt.set_idx (Vec.get s.heap i) _absent_index; - ); - done; - Vec.shrink s.heap (lim - !j); - for i = (lim / 2) - 1 downto 0 do - percolate_down s (Vec.get s.heap i) - done - - let size s = Vec.size s.heap - - let is_empty s = Vec.is_empty s.heap - - let clear {heap} = - Vec.iter (fun e -> Elt.set_idx e _absent_index) heap; - Vec.clear heap; - () - - let insert s elt = - if not (in_heap elt) then ( - Elt.set_idx elt (Vec.size s.heap); - Vec.push s.heap elt; - percolate_up s elt; - ) - - let[@inline] grow_to_at_least s sz = - Vec.grow_to_at_least s.heap sz - - let remove_min ({heap} as s) = - if Vec.size heap=0 then raise Not_found; - let x = Vec.get heap 0 in - Elt.set_idx x _absent_index; - let new_hd = Vec.last heap in (* heap.last() *) - Vec.set heap 0 new_hd; - Elt.set_idx new_hd 0; - Vec.pop heap; (* remove last *) - (* enforce heap property again *) - if Vec.size heap > 1 then ( - percolate_down s new_hd; - ); - x - - let remove ({heap} as s) (elt:elt) : unit = - if in_heap elt then ( - let i = Elt.idx elt in - (* move last element in place of [i] *) - let elt' = Vec.last heap in - Vec.set heap i elt'; - Elt.set_idx elt' i; - Elt.set_idx elt ~-1; - Vec.pop heap; - assert (not (in_heap elt)); - (* element put in place of [elt] might be too high *) - if Vec.size heap > i then ( - percolate_down s elt'; - ); - ) - -end diff --git a/src/util/Heap.mli b/src/util/Heap.mli deleted file mode 100644 index ef88dbf0..00000000 --- a/src/util/Heap.mli +++ /dev/null @@ -1,6 +0,0 @@ - -module type RANKED = Heap_intf.RANKED - -module type S = Heap_intf.S - -module Make(X : RANKED) : S with type elt = X.t diff --git a/src/util/Heap_intf.ml b/src/util/Heap_intf.ml deleted file mode 100644 index c3df6013..00000000 --- a/src/util/Heap_intf.ml +++ /dev/null @@ -1,56 +0,0 @@ - -module type RANKED = sig - type t - val idx: t -> int (** Index in heap. return -1 if never set *) - val set_idx : t -> int -> unit (** Update index in heap *) - val dummy : t - val cmp : t -> t -> bool -end - -module type S = sig - type elt - (** Type of elements *) - - type t - (** Heap of {!elt}, whose priority is increased or decreased - incrementally (see {!decrease} for instance) *) - - val create : unit -> t - (** Create a heap *) - - val decrease : t -> elt -> unit - (** [decrease h x] decreases the value associated to [x] within [h], - making it closer to the root (so, more prioritary) *) - - val in_heap : elt -> bool - - (*val increase : (int -> int -> bool) -> t -> int -> unit*) - - val size : t -> int - (** Number of integers within the heap *) - - val is_empty : t -> bool - - val clear : t -> unit - (** Clear the content of the heap *) - - val insert : t -> elt -> unit - (** Insert a new element into the heap *) - - val grow_to_at_least: t -> int -> unit - (** Hint: augment the internal capacity of the heap until it reaches at - least the given integer *) - - (*val update : (int -> int -> bool) -> t -> int -> unit*) - - val remove_min : t -> elt - (** Remove and return the integer that has the lowest value from the heap - @raise Not_found if the heap is empty *) - - val remove : t -> elt -> unit - (** Remove element from the heap. - precond: [in_heap elt] *) - - val filter : t -> (elt -> bool) -> unit - (** Filter out values that don't satisfy the predicate *) -end diff --git a/src/util/Log.ml b/src/util/Log.ml deleted file mode 100644 index f60603ea..00000000 --- a/src/util/Log.ml +++ /dev/null @@ -1,33 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -(** {1 Logging functions, real version} *) - -let enabled = true (* NOTE: change here for 0-overhead *) - -let debug_level_ = ref 0 -let set_debug l = debug_level_ := l -let get_debug () = !debug_level_ - -let debug_fmt_ = ref Format.err_formatter - -let set_debug_out f = debug_fmt_ := f - -(* does the printing, inconditionally *) -let debug_real_ l k = - k (fun fmt -> - Format.fprintf !debug_fmt_ "@[<2>@{[%d|%.3f]@}@ " - l (Sys.time()); - Format.kfprintf - (fun fmt -> Format.fprintf fmt "@]@.") - !debug_fmt_ fmt) - -let[@inline] debugf l k = - if enabled && l <= !debug_level_ then ( - debug_real_ l k; - ) - -let[@inline] debug l msg = debugf l (fun k->k "%s" msg) diff --git a/src/util/Log.mli b/src/util/Log.mli deleted file mode 100644 index 8923f8e3..00000000 --- a/src/util/Log.mli +++ /dev/null @@ -1,26 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -(** {1 Logging function, for debugging} *) - -val enabled : bool - -val set_debug : int -> unit (** Set debug level *) -val get_debug : unit -> int (** Current debug level *) - -val debugf : - int -> - ((('a, Format.formatter, unit, unit) format4 -> 'a) -> unit) -> - unit -(** Emit a debug message at the given level. If the level is lower - than [get_debug ()], the message will indeed be emitted *) - -val debug : int -> string -> unit -(** Simpler version of {!debug}, without formatting *) - -val set_debug_out : Format.formatter -> unit -(** Change the output formatter. *) - diff --git a/src/util/Vec.ml b/src/util/Vec.ml deleted file mode 100644 index e9371324..00000000 --- a/src/util/Vec.ml +++ /dev/null @@ -1,208 +0,0 @@ -(**************************************************************************) -(* *) -(* Cubicle *) -(* Combining model checking algorithms and SMT solvers *) -(* *) -(* Mohamed Iguernelala *) -(* Universite Paris-Sud 11 *) -(* *) -(* Copyright 2011. This file is distributed under the terms of the *) -(* Apache Software License version 2.0 *) -(* *) -(**************************************************************************) - -type 'a t = { - mutable dummy: 'a; - mutable data : 'a array; - mutable sz : int; -} - -let _size_too_big()= - failwith "Vec: capacity exceeds maximum array size" - -let make capa d = - if capa > Sys.max_array_length then _size_too_big(); - {data = Array.make capa d; sz = 0; dummy = d} - -let[@inline] make_empty d = {data = [||]; sz=0; dummy=d } - -let init capa f d = - if capa > Sys.max_array_length then _size_too_big(); - {data = Array.init capa (fun i -> f i); sz = capa; dummy = d} - -let from_array data sz d = - assert (sz <= Array.length data); - {data = data; sz = sz; dummy = d} - -let from_list l d = - let a = Array.of_list l in - from_array a (Array.length a) d - -let to_list s = - let l = ref [] in - for i = 0 to s.sz - 1 do - l := s.data.(i) :: !l - done; - List.rev !l - -let[@inline] clear s = s.sz <- 0 - -let[@inline] shrink t i = - assert (i >= 0); - assert (i<=t.sz); - t.sz <- i - -let[@inline] pop t = - if t.sz = 0 then invalid_arg "vec.pop"; - t.sz <- t.sz - 1 - -let[@inline] size t = t.sz - -let[@inline] is_empty t = t.sz = 0 - -let grow_to_exact t new_capa = - assert (new_capa > Array.length t.data); - let new_data = Array.make new_capa t.dummy in - assert (t.sz <= new_capa); - Array.blit t.data 0 new_data 0 t.sz; - t.data <- new_data - -let grow_to_double_size t = - if Array.length t.data = Sys.max_array_length then _size_too_big(); - let size = min Sys.max_array_length (2* Array.length t.data + 1) in - grow_to_exact t size - -let grow_to_at_least t new_capa = - assert (new_capa >= 0); - if new_capa > Sys.max_array_length then _size_too_big (); - let data = t.data in - let capa = ref (max (Array.length data) 1) in - while !capa < new_capa do - capa := min (2 * !capa + 1) Sys.max_array_length; - done; - if !capa > Array.length data then ( - grow_to_exact t !capa - ) - -let[@inline] is_full t = Array.length t.data = t.sz - -let[@inline] push t e = - if is_full t then grow_to_double_size t; - Array.unsafe_set t.data (t.sz) e; - t.sz <- t.sz + 1 - -let[@inline] last t = - if t.sz = 0 then invalid_arg "vec.last"; - Array.unsafe_get t.data (t.sz - 1) - -let[@inline] pop_last t = - if t.sz = 0 then invalid_arg "vec.pop_last"; - let x = Array.unsafe_get t.data (t.sz - 1) in - t.sz <- t.sz - 1; - x - -let[@inline] get t i = - if i < 0 || i >= t.sz then invalid_arg "vec.get"; - Array.unsafe_get t.data i - -let[@inline] set t i v = - if i < 0 || i > t.sz then invalid_arg "vec.set"; - if i = t.sz then ( - push t v - ) else ( - Array.unsafe_set t.data i v - ) - -let[@inline] copy t = - let data = Array.copy t.data in - {data; sz=t.sz; dummy=t.dummy} - -let[@inline] move_to t t' = - t'.data <- Array.copy t.data; - t'.sz <- t.sz - -let[@inline] fast_remove t i = - assert (i < t.sz); - t.data.(i) <- t.data.(t.sz - 1); - t.sz <- t.sz - 1 - -let filter_in_place f vec = - let i = ref 0 in - while !i < size vec do - if f (get vec !i) then incr i else fast_remove vec !i - done - -let sort t f = - let sub_arr = Array.sub t.data 0 t.sz in - Array.fast_sort f sub_arr; - t.data <- sub_arr - -let[@inline] iter f t = - for i = 0 to size t - 1 do - f (Array.unsafe_get t.data i) - done - -let append a b = - grow_to_at_least a (size a + size b); - iter (push a) b - -let append_l v l = List.iter (push v) l - -let fold f acc t = - let rec _fold f acc t i = - if i=t.sz - then acc - else ( - let acc' = f acc (Array.unsafe_get t.data i) in - _fold f acc' t (i+1) - ) - in _fold f acc t 0 - -exception ExitVec - -let exists p t = - try - for i = 0 to t.sz - 1 do - if p (Array.unsafe_get t.data i) then raise ExitVec - done; - false - with ExitVec -> true - -let for_all p t = - try - for i = 0 to t.sz - 1 do - if not (p (Array.unsafe_get t.data i)) then raise ExitVec - done; - true - with ExitVec -> false - -let print ?(sep=", ") pp out v = - let first = ref true in - iter - (fun x -> - if !first then first := false else Format.fprintf out "%s@," sep; - pp out x) - v - -(* -template -static inline void remove(V& ts, const T& t) -{ - int j = 0; - for (; j < ts.size() && ts[j] != t; j++); - assert(j < ts.size()); - ts[j] = ts.last(); - ts.pop(); -} -#endif - -template -static inline bool find(V& ts, const T& t) -{ - int j = 0; - for (; j < ts.size() && ts[j] != t; j++); - return j < ts.size(); -} - -#endif -*) diff --git a/src/util/Vec.mli b/src/util/Vec.mli deleted file mode 100644 index c7497020..00000000 --- a/src/util/Vec.mli +++ /dev/null @@ -1,120 +0,0 @@ -(**************************************************************************) -(* *) -(* Cubicle *) -(* Combining model checking algorithms and SMT solvers *) -(* *) -(* Mohamed Iguernelala *) -(* Universite Paris-Sud 11 *) -(* *) -(* Copyright 2011. This file is distributed under the terms of the *) -(* Apache Software License version 2.0 *) -(* *) -(**************************************************************************) - -type 'a t -(** Abstract type of vectors of 'a *) - -val make : int -> 'a -> 'a t -(** [make cap dummy] creates a new vector filled with [dummy]. The vector - is initially empty but its underlying array has capacity [cap]. - [dummy] will stay alive as long as the vector *) - -val make_empty : 'a -> 'a t -(** Vector with an empty capacity. The only argument is the dummy. *) - -val init : int -> (int -> 'a) -> 'a -> 'a t -(** Same as {!Array.init}, but also with a dummy element *) - -val from_array : 'a array -> int -> 'a -> 'a t -(** [from_array arr size dummy] takes ownership of [data] (no copy) - to create a vector. [size] is the length of the slice of [data] that is - used ([size <= Array.length data] must hold) *) - -val from_list : 'a list -> 'a -> 'a t - -val to_list : 'a t -> 'a list -(** Returns the list of elements of the vector *) - -val clear : 'a t -> unit -(** Set size to 0, doesn't free elements *) - -val shrink : 'a t -> int -> unit -(** [shrink vec sz] resets size of [vec] to [sz]. - Assumes [sz >=0 && sz <= size vec] *) - -val pop : 'a t -> unit -(** Pop last element - @raise Invalid_argument if the vector is empty *) - -val size : 'a t -> int - -val is_empty : 'a t -> bool - -val grow_to_exact : 'a t -> int -> unit - -val grow_to_double_size : 'a t -> unit - -val grow_to_at_least : 'a t -> int -> unit -(** [grow_to_at_least vec n] ensures that [capacity vec >= n] in - the most efficient way *) - -val is_full : 'a t -> bool -(** Is the capacity of the vector equal to the number of its elements? *) - -val push : 'a t -> 'a -> unit - -val append : 'a t -> 'a t -> unit -(** [append v1 v2] pushes all elements of [v2] into [v1] *) - -val append_l : 'a t -> 'a list -> unit - -val last : 'a t -> 'a -(** Last element, or - @raise Invalid_argument if the vector is empty *) - -val pop_last : 'a t -> 'a -(** Combine {!last} and {!pop}: remove last element and return it - @raise Invalid_argument if empty *) - -val get : 'a t -> int -> 'a -(** get the element at the given index, or - @raise Invalid_argument if the index is not valid *) - -val set : 'a t -> int -> 'a -> unit -(** set the element at the given index, either already set or the first - free slot if [not (is_full vec)], or - @raise Invalid_argument if the index is not valid *) - -val copy : 'a t -> 'a t -(** Fresh copy *) - -val move_to : 'a t -> 'a t -> unit -(** [move_to a b] copies the content of [a] to [b], discarding [b]'s old content *) - -val fast_remove : 'a t -> int -> unit -(** Remove element at index [i] without preserving order - (swap with last element) *) - -val filter_in_place : ('a -> bool) -> 'a t -> unit -(** [filter_in_place f v] removes from [v] the elements that do - not satisfy [f] *) - -val sort : 'a t -> ('a -> 'a -> int) -> unit -(** Sort in place the array *) - -val iter : ('a -> unit) -> 'a t -> unit -(** Iterate on elements *) - -val fold : ('b -> 'a -> 'b) -> 'b -> 'a t -> 'b -(** Fold over elements *) - -val exists : ('a -> bool) -> 'a t -> bool -(** Does there exist an element that satisfies the predicate? *) - -val for_all : ('a -> bool) -> 'a t -> bool -(** Do all elements satisfy the predicate? *) - -val print : - ?sep:string -> - (Format.formatter -> 'a -> unit) -> - Format.formatter -> 'a t -> unit diff --git a/src/util/dune b/src/util/dune index 841071c4..dc285068 100644 --- a/src/util/dune +++ b/src/util/dune @@ -1,7 +1,7 @@ (library (name sidekick_util) (public_name sidekick.util) - (libraries containers sequence) + (libraries containers sequence msat) (flags :standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string) (ocamlopt_flags :standard -O3 -bin-annot -unbox-closures -unbox-closures-factor 20)