From 70749155bf2301726798ee3ab695442a1050c305 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 9 May 2018 19:34:53 -0500 Subject: [PATCH] cleanup of unused sublibrary --- Makefile | 11 ++--- src/th_sat/Sidekick_th_sat.ml | 9 ---- src/th_sat/Sidekick_th_sat.mli | 16 ------- src/th_sat/Th_sat.ml | 87 ---------------------------------- src/th_sat/Th_sat.mli | 31 ------------ src/th_sat/jbuild | 13 ----- 6 files changed, 4 insertions(+), 163 deletions(-) delete mode 100644 src/th_sat/Sidekick_th_sat.ml delete mode 100644 src/th_sat/Sidekick_th_sat.mli delete mode 100644 src/th_sat/Th_sat.ml delete mode 100644 src/th_sat/Th_sat.mli delete mode 100644 src/th_sat/jbuild diff --git a/Makefile b/Makefile index 7f69cdbf..ebc66e93 100644 --- a/Makefile +++ b/Makefile @@ -3,20 +3,17 @@ .PHONY: clean build build-dev -NAME=msat J?=3 TIMEOUT?=30 -TARGETS=src/main/main.exe OPTS= -j $(J) -build: - jbuilder build $(TARGETS) $(OPTS) - build-install: - jbuilder build @install + jbuilder build $(OPTS) @install + +build: build-install build-dev: - jbuilder build $(TARGETS) $(OPTS) --dev + jbuilder build $(OPTS) --dev enable_log: cd src/core; ln -sf log_real.ml log.ml diff --git a/src/th_sat/Sidekick_th_sat.ml b/src/th_sat/Sidekick_th_sat.ml deleted file mode 100644 index 8a710fe4..00000000 --- a/src/th_sat/Sidekick_th_sat.ml +++ /dev/null @@ -1,9 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2016 Guillaume Bury -*) - -module Th = Th_sat - -include DAgon_sat.Make(Th) - diff --git a/src/th_sat/Sidekick_th_sat.mli b/src/th_sat/Sidekick_th_sat.mli deleted file mode 100644 index cdd20ab8..00000000 --- a/src/th_sat/Sidekick_th_sat.mli +++ /dev/null @@ -1,16 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2016 Guillaume Bury -*) - -(** Sat solver - - This modules instanciates a pure sat solver using integers to represent - atomic propositions. -*) - -module Th = Th_sat - -include module type of Sidekick_sat.Make(Th) -(** A functor that can generate as many solvers as needed. *) - diff --git a/src/th_sat/Th_sat.ml b/src/th_sat/Th_sat.ml deleted file mode 100644 index 0916cf97..00000000 --- a/src/th_sat/Th_sat.ml +++ /dev/null @@ -1,87 +0,0 @@ - -exception Bad_atom -(** Exception raised if an atom cannot be created *) - -type proof = unit -(** A empty type for proofs *) - -type formula = int - -type t = { - actions: (formula, proof) CDCL.actions; - mutable max_index: int; - mutable max_fresh: int; -} - -let create actions : t = { - actions; - max_index = 0; - max_fresh= (-1); -} - -module Form = struct - type t = formula - (** Atoms are represented as integers. [-i] begin the negation of [i]. - Additionally, since we nee dot be able to create fresh atoms, we - use even integers for user-created atoms, and odd integers for the - fresh atoms. *) - - let max_lit = max_int - - let hash (a:int) = a land max_int - let equal (a:int) b = a=b - let compare (a:int) b = Pervasives.compare a b - - (** Internal function for creating atoms. - Updates the internal counters *) - let make_ st i = - if i <> 0 && (abs i) < max_lit then ( - st.max_index <- max st.max_index (abs i); - i - ) else ( - raise Bad_atom - ) - - (** A dummy atom *) - let dummy = 0 - - let neg a = - a - - let norm a = - abs a, if a < 0 then - CDCL.Negated - else - CDCL.Same_sign - - let print fmt a = - Format.fprintf fmt "%s%s%d" - (if a < 0 then "~" else "") - (if a mod 2 = 0 then "v" else "f") - ((abs a) / 2) - -end - -let abs = abs - -let sign i = i > 0 - -let apply_sign b i = if b then i else Form.neg i - -let set_sign b i = if b then abs i else Form.neg (abs i) - -let make st i = Form.make_ st (2 * i) - -let fresh st = - st.max_fresh <- 1 + st.max_fresh; - Form.make_ st (2 * st.max_fresh + 1) - -(* -let iter: (t -> unit) -> unit = fun f -> - for j = 1 to !max_index do - f j - done -*) - -let assume _ _ = CDCL.Theory_intf.Sat - -let if_sat _ _ = CDCL.Theory_intf.Sat diff --git a/src/th_sat/Th_sat.mli b/src/th_sat/Th_sat.mli deleted file mode 100644 index 2121adb6..00000000 --- a/src/th_sat/Th_sat.mli +++ /dev/null @@ -1,31 +0,0 @@ - -(** The module defining formulas *) - -(** SAT Formulas - - This modules implements formuals adequate for use in a pure SAT Solver. - Atomic formulas are represented using integers, that should allow - near optimal efficiency (both in terms of space and time). -*) - -open CDCL - -include Theory_intf.S with type formula = int and type proof = unit -(** This modules implements the requirements for implementing an SAT Solver. *) - -val make : t -> int -> formula -(** Make a proposition from an integer. *) - -val fresh : t -> formula -(** Make a fresh atom *) - -val sign : formula -> bool -(** Is the given atom positive ? *) - -val apply_sign : bool -> formula -> formula -(** [apply_sign b] is the identity if [b] is [true], and the negation - function if [b] is [false]. *) - -val set_sign : bool -> formula -> formula -(** Return the atom with the sign set. *) - diff --git a/src/th_sat/jbuild b/src/th_sat/jbuild deleted file mode 100644 index f1b21eb0..00000000 --- a/src/th_sat/jbuild +++ /dev/null @@ -1,13 +0,0 @@ -; vim:ft=lisp: - -(library - ((name Sidekick_th_sat) - (public_name sidekick.th_sat) - (libraries (sidekick.sat cdcl.tseitin)) - (synopsis "sat interface") - (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open CDCL)) - (ocamlopt_flags (:standard -O3 -bin-annot - -unbox-closures -unbox-closures-factor 20)) - )) - -