Permalink
Browse files

Add information about the separate namespace

  • Loading branch information...
1 parent 75b17c1 commit 3b3e963f1ae49e9e4d25097c83a33476e9f455c1 @sid0 committed Mar 25, 2012
Showing with 15 additions and 0 deletions.
  1. +15 −0 doc/technical.tex
View
@@ -15,3 +15,18 @@ \section{Design and Implementation}
the aim of the interface is to hide the complexities of the C wrapper and stay
as close to the SMT-LIB v2 standard \cite{smtlib2:10} as possible, while
extending it in useful ways.
+
+We use a separate Racket namespace to store user-defined constants and functions
+in. Thus a command of the form \texttt{(smt:declare-fun x () Int)} will not
+create a binding for \texttt{x} in the caller's namespace. This has been done
+because several functions built into the SMT-LIB specification (such as
+\texttt{=} and \texttt{<=}) collide with Racket-provided symbols. However, the
+system does let the programmer substitute values from her own namespace using
+the \texttt{unquote} form familiar to Lisp programmers (usually shortened to a
+prefixed comma). So the following code asserts that \texttt{x} is 20.
+
+\begin{verbatim}
+(smt:declare-fun x () Int)
+(define n 20)
+(smt:assert (= x ,n))
+\end{verbatim}

0 comments on commit 3b3e963

Please sign in to comment.