cleanup and fixed spacing issues

Author: SaswatPadhi

language/listing-style.tex

@@ -1,24 +1,25 @@
 \lstset{
-    basicstyle=\ttfamily,
+    basicstyle=\ttfamily\color{black!80!white},
     captionpos=b,
     extendedchars=true,
     tabsize=2,
     columns=fixed,
     keepspaces=true,
     showstringspaces=false,
     breaklines=true,
-    commentstyle=\color{gray},
-    keywordstyle=[1]\color{blue!72!black},
-    keywordstyle=[2]\color{orange!64!black},
-    keywordstyle=[3]\color{teal!80!black},
-    keywordstyle=[4]\color{red!64!black},
-    keywordstyle=[5]\color{green!40!black},
-    keywordstyle=[6]\color{purple!96!black},
+    commentstyle=\color{gray!90!white},
+    keywordstyle=[1]\color{blue!75!black},
+    keywordstyle=[2]\color{orange!75!black},
+    keywordstyle=[3]\color{teal!90!black},
+    keywordstyle=[4]\color{red!65!black},
+    keywordstyle=[5]\color{green!45!black},
+    keywordstyle=[6]\color{purple!95!black},
+    keywordstyle=[7]\color{black},
     sensitive=true,
     numbers=left,
     numberblanklines=false,
     numbersep=8pt,
-    numberstyle=\ttfamily\fontsize{8pt}{8.5}\selectfont\color{gray},
+    numberstyle=\ttfamily\fontsize{8pt}{8.5}\selectfont\color{gray!60!white},
     xleftmargin=2em,
 }
 
@@ -28,17 +29,29 @@
 
 \lstdefinelanguage{SyGuS}{
     alsoletter={\_,-,+,*,=,>,<,:},
-    escapeinside={([}{])},
     mathescape=true,
     texcl=true,
     morecomment=[l]{;},
     morestring=[b]",
-    keywords=[1]{check-synth, set-feature, set-logic, set-option},
-    keywords=[2]{BV, CHC, CHC_, CHC_QF_, DTLIA, DTNIA, Inv, Inv_, Inv_QF_, LIA, LRA, NIA, PBE, PBE_, QF_, S, SLIA, CHC_LIA, Inv\_LIA, PBE\_SLIA},
-    keywords=[3]{declare-var, declare-datatype, declare-datatypes, declare-sort, define-fun, define-sort},
-    keywords=[4]{assume, chc-constraint, constraint, inv-constraint},
-    keywords=[5]{synth-fun, synth-inv, synth-pred},
-    keywords=[6]{:fwd-decls, :grammars, :oracles, :recursion}
+    keywords=[1]{check-synth, %
+                 set-feature, set-logic, set-option},
+    keywords=[2]{BV, CHC, CHC_, CHC_QF_, CHC_LIA, DTLIA, DTNIA, %
+                 Inv, Inv_, Inv_QF_, Inv\_LIA, LIA, LRA, NIA, %
+                 PBE, PBE_, PBE\_SLIA, QF_, S, SLIA},
+    keywords=[3]{declare-var, %
+                 declare-datatype, declare-datatypes, %
+                 declare-sort, %
+                 define-fun, define-sort},
+    keywords=[4]{assume, %
+                 chc-constraint, constraint, inv-constraint},
+    keywords=[5]{synth-fun},
+    keywords=[6]{oracle-assume, oracle-constraint, %
+                 declare-oracle-fun, %
+                 declare-correctness-oracle, declare-correctness-cex-oracle, %
+                 oracle-constraint-cex, oracle-constraint-io, %
+                 oracle-constraint-membership, %
+                 oracle-constraint-poswitness, oracle-constraint-negwitness}
+    keywords=[7]{:fwd-decls, :grammars, :oracles, :recursion}
 }
 
-\global\long\def\sygusinline{\lstinline[language=SyGuS,mathescape]}
+\global\long\def\code{\lstinline[language=SyGuS]}

language/sygus-macros.tex

@@ -120,7 +120,7 @@
 
 \global\long\def\attribute{\left\langle Attr\right\rangle }
 
-\global\long\def\constdeclkwd{\texttt{declare-const}}
+%\global\long\def\constdeclkwd{\texttt{declare-const}}
 
 
 \global\long\def\dtdeclkwd{\texttt{declare-datatype}}
@@ -135,8 +135,8 @@
 \global\long\def\recfunsdefkwd{\texttt{define-funs-rec}}
 
 \global\long\def\setlogickwd{\texttt{set-logic}}
-\global\long\def\setlogicinputkwd{\texttt{set-logic-input}}
-\global\long\def\setlogicoutputkwd{\texttt{set-logic-output}}
+% \global\long\def\setlogicinputkwd{\texttt{set-logic-input}}
+% \global\long\def\setlogicoutputkwd{\texttt{set-logic-output}}
 \global\long\def\setinfokwd{\texttt{set-info}}
 
 
@@ -154,7 +154,7 @@
 
 \global\long\def\fundeclkwd{\texttt{declare-fun}}
 
-%TODO: Switch to \global\long\def\synthfunkwd{\text{\sygusinline|synth-fun|}}
+%TODO: Switch to \global\long\def\synthfunkwd{\text{\code|synth-fun|}}
 \global\long\def\synthfunkwd{\texttt{synth-fun}}
 
 \global\long\def\synthinvkwd{\texttt{synth-inv}}