\renewcommand{\phi}{\varphi}
\renewcommand{\implies}{\rightarrow}
\newcommand{\imp}{\rightarrow}
\newcommand{\entails}{\enspace \vdash \enspace}
\newcommand{\ent}{\enspace \vdash \enspace}
\newcommand{\eqv}{\leftrightarrow}
\newcommand{\biimp}{\leftrightarrow}
\newcommand{\lxor}{\oplus}
\newcommand{\nentails}{\nvdash}
\newcommand{\nmodels}{\nvDash}

\newcommand{\true}{\ensuremath{\top}}
\newcommand{\false}{\ensuremath{\bot}}

% multiple choice itemize
\newcommand{\ticked}{\ensuremath{\boxtimes}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% TSEITIN rules
\newcommand{\tseitinAnd}[3]{
  \def\CHI{#1}%
  \def\PHI{#2}%
  \def\PSI{#3}%
  \ensuremath{(\lnot \CHI \lor \PHI) \land (\lnot \CHI \lor \PSI) \land (\lnot \PSI \lor \lnot \PSI \lor \CHI)}%
}
\newcommand{\tseitinOr}[3]{
  \def\CHI{#1}%
  \def\PHI{#2}%
  \def\PSI{#3}%
  \ensuremath{(\lnot \PHI \lor \CHI) \land (\lnot \PSI \lor \CHI) \land (\lnot \CHI \lor \lnot \PHI \lor \PSI)}%
}
\newcommand{\tseitinNot}[2]{
  \def\CHI{#1}%
  \def\PHI{#2}%
  \ensuremath{(\lnot \CHI \lor \lnot \PHI) \land (\CHI \lor \PHI)}%
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% DPLL helper
\newenvironment{dplltabular}[1]
  {\begin{tabular}{ |l|*{#1}{c|} } \hline}
  {\end{tabular}}

\ExplSyntaxOn
\NewDocumentCommand{\dpllrow}{m}
 {
  \seq_set_split:Nnn \l_row {|} { #1 }
  \seq_use:Nn \l_row { & }
  \\
  \hline
 }
\seq_new:N \l_row % allocate a sequence
\ExplSyntaxOff

\newcommand{\dpllStep}[1]{
  Step & \dpllrow{#1}
}

\newcommand{\dpllDecL}[1]{
  Decision Level & \dpllrow{#1}
}

\newcommand{\dpllAssi}[1]{
  Assignment & \dpllrow{#1}
}

\newcommand{\dpllBCP}[1]{
  BCP & \dpllrow{#1}
}

\newcommand{\dpllPL}[1]{
  PL & \dpllrow{#1}
}

\newcommand{\dpllDeci}[1]{
  Decision & \dpllrow{#1}
}

\newcommand{\dpllClause}[3]{
  \def\ITEM{#1}%
  \def\CLAUSE{#2}%
  Cl. \ITEM: \CLAUSE & \dpllrow{#3}
}

\ExplSyntaxOn
\NewDocumentCommand{\clause}{m}
 {
  \seq_set_split:Nnn \l_clause {;} { #1 }
  \seq_use:Nn \l_clause { \lor }
 }
\seq_new:N \l_clause % allocate a sequence
\ExplSyntaxOff

\ExplSyntaxOn
\NewDocumentCommand{\cube}{m}
 {
  \seq_set_split:Nnn \l_cube {;} { #1 }
  \seq_use:Nn \l_cube { \land }
 }
\seq_new:N \l_cube % allocate a sequence
\ExplSyntaxOff

\newcommand{\cmark}{\ding{51}}
\newcommand{\xmark}{\ding{55}}
\newcommand{\done}{\cmark}
\newcommand{\conflict}{\{\} \xmark}

\NewEnviron{conflictgraph}[1][1.5cm]{%
  \begin{tikzpicture}[->,
                      >=stealth',
                      shorten >=1pt,
                      auto,
                      node distance=#1,
                      thick,
                      base node/.style={circle,draw,minimum size=20pt},
                      real node/.style={double,circle,draw,minimum size=20pt}]
          \BODY
  \end{tikzpicture}
}

\newcommand*\circled[1]{\tikz[baseline=(char.base)]{
            \node[shape=circle,draw,inner sep=1.5pt] (char) {#1};}}

\tikzset{
  line/.style={-},
  dot/.style={decoration={
  markings,
  mark=at position #1 with {\draw circle (2pt);}},postaction={decorate}},
  fulldot/.style={decoration={
  markings,
  mark=at position #1 with {\fill circle (2pt);}},postaction={decorate}},
}

\newenvironment{scprooftree}[1]%
  {\gdef\scalefactor{#1}\begin{center}\proofSkipAmount \leavevmode}%
  {\scalebox{\scalefactor}{\DisplayProof}\proofSkipAmount \end{center} }

\tikzset{
  line/.style={-},
  dot/.style={decoration={
  markings,
  mark=at position #1 with {\draw circle (2pt);}},postaction={decorate}},
  fulldot/.style={decoration={
  markings,
  mark=at position #1 with {\fill circle (2pt);}},postaction={decorate}},
}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% BDD helper

\newenvironment{cofactors}
  {\begin{tabbing}}
  {\end{tabbing}}



\NewEnviron{bdd}[1][3em]{%
  \begin{tikzpicture}[node distance=#1,
                      base node/.style={circle,draw,minimum size=20pt},
                      func node/.style={rectangle,draw,minimum size=10pt},
                      cofactor/.style={circle,draw,minimum size=10pt},
                      phantom/.style={circle,draw,inner sep=0pt,minimum size=0pt}]
          \BODY
  \end{tikzpicture}
}

\newcommand{\funcEdge}[3][]{
  \path[] (#2) edge [#1] (#3);
}
\newcommand{\thenEdge}[3][]{
  \path[] (#2) edge [#1] (#3);
}
\newcommand{\elseEdge}[3][]{
  \path[] (#2) edge [#1] node [midway,draw,circle,fill=white,transform shape,inner sep=0pt,minimum size=0.3em] (ref) {} (#3);
}
\newcommand{\negatedEdge}[3][]{
  \path[] (#2) edge [#1] node [midway,draw,circle,fill=black,transform shape,inner sep=0pt,minimum size=0.3em] (ref) {} (#3);
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\NewEnviron{egraph}[1][1.5cm]{%
  \begin{tikzpicture}[-,
                      >=stealth',
                      shorten >=1pt,
                      auto,
                      node distance=#1,
                      thick,
                      base node/.style={circle,draw,minimum size=20pt}]
          \BODY
  \end{tikzpicture}
}

\newcommand{\chord}[2]{
  \draw[dashed,red] (#1) -- (#2);
}

\newcommand{\egraphFuncConstraint}[3]{%
  &((e_{#1=#2}~\land~e_{#2=#3})~\imp~e_{#1=#3})~\land\\
  &((e_{#1=#2}~\land~e_{#1=#3})~\imp~e_{#2=#3})~\land\\
  &((e_{#1=#3}~\land~e_{#2=#3})~\imp~e_{#1=#2})
}

\newcommand{\eq}[2]{
  e_{#1=#2}
}

\newcommand{\ackermannFuncConstraint}[3]{%
  (#2=#3~\imp~#1_{#2}=#1_{#3})
}