simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-12 14:00:42 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Some revisions

Browse source
This commit is contained in:
Guillaume Bury 2017-08-31 16:40:14 +02:00
parent 64c170f3a1
commit 1a9f4a554c
3 changed files with 4 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

BIN
poster/poster.pdf
View file

Binary file not shown.

7
poster/poster.tex
View file

@ -45,7 +45,7 @@
\msat{}: a SAT solving library in OCaml. Solves the \textbf{satisfibility} \msat{}: a SAT solving library in OCaml. Solves the \textbf{satisfibility}
of propositional clauses. It is \textbf{Modular}: the user provides of propositional clauses. It is \textbf{Modular}: the user provides
the theory, and produces \textbf{formal proof}. the theory. And it \textbf{produces formal proofs}.
} }
\tblock{Conflict Driven Clause learning} \tblock{Conflict Driven Clause learning}
@ -97,14 +97,13 @@
\tblock{Other solvers} \tblock{Other solvers}
{ {
\\
\begin{center} \begin{center}
\begin{tabular}{c@{\quad}|@{\quad}c@{\quad}|@{\quad}c@{\quad}|@{\quad}c} \begin{tabular}{c@{\quad}|@{\quad}c@{\quad}|@{\quad}c@{\quad}|@{\quad}c}
regstab & SAT & binary only & only pure SAT \\ \hline regstab & SAT & binary only & only pure SAT \\ \hline
\begin{tabular}{c}\textbf{minisat}\\\textbf{sattools}\\ocaml-sat-solvers\end{tabular} & SAT & C bindings & only pure SAT \\ \hline \begin{tabular}{c}\textbf{minisat}\\\textbf{sattools}\\ocaml-sat-solvers\end{tabular} & SAT & C bindings & only pure SAT \\ \hline
Alt-ergo & SMT & binary only & Fixed theory \\ \hline Alt-ergo & SMT & binary only & Fixed theory \\ \hline
\textbf{Alt-ergo-zero} & SMT & OCaml lib & Fixed theory \\ \hline \textbf{Alt-ergo-zero} & SMT & OCaml lib & Fixed theory \\ \hline
\begin{tabular}{c}ocamlyices\\yices2\end{tabular} & SMT & C bindings & Fixed theory \\ \hline \begin{tabular}{c}ocamlyices\\yices2\end{tabular} & SMT & C bindings & Fixed theory \\
\end{tabular} \end{tabular}
\end{center} \end{center}
} }
@ -158,7 +157,7 @@
pigeon/hole7 & 4.257 & 0.213 & 0.015 & 0.073 \\ \hline pigeon/hole7 & 4.257 & 0.213 & 0.015 & 0.073 \\ \hline
pigeon/hole8 & 31.450 & 0.941 & 0.096 & 2.488 \\ \hline pigeon/hole8 & 31.450 & 0.941 & 0.096 & 2.488 \\ \hline
pigeon/hole9 & \begin{tabular}{c}timeout\\(600)\end{tabular} & 8.886 & 0.634 & 4.075 \\ \hline pigeon/hole9 & \begin{tabular}{c}timeout\\(600)\end{tabular} & 8.886 & 0.634 & 4.075 \\ \hline
pigeon/hole10 & \begin{tabular}{c}timeout\\(600)\end{tabular} & 161.478 & \begin{tabular}{c}9.579 (minisat)\\160.376 (sattools)\end{tabular} & 72.050 \\ \hline pigeon/hole10 & \begin{tabular}{c}timeout\\(600)\end{tabular} & 161.478 & \begin{tabular}{c}9.579 (minisat)\\160.376 (sattools)\end{tabular} & 72.050 \\
\end{tabular} \end{tabular}
} }

2
poster/solver_intf.ml
View file

@ -1,4 +1,4 @@
module Make(Th: Theory_intf)() : sig module Make(Th: Theory_intf.S)() : sig
type 'f sat_state = { eval : 'f -> bool; ... } type 'f sat_state = { eval : 'f -> bool; ... }
type ('c,'p) unsat_state = type ('c,'p) unsat_state =
{ conflict: unit -> 'c; proof : unit -> 'p } { conflict: unit -> 'c; proof : unit -> 'p }