mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-06 03:05:31 -05:00
cleanup of unused sublibrary
This commit is contained in:
Simon Cruanes
parent
4628bff514
commit
70749155bf
6 changed files with 4 additions and 163 deletions
11
Makefile
11
Makefile
|
|
@ -3,20 +3,17 @@
|
||||||
|
|
||||||
.PHONY: clean build build-dev
|
.PHONY: clean build build-dev
|
||||||
|
|
||||||
NAME=msat
|
|
||||||
J?=3
|
J?=3
|
||||||
TIMEOUT?=30
|
TIMEOUT?=30
|
||||||
TARGETS=src/main/main.exe
|
|
||||||
OPTS= -j $(J)
|
OPTS= -j $(J)
|
||||||
|
|
||||||
build:
|
|
||||||
jbuilder build $(TARGETS) $(OPTS)
|
|
||||||
|
|
||||||
build-install:
|
build-install:
|
||||||
jbuilder build @install
|
jbuilder build $(OPTS) @install
|
||||||
|
|
||||||
|
build: build-install
|
||||||
|
|
||||||
build-dev:
|
build-dev:
|
||||||
jbuilder build $(TARGETS) $(OPTS) --dev
|
jbuilder build $(OPTS) --dev
|
||||||
|
|
||||||
enable_log:
|
enable_log:
|
||||||
cd src/core; ln -sf log_real.ml log.ml
|
cd src/core; ln -sf log_real.ml log.ml
|
||||||
|
|
|
||||||
|
|
@ -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)
|
|
||||||
|
|
||||||
|
|
@ -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. *)
|
|
||||||
|
|
||||||
|
|
@ -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
|
|
||||||
|
|
@ -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. *)
|
|
||||||
|
|
||||||
|
|
@ -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))
|
|
||||||
))
|
|
||||||
|
|
||||||
|
|
||||||
Loading…
Add table
Reference in a new issue