mirror of
https://github.com/c-cube/sidekick.git
synced 2026-01-28 12:24:50 -05:00
remove dead library
This commit is contained in:
Simon Cruanes
parent
70749155bf
commit
c44e9bc16d
4 changed files with 0 additions and 376 deletions
|
|
@ -1,243 +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 Arg = Tseitin_intf.Arg
|
|
||||||
|
|
||||||
module type S = Tseitin_intf.S
|
|
||||||
|
|
||||||
module Make (A : Tseitin_intf.Arg) = struct
|
|
||||||
module F = A.Form
|
|
||||||
|
|
||||||
exception Empty_Or
|
|
||||||
type combinator = And | Or | Imp | Not
|
|
||||||
|
|
||||||
type atom = A.Form.t
|
|
||||||
type t =
|
|
||||||
| True
|
|
||||||
| Lit of atom
|
|
||||||
| Comb of combinator * t list
|
|
||||||
|
|
||||||
let rec print fmt phi =
|
|
||||||
match phi with
|
|
||||||
| True -> Format.fprintf fmt "true"
|
|
||||||
| Lit a -> F.print fmt a
|
|
||||||
| Comb (Not, [f]) ->
|
|
||||||
Format.fprintf fmt "not (%a)" print f
|
|
||||||
| Comb (And, l) -> Format.fprintf fmt "(%a)" (print_list "and") l
|
|
||||||
| Comb (Or, l) -> Format.fprintf fmt "(%a)" (print_list "or") l
|
|
||||||
| Comb (Imp, [f1; f2]) ->
|
|
||||||
Format.fprintf fmt "(%a => %a)" print f1 print f2
|
|
||||||
| _ -> assert false
|
|
||||||
and print_list sep fmt = function
|
|
||||||
| [] -> ()
|
|
||||||
| [f] -> print fmt f
|
|
||||||
| f::l -> Format.fprintf fmt "%a %s %a" print f sep (print_list sep) l
|
|
||||||
|
|
||||||
let make comb l = Comb (comb, l)
|
|
||||||
|
|
||||||
let make_atom p = Lit p
|
|
||||||
|
|
||||||
let f_true = True
|
|
||||||
let f_false = Comb(Not, [True])
|
|
||||||
|
|
||||||
let rec flatten comb acc = function
|
|
||||||
| [] -> acc
|
|
||||||
| (Comb (c, l)) :: r when c = comb ->
|
|
||||||
flatten comb (List.rev_append l acc) r
|
|
||||||
| a :: r ->
|
|
||||||
flatten comb (a :: acc) r
|
|
||||||
|
|
||||||
let rec opt_rev_map f acc = function
|
|
||||||
| [] -> acc
|
|
||||||
| a :: r -> begin match f a with
|
|
||||||
| None -> opt_rev_map f acc r
|
|
||||||
| Some b -> opt_rev_map f (b :: acc) r
|
|
||||||
end
|
|
||||||
|
|
||||||
let remove_true l =
|
|
||||||
let aux = function
|
|
||||||
| True -> None
|
|
||||||
| f -> Some f
|
|
||||||
in
|
|
||||||
opt_rev_map aux [] l
|
|
||||||
|
|
||||||
let remove_false l =
|
|
||||||
let aux = function
|
|
||||||
| Comb(Not, [True]) -> None
|
|
||||||
| f -> Some f
|
|
||||||
in
|
|
||||||
opt_rev_map aux [] l
|
|
||||||
|
|
||||||
|
|
||||||
let make_not f = make Not [f]
|
|
||||||
|
|
||||||
let make_and l =
|
|
||||||
let l' = remove_true (flatten And [] l) in
|
|
||||||
if List.exists ((=) f_false) l' then
|
|
||||||
f_false
|
|
||||||
else
|
|
||||||
make And l'
|
|
||||||
|
|
||||||
let make_or l =
|
|
||||||
let l' = remove_false (flatten Or [] l) in
|
|
||||||
if List.exists ((=) f_true) l' then
|
|
||||||
f_true
|
|
||||||
else match l' with
|
|
||||||
| [] -> raise Empty_Or
|
|
||||||
| [a] -> a
|
|
||||||
| _ -> Comb (Or, l')
|
|
||||||
|
|
||||||
let make_imply f1 f2 = make Imp [f1; f2]
|
|
||||||
let make_equiv f1 f2 = make_and [ make_imply f1 f2; make_imply f2 f1]
|
|
||||||
let make_xor f1 f2 = make_or [ make_and [ make_not f1; f2 ];
|
|
||||||
make_and [ f1; make_not f2 ] ]
|
|
||||||
|
|
||||||
(* simplify formula *)
|
|
||||||
let (%%) f g x = f (g x)
|
|
||||||
|
|
||||||
let rec sform f k = match f with
|
|
||||||
| True | Comb (Not, [True]) -> k f
|
|
||||||
| Comb (Not, [Lit a]) -> k (Lit (F.neg a))
|
|
||||||
| Comb (Not, [Comb (Not, [f])]) -> sform f k
|
|
||||||
| Comb (Not, [Comb (Or, l)]) -> sform_list_not [] l (k %% make_and)
|
|
||||||
| Comb (Not, [Comb (And, l)]) -> sform_list_not [] l (k %% make_or)
|
|
||||||
| Comb (And, l) -> sform_list [] l (k %% make_and)
|
|
||||||
| Comb (Or, l) -> sform_list [] l (k %% make_or)
|
|
||||||
| Comb (Imp, [f1; f2]) ->
|
|
||||||
sform (make_not f1) (fun f1' -> sform f2 (fun f2' -> k (make_or [f1'; f2'])))
|
|
||||||
| Comb (Not, [Comb (Imp, [f1; f2])]) ->
|
|
||||||
sform f1 (fun f1' -> sform (make_not f2) (fun f2' -> k (make_and [f1';f2'])))
|
|
||||||
| Comb ((Imp | Not), _) -> assert false
|
|
||||||
| Lit _ -> k f
|
|
||||||
and sform_list acc l k = match l with
|
|
||||||
| [] -> k acc
|
|
||||||
| f :: tail ->
|
|
||||||
sform f (fun f' -> sform_list (f'::acc) tail k)
|
|
||||||
and sform_list_not acc l k = match l with
|
|
||||||
| [] -> k acc
|
|
||||||
| f :: tail ->
|
|
||||||
sform (make_not f) (fun f' -> sform_list_not (f'::acc) tail k)
|
|
||||||
|
|
||||||
let ( @@ ) l1 l2 = List.rev_append l1 l2
|
|
||||||
(* let ( @ ) = `Use_rev_append_instead (* prevent use of non-tailrec append *) *)
|
|
||||||
|
|
||||||
type fresh_state = A.t
|
|
||||||
|
|
||||||
type state = {
|
|
||||||
fresh: fresh_state;
|
|
||||||
mutable acc_or : (atom * atom list) list;
|
|
||||||
mutable acc_and : (atom * atom list) list;
|
|
||||||
|
|
||||||
}
|
|
||||||
|
|
||||||
let create fresh : state = {
|
|
||||||
fresh;
|
|
||||||
acc_or=[];
|
|
||||||
acc_and=[];
|
|
||||||
}
|
|
||||||
|
|
||||||
let mk_proxy st : F.t = A.fresh st.fresh
|
|
||||||
|
|
||||||
(* build a clause by flattening (if sub-formulas have the
|
|
||||||
same combinator) and proxy-ing sub-formulas that have the
|
|
||||||
opposite operator. *)
|
|
||||||
let rec cnf st f = match f with
|
|
||||||
| Lit a -> None, [a]
|
|
||||||
| Comb (Not, [Lit a]) -> None, [F.neg a]
|
|
||||||
|
|
||||||
| Comb (And, l) ->
|
|
||||||
List.fold_left
|
|
||||||
(fun (_, acc) f ->
|
|
||||||
match cnf st f with
|
|
||||||
| _, [] -> assert false
|
|
||||||
| _cmb, [a] -> Some And, a :: acc
|
|
||||||
| Some And, l ->
|
|
||||||
Some And, l @@ acc
|
|
||||||
(* let proxy = mk_proxy () in *)
|
|
||||||
(* acc_and := (proxy, l) :: !acc_and; *)
|
|
||||||
(* proxy :: acc *)
|
|
||||||
| Some Or, l ->
|
|
||||||
let proxy = mk_proxy st in
|
|
||||||
st.acc_or <- (proxy, l) :: st.acc_or;
|
|
||||||
Some And, proxy :: acc
|
|
||||||
| None, l -> Some And, l @@ acc
|
|
||||||
| _ -> assert false
|
|
||||||
) (None, []) l
|
|
||||||
|
|
||||||
| Comb (Or, l) ->
|
|
||||||
List.fold_left
|
|
||||||
(fun (_, acc) f ->
|
|
||||||
match cnf st f with
|
|
||||||
| _, [] -> assert false
|
|
||||||
| _cmb, [a] -> Some Or, a :: acc
|
|
||||||
| Some Or, l ->
|
|
||||||
Some Or, l @@ acc
|
|
||||||
(* let proxy = mk_proxy () in *)
|
|
||||||
(* acc_or := (proxy, l) :: !acc_or; *)
|
|
||||||
(* proxy :: acc *)
|
|
||||||
| Some And, l ->
|
|
||||||
let proxy = mk_proxy st in
|
|
||||||
st.acc_and <- (proxy, l) :: st.acc_and;
|
|
||||||
Some Or, proxy :: acc
|
|
||||||
| None, l -> Some Or, l @@ acc
|
|
||||||
| _ -> assert false)
|
|
||||||
(None, []) l
|
|
||||||
| _ -> assert false
|
|
||||||
|
|
||||||
let cnf st f =
|
|
||||||
let acc = match f with
|
|
||||||
| True -> []
|
|
||||||
| Comb(Not, [True]) -> [[]]
|
|
||||||
| Comb (And, l) -> List.rev_map (fun f -> snd(cnf st f)) l
|
|
||||||
| _ -> [snd (cnf st f)]
|
|
||||||
in
|
|
||||||
let proxies = ref [] in
|
|
||||||
(* encore clauses that make proxies in !acc_and equivalent to
|
|
||||||
their clause *)
|
|
||||||
let acc =
|
|
||||||
List.fold_left
|
|
||||||
(fun acc (p,l) ->
|
|
||||||
proxies := p :: !proxies;
|
|
||||||
let np = F.neg p in
|
|
||||||
(* build clause [cl = l1 & l2 & ... & ln => p] where [l = [l1;l2;..]]
|
|
||||||
also add clauses [p => l1], [p => l2], etc. *)
|
|
||||||
let cl, acc =
|
|
||||||
List.fold_left
|
|
||||||
(fun (cl,acc) a -> (F.neg a :: cl), [np; a] :: acc)
|
|
||||||
([p],acc) l in
|
|
||||||
cl :: acc)
|
|
||||||
acc st.acc_and
|
|
||||||
in
|
|
||||||
(* encore clauses that make proxies in !acc_or equivalent to
|
|
||||||
their clause *)
|
|
||||||
let acc =
|
|
||||||
List.fold_left
|
|
||||||
(fun acc (p,l) ->
|
|
||||||
proxies := p :: !proxies;
|
|
||||||
(* add clause [p => l1 | l2 | ... | ln], and add clauses
|
|
||||||
[l1 => p], [l2 => p], etc. *)
|
|
||||||
let acc = List.fold_left (fun acc a -> [p; F.neg a]::acc)
|
|
||||||
acc l in
|
|
||||||
(F.neg p :: l) :: acc)
|
|
||||||
acc st.acc_or
|
|
||||||
in
|
|
||||||
acc
|
|
||||||
|
|
||||||
let make_cnf st f : _ list list =
|
|
||||||
st.acc_or <- [];
|
|
||||||
st.acc_and <- [];
|
|
||||||
cnf st (sform f (fun f' -> f'))
|
|
||||||
|
|
||||||
(* Naive CNF XXX remove???
|
|
||||||
let make_cnf f = mk_cnf (sform f)
|
|
||||||
*)
|
|
||||||
end
|
|
||||||
|
|
@ -1,22 +0,0 @@
|
||||||
(*
|
|
||||||
MSAT is free software, using the Apache license, see file LICENSE
|
|
||||||
Copyright 2014 Guillaume Bury
|
|
||||||
Copyright 2014 Simon Cruanes
|
|
||||||
*)
|
|
||||||
|
|
||||||
(** Tseitin CNF conversion
|
|
||||||
|
|
||||||
This modules implements Tseitin's Conjunctive Normal Form conversion, i.e.
|
|
||||||
the ability to transform an arbitrary boolean formula into an equi-satisfiable
|
|
||||||
CNF, that can then be fed to a SAT/SMT/McSat solver.
|
|
||||||
*)
|
|
||||||
|
|
||||||
module type Arg = Tseitin_intf.Arg
|
|
||||||
(** The implementation of formulas required to implement Tseitin's CNF conversion. *)
|
|
||||||
|
|
||||||
module type S = Tseitin_intf.S
|
|
||||||
(** The exposed interface of Tseitin's CNF conversion. *)
|
|
||||||
|
|
||||||
module Make(A : Arg) : S with type atom = A.Form.t and type fresh_state = A.t
|
|
||||||
(** This functor provides an implementation of Tseitin's CNF conversion. *)
|
|
||||||
|
|
||||||
|
|
@ -1,99 +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 *)
|
|
||||||
(* *)
|
|
||||||
(**************************************************************************)
|
|
||||||
|
|
||||||
(** Interfaces for Tseitin's CNF conversion *)
|
|
||||||
|
|
||||||
module type Arg = sig
|
|
||||||
(** Formulas
|
|
||||||
|
|
||||||
This defines what is needed of formulas in order to implement
|
|
||||||
Tseitin's CNF conversion.
|
|
||||||
*)
|
|
||||||
|
|
||||||
module Form : sig
|
|
||||||
type t
|
|
||||||
(** Type of atomic formulas. *)
|
|
||||||
|
|
||||||
val neg : t -> t
|
|
||||||
(** Negation of atomic formulas. *)
|
|
||||||
|
|
||||||
val print : Format.formatter -> t -> unit
|
|
||||||
(** Print the given formula. *)
|
|
||||||
end
|
|
||||||
|
|
||||||
type t
|
|
||||||
(** State *)
|
|
||||||
|
|
||||||
val fresh : t -> Form.t
|
|
||||||
(** Generate fresh formulas (that are different from any other). *)
|
|
||||||
|
|
||||||
end
|
|
||||||
|
|
||||||
module type S = sig
|
|
||||||
(** CNF conversion
|
|
||||||
|
|
||||||
This modules allows to convert arbitrary boolean formulas
|
|
||||||
into CNF.
|
|
||||||
*)
|
|
||||||
|
|
||||||
type atom
|
|
||||||
(** The type of atomic formulas. *)
|
|
||||||
|
|
||||||
type t
|
|
||||||
(** The type of arbitrary boolean formulas. Arbitrary boolean formulas
|
|
||||||
can be built using functions in this module, and then converted
|
|
||||||
to a CNF, which is a list of clauses that only use atomic formulas. *)
|
|
||||||
|
|
||||||
val f_true : t
|
|
||||||
(** The [true] formula, i.e a formula that is always satisfied. *)
|
|
||||||
|
|
||||||
val f_false : t
|
|
||||||
(** The [false] formula, i.e a formula that cannot be satisfied. *)
|
|
||||||
|
|
||||||
val make_atom : atom -> t
|
|
||||||
(** [make_atom p] builds the boolean formula equivalent to the atomic formula [p]. *)
|
|
||||||
|
|
||||||
val make_not : t -> t
|
|
||||||
(** Creates the negation of a boolean formula. *)
|
|
||||||
|
|
||||||
val make_and : t list -> t
|
|
||||||
(** Creates the conjunction of a list of formulas. An empty conjunction is always satisfied. *)
|
|
||||||
|
|
||||||
val make_or : t list -> t
|
|
||||||
(** Creates the disjunction of a list of formulas. An empty disjunction is never satisfied. *)
|
|
||||||
|
|
||||||
val make_xor : t -> t -> t
|
|
||||||
(** [make_xor p q] creates the boolean formula "[p] xor [q]". *)
|
|
||||||
|
|
||||||
val make_imply : t -> t -> t
|
|
||||||
(** [make_imply p q] creates the boolean formula "[p] implies [q]". *)
|
|
||||||
|
|
||||||
val make_equiv : t -> t -> t
|
|
||||||
(** [make_equiv p q] creates the boolena formula "[p] is equivalent to [q]". *)
|
|
||||||
|
|
||||||
type fresh_state
|
|
||||||
(** State used to produce fresh atoms *)
|
|
||||||
|
|
||||||
type state
|
|
||||||
(** State used for the Tseitin transformation *)
|
|
||||||
|
|
||||||
val create : fresh_state -> state
|
|
||||||
|
|
||||||
val make_cnf : state -> t -> atom list list
|
|
||||||
(** [make_cnf f] returns a conjunctive normal form of [f] under the form: a
|
|
||||||
list (which is a conjunction) of lists (which are disjunctions) of
|
|
||||||
atomic formulas. *)
|
|
||||||
|
|
||||||
val print : Format.formatter -> t -> unit
|
|
||||||
(** [print fmt f] prints the formula on the formatter [fmt].*)
|
|
||||||
|
|
||||||
end
|
|
||||||
|
|
@ -1,12 +0,0 @@
|
||||||
; vim:ft=lisp:
|
|
||||||
|
|
||||||
(library
|
|
||||||
((name CDCL_tseitin)
|
|
||||||
(public_name sidekick.tseitin)
|
|
||||||
(synopsis "Tseitin transformation for CDCL")
|
|
||||||
(libraries ())
|
|
||||||
(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