diff --git a/SPE/OPT/TP 2/.kile/réponseauxquestions.kilepr.gui b/SPE/OPT/TP 2/.kile/réponseauxquestions.kilepr.gui new file mode 100644 index 0000000..6b4fa19 --- /dev/null +++ b/SPE/OPT/TP 2/.kile/réponseauxquestions.kilepr.gui @@ -0,0 +1,30 @@ +[General] +kile_livePreviewEnabled=true +kile_livePreviewStatusUserSpecified=false +kile_livePreviewTool=LivePreview-PDFLaTeX +lastDocument=Questions + +[document-settings,item:Questions] +Bookmarks= +Encoding= +Highlighting=LaTeX +Highlighting Set By User=false +Indentation Mode=normal +Mode=LaTeX +Mode Set By User=false + +[item:Questions] +open=true +order=0 + +[item:réponseauxquestions.kilepr] +open=false +order=-1 + +[view-settings,view=0,item:Questions] +CursorColumn=25 +CursorLine=3 +Dynamic Word Wrap=true +JumpList= +TextFolding=[] +ViMarks= diff --git a/SPE/OPT/TP 2/.kile/tp2.kilepr.gui b/SPE/OPT/TP 2/.kile/tp2.kilepr.gui new file mode 100644 index 0000000..953b043 --- /dev/null +++ b/SPE/OPT/TP 2/.kile/tp2.kilepr.gui @@ -0,0 +1,30 @@ +[General] +kile_livePreviewEnabled=true +kile_livePreviewStatusUserSpecified=false +kile_livePreviewTool=LivePreview-PDFLaTeX +lastDocument=Questions.tex + +[document-settings,item:Questions.tex] +Bookmarks= +Encoding= +Highlighting=LaTeX +Highlighting Set By User=false +Indentation Mode=normal +Mode=LaTeX +Mode Set By User=false + +[item:Questions.tex] +open=true +order=0 + +[item:tp2.kilepr] +open=false +order=-1 + +[view-settings,view=0,item:Questions.tex] +CursorColumn=14 +CursorLine=35 +Dynamic Word Wrap=true +JumpList= +TextFolding=[] +ViMarks=.,55,44,[,55,40,],55,44 diff --git a/SPE/OPT/TP 2/Questions.aux b/SPE/OPT/TP 2/Questions.aux new file mode 100644 index 0000000..01200ba --- /dev/null +++ b/SPE/OPT/TP 2/Questions.aux @@ -0,0 +1,3 @@ +\relax +\@writefile{toc}{\contentsline {section}{\numberline {III}Forme normale disjonctive}{1}\protected@file@percent } +\@writefile{toc}{\contentsline {subsection}{\numberline {III.1}Question :}{1}\protected@file@percent } diff --git a/SPE/OPT/TP 2/Questions.log b/SPE/OPT/TP 2/Questions.log new file mode 100644 index 0000000..f8393b7 --- /dev/null +++ b/SPE/OPT/TP 2/Questions.log @@ -0,0 +1,257 @@ +This is pdfTeX, Version 3.14159265-2.6-1.40.21 (TeX Live 2020 Gentoo Linux) (preloaded format=pdflatex 2020.9.3) 12 SEP 2020 10:32 +entering extended mode + restricted \write18 enabled. + %&-line parsing enabled. +**Questions.tex +(./Questions.tex +LaTeX2e <2020-02-02> patch level 5 +L3 programming layer <2020-02-25> +(/usr/share/texmf-dist/tex/latex/base/article.cls +Document Class: article 2019/12/20 v1.4l Standard LaTeX document class +(/usr/share/texmf-dist/tex/latex/base/size10.clo +File: size10.clo 2019/12/20 v1.4l Standard LaTeX file (size option) +) +\c@part=\count167 +\c@section=\count168 +\c@subsection=\count169 +\c@subsubsection=\count170 +\c@paragraph=\count171 +\c@subparagraph=\count172 +\c@figure=\count173 +\c@table=\count174 +\abovecaptionskip=\skip47 +\belowcaptionskip=\skip48 +\bibindent=\dimen134 +) +(/usr/share/texmf-dist/tex/latex/mathtools/mathtools.sty +Package: mathtools 2020/01/17 v1.23 mathematical typesetting tools + +(/usr/share/texmf-dist/tex/latex/graphics/keyval.sty +Package: keyval 2014/10/28 v1.15 key=value parser (DPC) +\KV@toks@=\toks15 +) +(/usr/share/texmf-dist/tex/latex/tools/calc.sty +Package: calc 2017/05/25 v4.3 Infix arithmetic (KKT,FJ) +\calc@Acount=\count175 +\calc@Bcount=\count176 +\calc@Adimen=\dimen135 +\calc@Bdimen=\dimen136 +\calc@Askip=\skip49 +\calc@Bskip=\skip50 +LaTeX Info: Redefining \setlength on input line 80. +LaTeX Info: Redefining \addtolength on input line 81. +\calc@Ccount=\count177 +\calc@Cskip=\skip51 +) +(/usr/share/texmf-dist/tex/latex/mathtools/mhsetup.sty +Package: mhsetup 2017/03/31 v1.3 programming setup (MH) +) +(/usr/share/texmf-dist/tex/latex/amsmath/amsmath.sty +Package: amsmath 2020/01/20 v2.17e AMS math features +\@mathmargin=\skip52 + +For additional information on amsmath, use the `?' option. +(/usr/share/texmf-dist/tex/latex/amsmath/amstext.sty +Package: amstext 2000/06/29 v2.01 AMS text + +(/usr/share/texmf-dist/tex/latex/amsmath/amsgen.sty +File: amsgen.sty 1999/11/30 v2.0 generic functions +\@emptytoks=\toks16 +\ex@=\dimen137 +)) +(/usr/share/texmf-dist/tex/latex/amsmath/amsbsy.sty +Package: amsbsy 1999/11/29 v1.2d Bold Symbols +\pmbraise@=\dimen138 +) +(/usr/share/texmf-dist/tex/latex/amsmath/amsopn.sty +Package: amsopn 2016/03/08 v2.02 operator names +) +\inf@bad=\count178 +LaTeX Info: Redefining \frac on input line 227. +\uproot@=\count179 +\leftroot@=\count180 +LaTeX Info: Redefining \overline on input line 389. +\classnum@=\count181 +\DOTSCASE@=\count182 +LaTeX Info: Redefining \ldots on input line 486. +LaTeX Info: Redefining \dots on input line 489. +LaTeX Info: Redefining \cdots on input line 610. +\Mathstrutbox@=\box45 +\strutbox@=\box46 +\big@size=\dimen139 +LaTeX Font Info: Redeclaring font encoding OML on input line 733. +LaTeX Font Info: Redeclaring font encoding OMS on input line 734. +\macc@depth=\count183 +\c@MaxMatrixCols=\count184 +\dotsspace@=\muskip16 +\c@parentequation=\count185 +\dspbrk@lvl=\count186 +\tag@help=\toks17 +\row@=\count187 +\column@=\count188 +\maxfields@=\count189 +\andhelp@=\toks18 +\eqnshift@=\dimen140 +\alignsep@=\dimen141 +\tagshift@=\dimen142 +\tagwidth@=\dimen143 +\totwidth@=\dimen144 +\lineht@=\dimen145 +\@envbody=\toks19 +\multlinegap=\skip53 +\multlinetaggap=\skip54 +\mathdisplay@stack=\toks20 +LaTeX Info: Redefining \[ on input line 2859. +LaTeX Info: Redefining \] on input line 2860. +) +LaTeX Info: Thecontrolsequence`\('isalreadyrobust on input line 129. +LaTeX Info: Thecontrolsequence`\)'isalreadyrobust on input line 129. +LaTeX Info: Thecontrolsequence`\['isalreadyrobust on input line 129. +LaTeX Info: Thecontrolsequence`\]'isalreadyrobust on input line 129. +\g_MT_multlinerow_int=\count190 +\l_MT_multwidth_dim=\dimen146 +\origjot=\skip55 +\l_MT_shortvdotswithinadjustabove_dim=\dimen147 +\l_MT_shortvdotswithinadjustbelow_dim=\dimen148 +\l_MT_above_intertext_sep=\dimen149 +\l_MT_below_intertext_sep=\dimen150 +\l_MT_above_shortintertext_sep=\dimen151 +\l_MT_below_shortintertext_sep=\dimen152 +) +(/usr/share/texmf-dist/tex/latex/listings/listings.sty +\lst@mode=\count191 +\lst@gtempboxa=\box47 +\lst@token=\toks21 +\lst@length=\count192 +\lst@currlwidth=\dimen153 +\lst@column=\count193 +\lst@pos=\count194 +\lst@lostspace=\dimen154 +\lst@width=\dimen155 +\lst@newlines=\count195 +\lst@lineno=\count196 +\lst@maxwidth=\dimen156 + +(/usr/share/texmf-dist/tex/latex/listings/lstmisc.sty +File: lstmisc.sty 2019/09/10 1.8c (Carsten Heinz) +\c@lstnumber=\count197 +\lst@skipnumbers=\count198 +\lst@framebox=\box48 +) +(/usr/share/texmf-dist/tex/latex/listings/listings.cfg +File: listings.cfg 2019/09/10 1.8c listings configuration +)) +Package: listings 2019/09/10 1.8c (Carsten Heinz) + +(/usr/share/texmf-dist/tex/latex/graphics/color.sty +Package: color 2019/11/23 v1.2a Standard LaTeX Color (DPC) + +(/usr/share/texmf-dist/tex/latex/graphics-cfg/color.cfg +File: color.cfg 2016/01/02 v1.6 sample color configuration +) +Package color Info: Driver file: pdftex.def on input line 147. + +(/usr/share/texmf-dist/tex/latex/graphics-def/pdftex.def +File: pdftex.def 2018/01/08 v1.0l Graphics/color driver for pdftex +)) +(/usr/share/texmf-dist/tex/latex/base/inputenc.sty +Package: inputenc 2018/08/11 v1.3c Input encoding file +\inpenc@prehook=\toks22 +\inpenc@posthook=\toks23 +) +(/usr/share/texmf-dist/tex/latex/listings/lstlang1.sty +File: lstlang1.sty 2019/09/10 1.8c listings language file +) +(/usr/share/texmf-dist/tex/latex/listings/lstlang2.sty +File: lstlang2.sty 2019/09/10 1.8c listings language file +) +(/usr/share/texmf-dist/tex/latex/listings/lstmisc.sty +File: lstmisc.sty 2019/09/10 1.8c (Carsten Heinz) +) +(/usr/share/texmf-dist/tex/latex/l3backend/l3backend-pdfmode.def +File: l3backend-pdfmode.def 2020-02-23 L3 backend support: PDF mode +\l__kernel_color_stack_int=\count199 +\l__pdf_internal_box=\box49 +) +No file Questions.aux. +\openout1 = `Questions.aux'. + +LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 44. +LaTeX Font Info: ... okay on input line 44. +LaTeX Font Info: Checking defaults for OMS/cmsy/m/n on input line 44. +LaTeX Font Info: ... okay on input line 44. +LaTeX Font Info: Checking defaults for OT1/cmr/m/n on input line 44. +LaTeX Font Info: ... okay on input line 44. +LaTeX Font Info: Checking defaults for T1/cmr/m/n on input line 44. +LaTeX Font Info: ... okay on input line 44. +LaTeX Font Info: Checking defaults for TS1/cmr/m/n on input line 44. +LaTeX Font Info: ... okay on input line 44. +LaTeX Font Info: Checking defaults for OMX/cmex/m/n on input line 44. +LaTeX Font Info: ... okay on input line 44. +LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 44. +LaTeX Font Info: ... okay on input line 44. +(/usr/share/texmf-dist/tex/latex/graphics/graphicx.sty +Package: graphicx 2019/11/30 v1.2a Enhanced LaTeX Graphics (DPC,SPQR) + +(/usr/share/texmf-dist/tex/latex/graphics/graphics.sty +Package: graphics 2019/11/30 v1.4a Standard LaTeX Graphics (DPC,SPQR) + +(/usr/share/texmf-dist/tex/latex/graphics/trig.sty +Package: trig 2016/01/03 v1.10 sin cos tan (DPC) +) +(/usr/share/texmf-dist/tex/latex/graphics-cfg/graphics.cfg +File: graphics.cfg 2016/06/04 v1.11 sample graphics configuration +) +Package graphics Info: Driver file: pdftex.def on input line 105. +) +\Gin@req@height=\dimen157 +\Gin@req@width=\dimen158 +) +\c@lstlisting=\count266 + +(/usr/share/texmf-dist/tex/context/base/mkii/supp-pdf.mkii +[Loading MPS to PDF converter (version 2006.09.02).] +\scratchcounter=\count267 +\scratchdimen=\dimen159 +\scratchbox=\box50 +\nofMPsegments=\count268 +\nofMParguments=\count269 +\everyMPshowfont=\toks24 +\MPscratchCnt=\count270 +\MPscratchDim=\dimen160 +\MPnumerator=\count271 +\makeMPintoPDFobject=\count272 +\everyMPtoPDFconversion=\toks25 +) (/usr/share/texmf-dist/tex/latex/epstopdf-pkg/epstopdf-base.sty +Package: epstopdf-base 2020-01-24 v2.11 Base part for package epstopdf +Package epstopdf-base Info: Redefining graphics rule for `.eps' on input line 4 +85. + +(/usr/share/texmf-dist/tex/latex/latexconfig/epstopdf-sys.cfg +File: epstopdf-sys.cfg 2010/07/13 v1.3 Configuration of (r)epstopdf for TeX Liv +e +)) [1 + +{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}] (./Questions.aux) ) +Here is how much of TeX's memory you used: + 4110 strings out of 482906 + 56889 string characters out of 5959892 + 481182 words of memory out of 5000000 + 19362 multiletter control sequences out of 15000+600000 + 537879 words of font info for 44 fonts, out of 8000000 for 9000 + 14 hyphenation exceptions out of 8191 + 37i,5n,51p,242b,1155s stack positions out of 5000i,500n,10000p,200000b,80000s + +Output written on Questions.pdf (1 page, 67274 bytes). +PDF statistics: + 36 PDF objects out of 1000 (max. 8388607) + 25 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) + diff --git a/SPE/OPT/TP 2/Questions.pdf b/SPE/OPT/TP 2/Questions.pdf new file mode 100644 index 0000000..709905b Binary files /dev/null and b/SPE/OPT/TP 2/Questions.pdf differ diff --git a/SPE/OPT/TP 2/Questions.synctex.gz b/SPE/OPT/TP 2/Questions.synctex.gz new file mode 100644 index 0000000..11361bb Binary files /dev/null and b/SPE/OPT/TP 2/Questions.synctex.gz differ diff --git a/SPE/OPT/TP 2/Questions.tex b/SPE/OPT/TP 2/Questions.tex new file mode 100644 index 0000000..81d6076 --- /dev/null +++ b/SPE/OPT/TP 2/Questions.tex @@ -0,0 +1,59 @@ +\documentclass[a4paper,10pt]{article} +%\documentclass[a4paper,10pt]{scrartcl} + +\usepackage{mathtools} + +\usepackage{listings} +\usepackage{color} +\usepackage[utf8]{inputenc} +\definecolor{dkgreen}{rgb}{0,0.6,0} +\definecolor{gray}{rgb}{0.5,0.5,0.5} +\definecolor{mauve}{rgb}{0.58,0,0.82} +\lstset{frame=tb, + language=caml, + aboveskip=3mm, + belowskip=3mm, + showstringspaces=false, + columns=flexible, + basicstyle={\small\ttfamily}, + numbers=none, + numberstyle=\tiny\color{gray}, + keywordstyle=\color{blue}, + commentstyle=\color{dkgreen}, + stringstyle=\color{mauve}, + breaklines=true, + breakatwhitespace=true, + tabsize=3 +} +\renewcommand{\thesection}{\Roman{section}} +\newcommand{\sectioni}[2]{\setcounter{section}{#1}\addtocounter{section}{-1}\section{#2}} +\newcommand{\subsectioni}[2]{\setcounter{subsection}{#1}\addtocounter{subsection}{-1}\subsection{#2}} +\title{Questions du TP2} +\author{} +\date{} + +\pdfinfo{% + /Title () + /Author () + /Creator () + /Producer () + /Subject () + /Keywords () +} + +\begin{document} + \maketitle + \sectioni{3}{Forme normale disjonctive} + \subsectioni{1}{Question :} + On se sert du code écrit aux questions précédentes, + \begin{lstlisting} +# table_de_verite 3 g;; +- : bool array = [|true; false; true; false; true; false; false; true|] + \end{lstlisting} + $\mathcal{G} = + (\neg V_2 \wedge \neg V_1 \wedge \neg V_0) \vee + (\neg V_2 \wedge V_1 \wedge \neg V_0) \vee + (V_2 \wedge \neg V_1 \wedge \neg V_0) \vee + (V_2 \wedge V_1 \wedge V_0) + $ +\end{document} diff --git a/SPE/OPT/TP 2/main.ml b/SPE/OPT/TP 2/main.ml index d71ea85..b55a0be 100644 --- a/SPE/OPT/TP 2/main.ml +++ b/SPE/OPT/TP 2/main.ml @@ -19,15 +19,20 @@ let rec evaluer_tab t form = match form with | Or (h::tail) -> (evaluer_tab t h) || (evaluer_tab t (Or tail));; 5 lsr 1;; -let evaluer n c f = +let contexte_from_int n c = let contexte = Array.make n false in let j = ref c in for i = 0 to n-1 do - contexte.(i) <- !j mod 2 = 0; + contexte.(i) <- !j mod 2 <> 0; j := !j lsr 1 done; + contexte;; + +let evaluer n c f = + let contexte = contexte_from_int n c in evaluer_tab contexte f;; -evaluer 3 0 f;; + +evaluer 3 3 g;; let table_de_verite n f = let rec puis n a = match n with @@ -40,3 +45,23 @@ let table_de_verite n f = res;; table_de_verite 3 g;; +let forme_normale_disjonctive n f = + let rec puis n a = match n with + | 0 -> 1 + | _ -> a * (puis (n-1) a) in + + let rec disjonction c conjs = + + let rec conjonction cont conj n = match n with + | -1 -> And conj + | _ -> conjonction cont ((if cont.(n) then (Var n) else Not (Var n))::conj) (n-1) in + + match c with + | -1 -> Or conjs + | _ -> let contexte = context_from_int n c in + if evaluer_tab contexte f then + disjonction (c-1) ((conjonction contexte [] (n-1))::conjs) + else + disjonction (c-1) conjs in + disjonction ((puis n 2) -1) [];; +forme_normale_disjonctive 3 g;; \ No newline at end of file diff --git a/SPE/OPT/TP 2/tp2.kilepr b/SPE/OPT/TP 2/tp2.kilepr new file mode 100644 index 0000000..e7c8f30 --- /dev/null +++ b/SPE/OPT/TP 2/tp2.kilepr @@ -0,0 +1,31 @@ +[General] +bib_extensions=.bib +bibliographyBackendAutoDetected= +bibliographyBackendUserOverride= +def_graphic_ext=eps +img_extIsRegExp=false +img_extensions=.eps .jpg .jpeg .png .pdf .ps .fig .gif +kileprversion=3 +kileversion=2.9.93 +masterDocument= +name=TP2 +pkg_extIsRegExp=false +pkg_extensions=.cls .sty .bbx .cbx .lbx +src_extIsRegExp=false +src_extensions=.tex .ltx .latex .dtx .ins + +[Tools] +MakeIndex= +QuickBuild= + +[item:Questions.tex] +archive=true +encoding= +highlight=LaTeX +mode=LaTeX + +[item:tp2.kilepr] +archive=true +encoding= +highlight= +mode=