\begin{slide}{SMT-\{LIB,COMP\}}

  \begin{itemize}\itemsep 0pt \parskip 2pt
  \item 
    Standard-Modellierungssprache, Syntax/Semantik-Def:

    \url{http://smtlib.cs.uiowa.edu/standard.shtml}    
  \item 
    Aufgabensammlung: \url{http://smtlib.cs.uiowa.edu/benchmarks.shtml}

    Modelle aus Kombinatorik, Scheduling, Hard- und Software-Verifikation, \dots
    
    Herkunft: crafted, industrial, (random)
  \item
    Wettbewerb: \url{http://www.smtcomp.org/}
  \item 
    typische Solver:
    \begin{itemize}
    \item Z3 
      {\small \url{http://z3.codeplex.com/}} (Microsoft Research)
    \item Yices {\small \url{http://yices.csl.sri.com/}} (SRI, ehem. Stanford Research Inst.)
    \end{itemize}
  \end{itemize}

\end{slide}

\begin{slide}{Beispiel \texttt{queen10-1.smt2} aus SMT-LIB}
\begin{small}
\begin{verbatim}
(set-logic QF_IDL) (declare-fun x0 () Int)
(declare-fun x1 () Int) (declare-fun x2 () Int)
(declare-fun x3 () Int) (declare-fun x4 () Int)
(assert (let ((?v_0 (- x0 x4)) (?v_1 (- x1 x4))
(?v_2 (- x2 x4)) (?v_3 (- x3 x4)) (?v_4 (- x0 x1))
(?v_5 (- x0 x2)) (?v_6 (- x0 x3)) (?v_7 (- x1 x2))
(?v_8 (- x1 x3)) (?v_9 (- x2 x3))) (and (<= ?v_0 3)
(>= ?v_0 0) (<= ?v_1 3) (>= ?v_1 0) (<= ?v_2 3) (>=
?v_2 0) (<= ?v_3 3) (>= ?v_3 0) (not (= x0 x1))
(not (= x0 x2)) (not (= x0 x3)) (not (= x1 x2))
(not (= x1 x3)) (not (= x2 x3)) (not (= ?v_4 1))
(not (= ?v_4 (- 1))) (not (= ?v_5 2)) (not (= ?v_5
(- 2))) (not (= ?v_6 3)) (not (= ?v_6 (- 3))) (not
(= ?v_7 1)) (not (= ?v_7 (- 1))) (not (= ?v_8 2))
(not (= ?v_8 (- 2))) (not (= ?v_9 1)) (not (= ?v_9
(- 1)))))) (check-sat) (exit)
\end{verbatim}
\end{small}

\end{slide}

\begin{slide}{Umfang der Benchmarks (2014)}
{\small \url{http://www.cs.nyu.edu/~barrett/smtlib/?C=S;O=D}}
\begin{small}
\begin{verbatim}
QF_BV_DisjunctiveScheduling.zip           2.7G  
QF_IDL_DisjunctiveScheduling.zip          2.4G  
incremental_Hierarchy.zip                 2.1G  
QF_BV_except_DisjunctiveScheduling.zip    1.6G  
QF_IDL_except_DisjunctiveScheduling.zip   417M  
QF_LIA_Hierarchy.zip                      294M  
QF_UFLRA_Hierarchy.zip                    217M  
QF_NRA_Hierarchy.zip                      170M  
QF_LRA_Hierarchy.zip                      160M  
\end{verbatim}
\end{small}
\begin{itemize}
\item QF: quantifier free, 
\item I: integer, R: real, BV: bitvector
\item D: difference, L: linear, N: polynomial
\end{itemize}



\end{slide}
