mirror of
https://github.com/c-cube/sidekick.git
synced 2026-01-22 01:06:43 -05:00
wip: migrate to msat 0.8
This commit is contained in:
Simon Cruanes
parent
4fadbeb04d
commit
27d1841f6b
66 changed files with 359 additions and 5686 deletions
|
|
@ -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
|
||||
|
||||
|
|
@ -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
|
||||
"@[<v>p cnf %d %d@,%a@]@." n m
|
||||
(export_vec "Clauses") clauses
|
||||
end
|
||||
|
||||
|
|
@ -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. *)
|
||||
|
||||
|
|
@ -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 "<TR><TD colspan=\"2\">%a</TD></TR>" print_clause c;
|
||||
match l with
|
||||
| [] ->
|
||||
Format.fprintf fmt "<TR><TD BGCOLOR=\"%s\" colspan=\"2\">%s</TD></TR>" color rule
|
||||
| f :: r ->
|
||||
Format.fprintf fmt "<TR><TD BGCOLOR=\"%s\" rowspan=\"%d\">%s</TD><TD>%a</TD></TR>"
|
||||
color (List.length l) rule f ();
|
||||
List.iter (fun f -> Format.fprintf fmt "<TR><TD>%a</TD></TR>" f ()) r
|
||||
|
||||
let print_dot_node fmt id color c rule rule_color l =
|
||||
Format.fprintf fmt "%s [shape=plaintext, label=<<TABLE %a>%a</TABLE>>];@\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))
|
||||
|
|
@ -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. *)
|
||||
|
||||
|
|
@ -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)
|
||||
)
|
||||
|
||||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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)$
|
||||
|
||||
|
|
@ -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)
|
||||
)
|
||||
|
||||
|
|
@ -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] <file>"
|
||||
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),
|
||||
"<s>[kMGT] Sets the size limit for the sat solver";
|
||||
"-time", Arg.String (int_arg time_limit),
|
||||
"<t>[smhd] Sets the time limit for the sat solver";
|
||||
"-v", Arg.Int (fun i -> Log.set_debug i),
|
||||
"<lvl> 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
|
||||
|
||||
|
|
@ -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)
|
||||
|
||||
|
||||
|
|
@ -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. *)
|
||||
|
||||
|
|
@ -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 "@[<hov 0>%a@]" (fun _ -> Mi.iter aux) map
|
||||
|
||||
module type S = sig
|
||||
type 'a key
|
||||
val get : 'a key -> ('a key, 'b) t -> 'b
|
||||
val mem : 'a key -> ('a key, 'b) t -> bool
|
||||
val bind : 'a key -> 'b -> ('a key, 'b) t -> ('a key, 'b) t
|
||||
val remove : 'a key -> ('a key, 'b) t -> ('a key, 'b) t
|
||||
end
|
||||
|
||||
(* Variable substitutions *)
|
||||
module Id = struct
|
||||
type 'a key = 'a id
|
||||
let tok v = (v.index, 0)
|
||||
let get v s = snd (Mi.find (tok v) s)
|
||||
let mem v s = Mi.mem (tok v) s
|
||||
let bind v t s = Mi.add (tok v) (v, t) s
|
||||
let remove v s = Mi.remove (tok v) s
|
||||
end
|
||||
|
||||
end
|
||||
|
||||
(* Dummies *)
|
||||
(* ************************************************************************ *)
|
||||
|
||||
module Dummy = struct
|
||||
|
||||
let id_ttype =
|
||||
{ index = -1; id_name = "<dummy>"; id_type = Type; }
|
||||
|
||||
let ty =
|
||||
{ ty = TyVar id_ttype; ty_hash = -1; }
|
||||
|
||||
let id =
|
||||
{ index = -2; id_name = "<dummy>"; id_type = ty; }
|
||||
|
||||
let term =
|
||||
{ term = Var id; t_type = ty; t_hash = -1; }
|
||||
|
||||
let atom =
|
||||
{ atom = Pred term; sign = true; f_hash = -1; }
|
||||
|
||||
end
|
||||
|
||||
(* Variables *)
|
||||
(* ************************************************************************ *)
|
||||
|
||||
module Id = struct
|
||||
type 'a t = 'a id
|
||||
|
||||
(* Hash & comparisons *)
|
||||
let hash v = v.index
|
||||
|
||||
let compare: 'a. 'a id -> 'a id -> int =
|
||||
fun v1 v2 -> compare v1.index v2.index
|
||||
|
||||
let equal v1 v2 = compare v1 v2 = 0
|
||||
|
||||
(* Printing functions *)
|
||||
let print = Print.id
|
||||
|
||||
(* Id count *)
|
||||
let _count = ref 0
|
||||
|
||||
(* Constructors *)
|
||||
let mk_new id_name id_type =
|
||||
incr _count;
|
||||
let index = !_count in
|
||||
{ index; id_name; id_type }
|
||||
|
||||
let ttype name = mk_new name Type
|
||||
let ty name ty = mk_new name ty
|
||||
|
||||
let const name fun_vars fun_args fun_ret =
|
||||
mk_new name { fun_vars; fun_args; fun_ret; }
|
||||
|
||||
let ty_fun name n =
|
||||
let rec replicate acc n =
|
||||
if n <= 0 then acc
|
||||
else replicate (Type :: acc) (n - 1)
|
||||
in
|
||||
const name [] (replicate [] n) Type
|
||||
|
||||
let term_fun = const
|
||||
|
||||
(* Builtin Types *)
|
||||
let prop = ty_fun "Prop" 0
|
||||
let base = ty_fun "$i" 0
|
||||
|
||||
end
|
||||
|
||||
(* Types *)
|
||||
(* ************************************************************************ *)
|
||||
|
||||
module Ty = struct
|
||||
type t = ty
|
||||
type subst = (ttype id, ty) Subst.t
|
||||
|
||||
(* Hash & Comparisons *)
|
||||
let rec hash_aux t = match t.ty with
|
||||
| TyVar v -> Id.hash v
|
||||
| TyApp (f, args) ->
|
||||
Hashtbl.hash (Id.hash f, List.map hash args)
|
||||
|
||||
and hash t =
|
||||
if t.ty_hash = -1 then
|
||||
t.ty_hash <- hash_aux t;
|
||||
t.ty_hash
|
||||
|
||||
let discr ty = match ty.ty with
|
||||
| TyVar _ -> 1
|
||||
| TyApp _ -> 2
|
||||
|
||||
let rec compare u v =
|
||||
let hu = hash u and hv = hash v in
|
||||
if hu <> hv then Pervasives.compare hu hv
|
||||
else match u.ty, v.ty with
|
||||
| TyVar v1, TyVar v2 -> Id.compare v1 v2
|
||||
| TyApp (f1, args1), TyApp (f2, args2) ->
|
||||
begin match Id.compare f1 f2 with
|
||||
| 0 -> list_cmp compare args1 args2
|
||||
| x -> x
|
||||
end
|
||||
| _, _ -> Pervasives.compare (discr u) (discr v)
|
||||
|
||||
let equal u v =
|
||||
u == v || (hash u = hash v && compare u v = 0)
|
||||
|
||||
(* Printing functions *)
|
||||
let print = Print.ty
|
||||
|
||||
(* Constructors *)
|
||||
let mk_ty ty = { ty; ty_hash = -1; }
|
||||
|
||||
let of_id v = mk_ty (TyVar v)
|
||||
|
||||
let apply f args =
|
||||
assert (f.id_type.fun_vars = []);
|
||||
if List.length args <> List.length f.id_type.fun_args then
|
||||
raise (Bad_ty_arity (f, args))
|
||||
else
|
||||
mk_ty (TyApp (f, args))
|
||||
|
||||
(* Builtin types *)
|
||||
let prop = apply Id.prop []
|
||||
let base = apply Id.base []
|
||||
|
||||
(* Substitutions *)
|
||||
let rec subst_aux map t = match t.ty with
|
||||
| TyVar v -> begin try Subst.Id.get v map with Not_found -> t end
|
||||
| TyApp (f, args) ->
|
||||
let new_args = List.map (subst_aux map) args in
|
||||
if List.for_all2 (==) args new_args then t
|
||||
else apply f new_args
|
||||
|
||||
let subst map t = if Subst.is_empty map then t else subst_aux map t
|
||||
|
||||
(* Typechecking *)
|
||||
let instantiate f tys args =
|
||||
if List.length f.id_type.fun_vars <> List.length tys ||
|
||||
List.length f.id_type.fun_args <> List.length args then
|
||||
raise (Bad_arity (f, tys, args))
|
||||
else
|
||||
let map = List.fold_left2 (fun acc v ty -> Subst.Id.bind v ty acc) Subst.empty f.id_type.fun_vars tys in
|
||||
let fun_args = List.map (subst map) f.id_type.fun_args in
|
||||
List.iter2 (fun t ty ->
|
||||
if not (equal t.t_type ty) then raise (Type_mismatch (t, t.t_type, ty)))
|
||||
args fun_args;
|
||||
subst map f.id_type.fun_ret
|
||||
|
||||
end
|
||||
|
||||
(* Terms *)
|
||||
(* ************************************************************************ *)
|
||||
|
||||
module Term = struct
|
||||
type t = term
|
||||
type subst = (ty id, term) Subst.t
|
||||
|
||||
(* Hash & Comparisons *)
|
||||
let rec hash_aux t = match t.term with
|
||||
| Var v -> Id.hash v
|
||||
| App (f, tys, args) ->
|
||||
let l = List.map Ty.hash tys in
|
||||
let l' = List.map hash args in
|
||||
Hashtbl.hash (Id.hash f, l, l')
|
||||
|
||||
and hash t =
|
||||
if t.t_hash = -1 then
|
||||
t.t_hash <- hash_aux t;
|
||||
t.t_hash
|
||||
|
||||
let discr t = match t.term with
|
||||
| Var _ -> 1
|
||||
| App _ -> 2
|
||||
|
||||
let rec compare u v =
|
||||
let hu = hash u and hv = hash v in
|
||||
if hu <> hv then Pervasives.compare hu hv
|
||||
else match u.term, v.term with
|
||||
| Var v1, Var v2 -> Id.compare v1 v2
|
||||
| App (f1, tys1, args1), App (f2, tys2, args2) ->
|
||||
begin match Id.compare f1 f2 with
|
||||
| 0 ->
|
||||
begin match list_cmp Ty.compare tys1 tys2 with
|
||||
| 0 -> list_cmp compare args1 args2
|
||||
| x -> x
|
||||
end
|
||||
| x -> x
|
||||
end
|
||||
| _, _ -> Pervasives.compare (discr u) (discr v)
|
||||
|
||||
let equal u v =
|
||||
u == v || (hash u = hash v && compare u v = 0)
|
||||
|
||||
(* Printing functions *)
|
||||
let print = Print.term
|
||||
|
||||
(* Constructors *)
|
||||
let mk_term term t_type =
|
||||
{ term; t_type; t_hash = -1; }
|
||||
|
||||
let of_id v =
|
||||
mk_term (Var v) v.id_type
|
||||
|
||||
let apply f ty_args t_args =
|
||||
mk_term (App (f, ty_args, t_args)) (Ty.instantiate f ty_args t_args)
|
||||
|
||||
(* Substitutions *)
|
||||
let rec subst_aux ty_map t_map t = match t.term with
|
||||
| Var v -> begin try Subst.Id.get v t_map with Not_found -> t end
|
||||
| App (f, tys, args) ->
|
||||
let new_tys = List.map (Ty.subst ty_map) tys in
|
||||
let new_args = List.map (subst_aux ty_map t_map) args in
|
||||
if List.for_all2 (==) new_tys tys && List.for_all2 (==) new_args args then t
|
||||
else apply f new_tys new_args
|
||||
|
||||
let subst ty_map t_map t =
|
||||
if Subst.is_empty ty_map && Subst.is_empty t_map then
|
||||
t
|
||||
else
|
||||
subst_aux ty_map t_map t
|
||||
|
||||
let rec replace (t, t') t'' = match t''.term with
|
||||
| _ when equal t t'' -> t'
|
||||
| App (f, ty_args, t_args) ->
|
||||
apply f ty_args (List.map (replace (t, t')) t_args)
|
||||
| _ -> t''
|
||||
|
||||
end
|
||||
|
||||
(* Formulas *)
|
||||
(* ************************************************************************ *)
|
||||
|
||||
module Atom = struct
|
||||
type t = atom
|
||||
|
||||
type proof = unit
|
||||
|
||||
(* Hash & Comparisons *)
|
||||
let h_eq = 2
|
||||
let h_pred = 3
|
||||
|
||||
let rec hash_aux f = match f.atom with
|
||||
| Equal (t1, t2) ->
|
||||
Hashtbl.hash (h_eq, Term.hash t1, Term.hash t2)
|
||||
| Pred t ->
|
||||
Hashtbl.hash (h_pred, Term.hash t)
|
||||
|
||||
and hash f =
|
||||
if f.f_hash = -1 then
|
||||
f.f_hash <- hash_aux f;
|
||||
f.f_hash
|
||||
|
||||
let discr f = match f.atom with
|
||||
| Equal _ -> 1
|
||||
| Pred _ -> 2
|
||||
|
||||
let compare f g =
|
||||
let hf = hash f and hg = hash g in
|
||||
if hf <> hg then Pervasives.compare hf hg
|
||||
else match f.atom, g.atom with
|
||||
| Equal (u1, v1), Equal(u2, v2) ->
|
||||
list_cmp Term.compare [u1; v1] [u2; v2]
|
||||
| Pred t1, Pred t2 -> Term.compare t1 t2
|
||||
| _, _ -> Pervasives.compare (discr f) (discr g)
|
||||
|
||||
let equal u v =
|
||||
u == v || (hash u = hash v && compare u v = 0)
|
||||
|
||||
(* Printing functions *)
|
||||
let print = Print.atom
|
||||
|
||||
(* Constructors *)
|
||||
let mk_formula f = {
|
||||
sign = true;
|
||||
atom = f;
|
||||
f_hash = -1;
|
||||
}
|
||||
|
||||
let dummy = Dummy.atom
|
||||
|
||||
let pred t =
|
||||
if not (Ty.equal Ty.prop t.t_type) then
|
||||
raise (Type_mismatch (t, t.t_type, Ty.prop))
|
||||
else
|
||||
mk_formula (Pred t)
|
||||
|
||||
let 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
|
||||
|
||||
|
|
@ -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
|
||||
|
||||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
||||
|
|
@ -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
|
||||
|
||||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
||||
1580
src/sat/Internal.ml
1580
src/sat/Internal.ml
File diff suppressed because it is too large
Load diff
|
|
@ -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
|
||||
(**/**)
|
||||
|
|
@ -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}
|
||||
|
|
@ -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
|
||||
"@[<v>%s - Full resume:@,@[<hov 2>Trail:@\n%a@]@,\
|
||||
@[<hov 2>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
|
||||
|
|
@ -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. *)
|
||||
|
||||
|
||||
|
|
@ -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
|
||||
|
||||
|
|
@ -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
|
||||
|
||||
11
src/sat/dune
11
src/sat/dune
|
|
@ -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)
|
||||
)
|
||||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 "(@[<hv1>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 "(@[<hv>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)
|
||||
|
|
|
|||
|
|
@ -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,
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
(**/**)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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_;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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
|
||||
(**/**)
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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>@{<green>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>@{<green>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>@{<yellow>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 "(@[@{<green>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 (
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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))
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 *)
|
||||
()
|
||||
35
src/util/Backtrack_stack.ml
Normal file
35
src/util/Backtrack_stack.ml
Normal file
|
|
@ -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
|
||||
)
|
||||
21
src/util/Backtrack_stack.mli
Normal file
21
src/util/Backtrack_stack.mli
Normal file
|
|
@ -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 *)
|
||||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
(**/**)
|
||||
149
src/util/Heap.ml
149
src/util/Heap.ml
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
@ -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>@{<Blue>[%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)
|
||||
|
|
@ -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. *)
|
||||
|
||||
208
src/util/Vec.ml
208
src/util/Vec.ml
|
|
@ -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<class V, class T>
|
||||
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<class V, class T>
|
||||
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
|
||||
*)
|
||||
120
src/util/Vec.mli
120
src/util/Vec.mli
|
|
@ -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
|
||||
|
|
@ -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)
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue