28 lines
4.2 KiB
Plaintext
28 lines
4.2 KiB
Plaintext
\begin{Verbatim}[commandchars=\\\{\},numbers=left,firstnumber=1,stepnumber=1,codes={\catcode`\$=3\catcode`\^=7\catcode`\_=8\relax},xleftmargin=5mm]
|
|
\PY{k}{predicate}\PY{l+s}{ }\PY{n+nf}{lex\PYZus{}minimize}\PY{p}{(}\PY{k+kt}{array}\PY{p}{[}\PY{k+kt}{int}\PY{p}{]}\PY{l+s}{ }\PY{k+kt}{of}\PY{l+s}{ }\PY{k+kt}{var}\PY{l+s}{ }\PY{k+kt}{int}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{o}\PY{p}{)}\PY{l+s}{ }\PY{o}{=}
|
|
\PY{l+s}{ }\PY{l+s}{ }\PY{k}{let}\PY{l+s}{ }\PY{p}{\PYZob{}}
|
|
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k+kt}{var}\PY{l+s}{ }\PY{n+nb}{index\PYZus{}set}\PY{p}{(}\PY{n+nv}{o}\PY{p}{)}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{stage}
|
|
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k+kt}{array}\PY{p}{[}\PY{n+nb}{index\PYZus{}set}\PY{p}{(}\PY{n+nv}{o}\PY{p}{)}\PY{p}{]}\PY{l+s}{ }\PY{k+kt}{of}\PY{l+s}{ }\PY{k+kt}{var}\PY{l+s}{ }\PY{k+kt}{int}\PY{p}{:}\PY{l+s}{ }\PY{n+nv}{best}\PY{p}{;}
|
|
\PY{l+s}{ }\PY{l+s}{ }\PY{p}{\PYZcb{}}\PY{l+s}{ }\PY{o}{in}\PY{l+s}{ }\PY{k}{if}\PY{l+s}{ }\PY{n+nf}{status}\PY{p}{(}\PY{p}{)}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nv}{START}\PY{l+s}{ }\PY{k}{then}
|
|
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{n+nv}{stage}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nb}{min}\PY{p}{(}\PY{n+nb}{index\PYZus{}set}\PY{p}{(}\PY{n+nv}{o}\PY{p}{)}\PY{p}{)}
|
|
\PY{l+s}{ }\PY{l+s}{ }\PY{k}{else}
|
|
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k}{if}\PY{l+s}{ }\PY{n+nf}{status}\PY{p}{(}\PY{p}{)}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nv}{UNSAT}\PY{l+s}{ }\PY{k}{then}
|
|
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k}{if}\PY{l+s}{ }\PY{n+nf}{lastval}\PY{p}{(}\PY{n+nv}{stage}\PY{p}{)}\PY{l+s}{ }\PY{o}{\PYZlt{}}\PY{l+s}{ }\PY{n+nv}{l}\PY{l+s}{ }\PY{k}{then}
|
|
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{n+nv}{stage}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nf}{lastval}\PY{p}{(}\PY{n+nv}{stage}\PY{p}{)}\PY{l+s}{ }\PY{o}{+}\PY{l+s}{ }\PY{l+m}{1}
|
|
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k}{else}
|
|
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{n+nf}{complete}\PY{p}{(}\PY{p}{)}\PY{l+s}{ }\PY{l+s}{ }\PY{c}{\PYZpc{} we are finished}
|
|
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k}{endif}
|
|
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k}{else}
|
|
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{n+nv}{stage}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nf}{lastval}\PY{p}{(}\PY{n+nv}{stage}\PY{p}{)}
|
|
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{o}{/\PYZbs{}}\PY{l+s}{ }\PY{n+nv}{best}\PY{p}{[}\PY{n+nv}{stage}\PY{p}{]}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nf}{sol}\PY{p}{(}\PY{l+s}{\PYZus{}}\PY{l+s}{o}\PY{l+s}{b}\PY{l+s}{j}\PY{l+s}{e}\PY{l+s}{c}\PY{l+s}{t}\PY{l+s}{i}\PY{l+s}{v}\PY{l+s}{e}\PY{p}{)}
|
|
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k}{endif}
|
|
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{o}{/\PYZbs{}}\PY{l+s}{ }\PY{k}{for}\PY{p}{(}\PY{n+nv}{i}\PY{l+s}{ }\PY{o}{in}\PY{l+s}{ }\PY{n+nb}{min}\PY{p}{(}\PY{n+nb}{index\PYZus{}set}\PY{p}{(}\PY{n+nv}{o}\PY{p}{)}\PY{p}{)}\PY{l+s}{.}\PY{l+s}{.}\PY{n+nv}{stage}\PY{o}{\PYZhy{}}\PY{l+m}{1}\PY{p}{)}\PY{l+s}{ }\PY{p}{(}
|
|
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{n+nv}{o}\PY{p}{[}\PY{n+nv}{i}\PY{p}{]}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nf}{lastval}\PY{p}{(}\PY{n+nv}{best}\PY{p}{[}\PY{n+nv}{i}\PY{p}{]}\PY{p}{)}
|
|
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{p}{)}
|
|
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{o}{/\PYZbs{}}\PY{l+s}{ }\PY{k}{if}\PY{l+s}{ }\PY{n+nf}{status}\PY{p}{(}\PY{p}{)}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nv}{SAT}\PY{l+s}{ }\PY{k}{then}
|
|
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{n+nv}{o}\PY{p}{[}\PY{n+nv}{stage}\PY{p}{]}\PY{l+s}{ }\PY{o}{\PYZlt{}}\PY{l+s}{ }\PY{n+nf}{sol}\PY{p}{(}\PY{l+s}{\PYZus{}}\PY{l+s}{o}\PY{l+s}{b}\PY{l+s}{j}\PY{l+s}{e}\PY{l+s}{c}\PY{l+s}{t}\PY{l+s}{i}\PY{l+s}{v}\PY{l+s}{e}\PY{p}{)}
|
|
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{k}{endif}
|
|
\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{l+s}{ }\PY{o}{/\PYZbs{}}\PY{l+s}{ }\PY{l+s}{\PYZus{}}\PY{l+s}{o}\PY{l+s}{b}\PY{l+s}{j}\PY{l+s}{e}\PY{l+s}{c}\PY{l+s}{t}\PY{l+s}{i}\PY{l+s}{v}\PY{l+s}{e}\PY{l+s}{ }\PY{o}{=}\PY{l+s}{ }\PY{n+nv}{o}\PY{p}{[}\PY{n+nv}{stage}\PY{p}{]}
|
|
\PY{l+s}{ }\PY{l+s}{ }\PY{k}{endif}\PY{p}{;}
|
|
\end{Verbatim}
|