Commit 1f508a49 authored by pa's avatar pa

Commit #0 : bootstrap

parents
include GNUmakefile.conf
#################
# General #
#################
.PHONY: default
default: build
.PHONY: all
all: build sujet/sujet.pdf rapport/rapport.pdf
.PHONY: build
build:
dune build --profile release
dpll: build
ln -s _build/install/default/bin/dpll dpll || true
.PHONY: doc
doc:
dune build @doc
.PHONY: clean
clean:
dune clean
cd sujet && rubber --clean --pdf sujet
cd rapport && rubber --clean --pdf rapport
@rm -rf $(FIRSTNAME)_$(LASTNAME).tar.gz
TIMEOUT=30
SUDOKUSTART=0
NSUDOKU=10
#################
# Sujet #
#################
sujet/sujet.pdf : sujet/sujet.tex
cd sujet && rubber --shell-escape -f --pdf sujet.tex
sujet.pdf: sujet/sujet.pdf
ln -s sujet/sujet.pdf sujet.pdf || true
#################
# Rapport #
#################
rapport/rapport.pdf : rapport/rapport.tex
cd rapport && rubber --shell-escape -f --pdf rapport.tex
rapport.pdf: rapport/rapport.pdf
ln -s rapport/rapport.pdf rapport.pdf || true
#################
# DPLL #
#################
.PHONY: tests
tests: build dpll
./tests/run.sh $(TIMEOUT)
#################
# Sudoku #
#################
.PHONY: sudoku
sudoku: build dpll
./sudoku/run.sh $(TIMEOUT) $(SUDOKUSTART) $(NSUDOKU)
#################
# archive #
#################
SRC=$(wildcard src/*.ml src/*.mli)
MISC=GNUmakefile GNUmakefile.conf
TESTS=tests/run.sh
.PHONY: archive
archive: build rapport/rapport.pdf
tar cvzf $(FIRSTNAME)_$(LASTNAME).tar.gz $(SRC) $(MISC) $(TESTS) rapport/rapport.pdf
#################
# bootstrap #
#################
# Use to generate the bootstrap archive
BOOTSTRAP=bootstrap
BDIRS=src tests sudoku sujet rapport
BMISC=GNUmakefile GNUmakefile.conf dune dune-project dpll.install dpll.opam
.PHONY: bootstrap
$(BOOTSTRAP).tar.gz: build sujet/sujet.pdf rapport/rapport.pdf
@export GLOBIGNORE='*~'
@mkdir -p $(BOOTSTRAP)
@rsync -rv --exclude="*~" --exclude="\#*" $(BDIRS) $(BMISC) $(BOOTSTRAP)
@mv $(BOOTSTRAP)/src/dpll-bootstrap.ml $(BOOTSTRAP)/src/dpll.ml
@mv $(BOOTSTRAP)/src/sudoku-bootstrap.ml $(BOOTSTRAP)/src/sudoku.ml
@tar cvzf $(BOOTSTRAP).tar.gz bootstrap/*
@rm -rf $(BOOTSTRAP)
FIRSTNAME=foo
LASTNAME=bar
\ No newline at end of file
lib: [
"_build/install/default/lib/dpll/META" {"META"}
"_build/install/default/lib/dpll/opam" {"opam"}
]
bin: [
"_build/install/default/bin/dpll" {"dpll"}
]
synopsis: "A naive implementation of DPLL algorithm"
description:
"""
An implementation of DPLL algorithm, a homework for the \"Logic Project\" class (Bachelor degree at the ENS Paris-Saclay).
"""
opam-version: "0.1"
maintainer: "francois.thire@lsv.fr"
homepage: "http://www.lsv.fr/~fthire/teaching/2018-2019/projet-logique/index.php"
dev-repo: "http://www.lsv.fr/~fthire/teaching/2018-2019/projet-logique/index.php"
authors: [ "Student" ]
license: "CeCILL"
depends: [
"ocaml" { >= "4.04.0" }
]
build: [ [ "dune" "build" "-p" name "-j" jobs ] ]
(env
(dev (flags :standard))
(release (flags :standard)))
\ No newline at end of file
(lang dune 1.2)
(using menhir 2.0)
\relax
\@writefile{toc}{\contentsline {section}{\numberline {1}Foo}{1}\protected@file@percent }
This is pdfTeX, Version 3.14159265-2.6-1.40.19 (TeX Live 2018) (preloaded format=pdflatex 2019.2.19) 15 APR 2019 09:59
entering extended mode
\write18 enabled.
%&-line parsing enabled.
**\nonstopmode \input{rapport.tex}
(./rapport.tex (/usr/local/texlive/2018/texmf-dist/tex/latex/base/article.cls
Document Class: article 2018/09/03 v1.4i Standard LaTeX document class
(/usr/local/texlive/2018/texmf-dist/tex/latex/base/size10.clo
File: size10.clo 2018/09/03 v1.4i Standard LaTeX file (size option)
)
\c@part=\count80
\c@section=\count81
\c@subsection=\count82
\c@subsubsection=\count83
\c@paragraph=\count84
\c@subparagraph=\count85
\c@figure=\count86
\c@table=\count87
\abovecaptionskip=\skip41
\belowcaptionskip=\skip42
\bibindent=\dimen102
)
(/usr/local/texlive/2018/texmf-dist/tex/latex/base/inputenc.sty
Package: inputenc 2018/08/11 v1.3c Input encoding file
\inpenc@prehook=\toks14
\inpenc@posthook=\toks15
) (./rapport.aux)
\openout1 = `rapport.aux'.
LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 9.
LaTeX Font Info: ... okay on input line 9.
LaTeX Font Info: Checking defaults for T1/cmr/m/n on input line 9.
LaTeX Font Info: ... okay on input line 9.
LaTeX Font Info: Checking defaults for OT1/cmr/m/n on input line 9.
LaTeX Font Info: ... okay on input line 9.
LaTeX Font Info: Checking defaults for OMS/cmsy/m/n on input line 9.
LaTeX Font Info: ... okay on input line 9.
LaTeX Font Info: Checking defaults for OMX/cmex/m/n on input line 9.
LaTeX Font Info: ... okay on input line 9.
LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 9.
LaTeX Font Info: ... okay on input line 9.
LaTeX Font Info: External font `cmex10' loaded for size
(Font) <12> on input line 10.
LaTeX Font Info: External font `cmex10' loaded for size
(Font) <8> on input line 10.
LaTeX Font Info: External font `cmex10' loaded for size
(Font) <6> on input line 10.
[1
{/usr/local/texlive/2018/texmf-var/fonts/map/pdftex/updmap/pdftex.map}]
(./rapport.aux) )
Here is how much of TeX's memory you used:
246 strings out of 492616
2817 string characters out of 6128967
59937 words of memory out of 5000000
4230 multiletter control sequences out of 15000+600000
7280 words of font info for 26 fonts, out of 8000000 for 9000
1141 hyphenation exceptions out of 8191
24i,6n,18p,145b,187s stack positions out of 5000i,500n,10000p,200000b,80000s
</usr/local/texlive/2018/texmf-dist/fonts/type1/public/amsfont
s/cm/cmbx12.pfb></usr/local/texlive/2018/texmf-dist/fonts/type1/public/amsfonts
/cm/cmr10.pfb></usr/local/texlive/2018/texmf-dist/fonts/type1/public/amsfonts/c
m/cmr12.pfb></usr/local/texlive/2018/texmf-dist/fonts/type1/public/amsfonts/cm/
cmr17.pfb>
Output written on rapport.pdf (1 page, 38061 bytes).
PDF statistics:
24 PDF objects out of 1000 (max. 8388607)
16 compressed objects within 1 object stream
0 named destinations out of 1000 (max. 500000)
1 words of extra memory for PDF output out of 10000 (max. 10000000)
\documentclass{article}
\usepackage[utf8]{inputenc}
\author{Coucou, c'est moi}
\title{Rapport pour le projet}
\date{\today}
\begin{document}
\maketitle
\section{Foo}
Hello !
\end{document}
\ No newline at end of file
EXCLUDE_QUERY_DIR
B /home/fthire/.opam/4.04.2/lib/menhirLib
B ../_build/default/src/.main.eobjs
S /home/fthire/.opam/4.04.2/lib/menhirLib
S .
FLG -w -40
type var = int
type lit = int
type model = int list
module Clause = Set.Make(struct type t = var let compare = compare end)
module Cnf = Set.Make(struct type t = Clause.t let compare = Clause.compare end)
type t =
{
nb_var : int;
nb_clause : int;
cnf : Cnf.t
}
let neg var = -var
type 'a printer = Format.formatter -> 'a -> unit
let pp_clause : Clause.t printer = fun fmt clause ->
Clause.iter (fun v -> Format.fprintf fmt "%d " v) clause
let pp_cnf : Cnf.t printer = fun fmt cnf ->
Cnf.iter (fun clause -> Format.fprintf fmt "%a0@." pp_clause clause) cnf
let pp : t printer = fun fmt t ->
Format.fprintf fmt "p %d %d@." t.nb_var t.nb_clause;
Format.fprintf fmt "%a@." pp_cnf t.cnf
(** Type of variables in cnf formulas. *)
type var = int
(** We use the same type for litterals except we use negatives values. *)
type lit = int
(** Contains litterals that satisfy a cnf formula as returned by a SAT solver. *)
type model = int list
(** A set of variables *)
module Clause : Set.S with type elt = var
(** A set of clauses *)
module Cnf : Set.S with type elt = Clause.t
(** A cnf problem *)
type t =
{
nb_var : int; (** number of variables *)
nb_clause : int; (** number of clauses *)
cnf : Cnf.t (** the cnf formula *)
}
(** [neg v] returns the opposite litteral *)
val neg : lit -> lit
type 'a printer = Format.formatter -> 'a -> unit
(** [pp_clause fmt cl] prints a clause *)
val pp_clause : Clause.t printer
(** [pp_cnf fmt cnf] prints a cnf *)
val pp_cnf : Cnf.t printer
(** [pp fmt ast] prints an ast (problem) *)
val pp : t printer
module Location =
struct
type t = {
file : string;
start_line : int;
start_column : int;
stop_line : int;
stop_column : int;
}
let mk file start_line start_column stop_line stop_column =
{ file; start_line; start_column; stop_line; stop_column; }
let mk_pos start stop =
let open Lexing in
mk
start.pos_fname
start.pos_lnum (start.pos_cnum - start.pos_bol)
stop.pos_lnum (stop.pos_cnum - stop.pos_bol)
end
module Statement =
struct
type t = Header of int * int | Clause of Cnf.Ast.Clause.t
(** Header of a dimacs file. First argument is the number of variables,
second is the number of clauses. *)
let p_cnf : ?loc:Location.t -> int -> int -> t = fun ?loc:_ n_var n_clause ->
Header(n_var,n_clause)
(** Make a clause from a list of literals. *)
let clause : ?loc:Location.t -> int list -> t = fun ?loc:_ ls ->
Clause (Cnf.Ast.Clause.of_list ls)
end
(** Format transformers (colors). *)
let red fmt = "\027[31m" ^^ fmt ^^ "\027[0m%!"
let gre fmt = "\027[32m" ^^ fmt ^^ "\027[0m%!"
let yel fmt = "\027[33m" ^^ fmt ^^ "\027[0m%!"
let blu fmt = "\027[34m" ^^ fmt ^^ "\027[0m%!"
let mag fmt = "\027[35m" ^^ fmt ^^ "\027[0m%!"
let cya fmt = "\027[36m" ^^ fmt ^^ "\027[0m%!"
(** Type of logging function data. *)
type logger_data =
{ logger_key : char (** Character used to unable the logger. *)
; logger_name : string (** 4 character name used as prefix in logs. *)
; logger_desc : string (** Description of the log displayed in help. *)
; logger_enabled : bool ref (** Is the log enabled? *) }
(** [log_enabled] is set to true when logging functions may print messages. *)
let log_enabled : bool ref = ref false
(** [loggers] constains the registered logging functions. *)
let loggers : logger_data list ref = ref []
(** [log_summary ()] returns descriptions for logging options. *)
let log_summary : unit -> string list = fun () ->
let fn data = Format.sprintf "%c : %s" data.logger_key data.logger_desc in
List.sort String.compare (List.map fn !loggers)
(** [set_log value key] enables or disables the loggers corresponding to every
character of [str] according to [value]. *)
let set_debug : bool -> string -> unit = fun value str ->
let fn {logger_key; logger_enabled; _} =
if String.contains str logger_key then logger_enabled := value
in
List.iter fn !loggers;
let is_enabled data = !(data.logger_enabled) in
log_enabled := List.exists is_enabled Pervasives.(!loggers)
(** Exception raised in case of failure. *)
exception Fatal of Location.pos option * string
(** Short name for a standard formatter with continuation. *)
type ('a,'b) koutfmt = ('a, Format.formatter, unit, unit, unit, 'b) format6
let fatal : Location.pos option -> ('a,'b) koutfmt -> 'a = fun pos fmt ->
let cont _ = raise (Fatal(pos, Format.flush_str_formatter ())) in
Format.kfprintf cont Format.str_formatter fmt
(** [exit_with fmt] is similar to [fatal_no_pos fmt], but the whole program is
(irrecoverably) stopped with return code [1], indicating failure. *)
let exit_with : ('a,'b) koutfmt -> 'a = fun fmt ->
Format.kfprintf (fun _ -> exit 1) Format.err_formatter (red (fmt ^^ "\n%!"))
let parse_lexbuf : string -> Lexing.lexbuf -> Ast.t = fun fname lexbuf ->
LexerDimacs.filename := fname;
try
ParserDimacs.file LexerDimacs.token lexbuf
with
| ParserDimacs.Error ->
let loc = Lexing.(lexbuf.lex_start_p) in
let loc = Some(LexerDimacs.locate loc loc) in
Console.fatal loc "Unexpected token [%s]." (Lexing.lexeme lexbuf)
let parse_file : string -> Ast.t = fun fname ->
let ic = open_in fname in
let lexbuf = Lexing.from_channel ic in
try let l = parse_lexbuf fname lexbuf in close_in ic; l
with e -> close_in ic; raise e
module type CHOICE = sig
val choice : Ast.Cnf.t -> Ast.var
end
module DefaultChoice =
struct
let choice : Ast.Cnf.t -> Ast.var = fun cnf -> failwith "todo: choice"
end
module type SOLVER = sig
val solve : Ast.t -> Ast.model option
end
module DPLL(C:CHOICE) : SOLVER =
struct
let solve : Ast.t -> Ast.model option = fun p -> failwith "todo: solve"
end
(** Signature module to choose a variable on which the DPLL algorithm will branch. *)
module type CHOICE = sig
val choice : Ast.Cnf.t -> Ast.var
end
(** Signature for a SAT solver. *)
module type SOLVER = sig
(** solve takes a cnf formula and returns either None if it is unsatisfiable or
a model that satisfies the formula. *)
val solve : Ast.t -> Ast.model option
end
(** DPLL is a SAT solver parameterized by a choice function. *)
module DPLL(C:CHOICE) : SOLVER
(** Implement a choice by Default. More choices can be implemented. *)
module DefaultChoice : CHOICE
(ocamllex (modules lexerDimacs))
(menhir
(flags (--explain --table --external-tokens TokensDimacs tokensDimacs.mly))
(modules parserDimacs)
)
(menhir
(flags (--only-tokens))
(modules tokensDimacs)
)
(executable
(name main)
(public_name dpll)
(libraries menhirLib)
(package dpll))
{
open TokensDimacs
let filename = ref ""
let locate : Lexing.position -> Lexing.position -> Location.pos = fun p1 p2 ->
let open Location in
let fname = if !filename = "" then None else Some(!filename) in
let start_line = p1.pos_lnum in
let start_col = p1.pos_cnum - p1.pos_bol in
let end_line = p2.pos_lnum in
let end_col = p2.pos_cnum - p2.pos_bol in
Lazy.from_val {fname; start_line; start_col; end_line; end_col}
let locate_lexbuf : Lexing.lexbuf -> Location.pos = fun lexbuf ->
locate lexbuf.lex_start_p lexbuf.lex_curr_p
let unexpected_char : Lexing.lexbuf -> char -> token = fun lexbuf c ->
Console.fatal (Some(locate_lexbuf lexbuf)) "Unexpected characters [%c]." c
}
let zero_numeric = '0'
let numeric = ['0' - '9']
let non_zero_numeric = ['1' - '9']
let positive_number = non_zero_numeric numeric*
let negative_number = ['-'] positive_number
let number = positive_number | negative_number
let printable_char = [^ '\n']
let comment = ['c'] printable_char* ['\n']
rule token = parse
| "c" { comment lexbuf }
| "p" { P }
| "cnf" { CNF }
| eof { EOF }
| zero_numeric { ZERO }
| [' ' '\t' '\r'] { token lexbuf }
| number { INT (int_of_string @@ Lexing.lexeme lexbuf) }
| '\n' { Lexing.new_line lexbuf; NEWLINE }
| _ as c { unexpected_char lexbuf c }
and comment = parse
| '\n' { Lexing.new_line lexbuf; token lexbuf }
| printable_char { comment lexbuf }
\ No newline at end of file
type pos = pos_data Lazy.t
and pos_data =
{ fname : string option (** File name for the position. *)
; start_line : int (** Line number of the starting point. *)
; start_col : int (** Column number (utf8) of the starting point. *)
; end_line : int (** Line number of the ending point. *)
; end_col : int (** Column number (utf8) of the ending point. *) }
(** [to_string pos] transforms [pos] into a readable string. *)
let to_string : pos -> string = fun p ->
let {fname; start_line; start_col; end_line; end_col} = Lazy.force p in
let fname =
match fname with
| None -> ""
| Some(n) -> n ^ ", "
in
if start_line <> end_line then
Printf.sprintf "%s%d:%d-%d:%d" fname start_line start_col end_line end_col
else if start_col = end_col then
Printf.sprintf "%s%d:%d" fname start_line start_col
else
Printf.sprintf "%s%d:%d-%d" fname start_line start_col end_col
(** [print oc pos] prints the optional position [pos] to [oc]. *)
let print : Format.formatter -> pos -> unit = fun ch p ->
Format.pp_print_string ch (to_string p)
type execution_mode =
| Cnf (** Solve a formula *)
| Sudoku of string (** Solve a sudoku given as a string *)
(** By default we solve a formula given in the dimacs format *)
let mode = ref Cnf
(** Default solver. By doing the third part of the project, you might come with other solvers *)
module S = Dpll.DPLL(Dpll.DefaultChoice)
(** Handle files given on the command line *)
let handle_file : string -> unit = fun fname ->
let p = Dimacs.parse_file fname in
begin
match S.solve p with
| None -> Format.printf "false@."
| Some _ -> Format.printf "true@."
end
let handle_sudoku : string -> unit = fun str ->
let sudoku, solution = Sudoku.read str in
let env, ast = Sudoku.to_cnf sudoku in
match S.solve ast with
| None ->
raise @@ failwith "No answer. Probably your encoding is incorrect"
| Some model ->
let candidate = Sudoku.solution_of env model in
if candidate <> solution then
raise @@ failwith "You found an incorrect answer."
(** Specification of the options handle by the program. You are only allowed to ADD new options *)
let spec =
let debug_flags =
let fn acc l = acc ^ "\n " ^ l in
List.fold_left fn "\n Available flags:" (Console.log_summary ())
in
let spec = Arg.align
[ ( "--debug"
, Arg.String (Console.set_debug true)
, "<flags> Sets the given debugging flags" ^ debug_flags )
; ( "--sudoku"
, Arg.String (fun s -> mode := Sudoku s)
, " Solve a sudoku given on the command line as a string" )]
in
spec
(** Entry point of the program *)
let _ =
let open Console in
let usage = Format.sprintf "Usage: %s [CMD] [FILE]" Sys.argv.(0) in
let files = ref [] in
Arg.parse spec (fun s -> files := s :: !files) usage;
try
begin
match !mode with
| Cnf -> List.iter handle_file !files
| Sudoku str -> handle_sudoku str
end
with
| Fatal(None, msg) -> exit_with "%s" msg
| Fatal(Some(p), msg) -> exit_with "[%a] %s" Location.print p msg
%{
let mk_clause : int list -> Ast.Clause.t = fun ls -> Ast.Clause.of_list ls