minor fixes, added contrib directory

9 files changed, 956 insertions, 3 deletions

diff --git a/DESIGN_QUESTIONS b/DESIGN_QUESTIONS
index 670089c34..0e8f50245 100644
--- a/DESIGN_QUESTIONS
+++ b/DESIGN_QUESTIONS
@@ -58,7 +58,7 @@ theory.h
 
   // TODO: these use the current EM (but must be renamed)
 
-  // TODO design decisoin: instead of returning a set of literals
+  // TODO design decision: instead of returning a set of literals
   // here, perhaps we have an interface back into the prop engine
   // where we assert directly.  we might sometimes unknowingly assert
   // something clearly inconsistent (esp. in a parallel context).
@@ -66,3 +66,17 @@ theory.h
   // we're already inconsistent---also could strategize dynamically on
   // whether enough theory prop work has occurred.
   virtual void propagate(Effort level = FULL_EFFORT) = 0;
+
+  could provide a continuation (essentially) to propagate literals.
+  argument Propagator prop
+  class Propagator {
+    PropEngine d_pe;
+  public:
+    // may not return due to a longjmp (?) or perhaps an exception
+    // returns next continuation
+    Propagator operator()(Literal l);
+  };
+
+
+==========================
+TODO:  add throw() specifications
diff --git a/Makefile.am b/Makefile.am
index a60337f29..b224de9b0 100644
--- a/Makefile.am
+++ b/Makefile.am
@@ -1,4 +1,4 @@
 AUTOMAKE_OPTIONS = foreign
 ACLOCAL_AMFLAGS = -I m4
 
-SUBDIRS = src doc
+SUBDIRS = src doc contrib
diff --git a/configure.ac b/configure.ac
index d55e72eed..804401a92 100644
--- a/configure.ac
+++ b/configure.ac
@@ -28,6 +28,7 @@ AC_TYPE_UINT64_T
 
 AC_CONFIG_FILES([
   Makefile
+  contrib/Makefile
   doc/Makefile
   src/Makefile
   src/include/Makefile
diff --git a/contrib/Makefile.am b/contrib/Makefile.am
new file mode 100644
index 000000000..952fde6ed
--- /dev/null
+++ b/contrib/Makefile.am
@@ -0,0 +1 @@
+EXTRA_DIST = README
diff --git a/contrib/README b/contrib/README
new file mode 100644
index 000000000..47d4941bd
--- /dev/null
+++ b/contrib/README
@@ -0,0 +1,4 @@
+This directory is for contributions to CVC4 that aren't directly
+part of the main project.
+
+-- Morgan Deters <mdeters@cs.nyu.edu>  Mon, 09 Nov 2009 15:14:41 -0500
diff --git a/contrib/cvc-devel.el b/contrib/cvc-devel.el
new file mode 100644
index 000000000..3e1d75084
--- /dev/null
+++ b/contrib/cvc-devel.el
@@ -0,0 +1,218 @@
+;;;; Add to your ~/.emacs the following lines:
+;;;;
+;;;;   (load-path "/full/path/to/this/file")
+;;;;   (require 'cvc-devel)
+;;;;   
+;;;; If you want to modify the key binding for inserting the comment,
+;;;; add also something like this:
+;;;;
+;;;;   (setq cvc-devel-comment-key "\M-/")
+;;;;
+
+(defvar cvc-devel-comment-key "\C-c\C-h"
+  "The hot key binding to insert an appropriate comment in C++ header
+in CVC code")
+
+(require 'cc-mode)
+(add-to-list 'c++-mode-hook
+	     '(lambda ()
+		(local-set-key cvc-devel-comment-key
+			       'insert-comment-template)))
+
+(defun insert-comment-template ()
+  "Insert a comment template into C++ file in the CVC style.  The
+comment is different depending on where it is inserted.  For example,
+inserting it in the empty file will produce a file comment, a class
+comment will be inserted before a class definition, and so on."
+  (interactive)
+  ; Check for macro
+  (cond
+   ((catch 'not-macro
+      (progn
+	(set-mark (point))
+	(cond ((not (search-forward "#define" nil t))
+	       (throw 'not-macro t)))
+	(beginning-of-line)
+	(cond ((not (= (mark) (point)))
+	       (progn
+		 (goto-char (mark))
+		 (throw 'not-macro t))))
+	; It's a macro: insert the comment template
+	(forward-char 7)
+	(re-search-forward "[^ ]")
+	(backward-char)
+	(set-mark (point))
+	(re-search-forward " \\|(\\|^")
+	(backward-char)
+	(copy-region-as-kill (mark) (point))
+	(beginning-of-line)
+	(insert-string
+"/*****************************************************************************/
+/*!
+ *\\def ")
+	(yank)
+	(insert-string "
+ *
+ * Author: ")
+        (insert-string (user-full-name))
+        (insert-string "
+ *
+ * Created: ")
+	(insert-string (current-time-string))
+	(insert-string "
+ *
+ * 
+ */
+/*****************************************************************************/
+")
+	(forward-line -3)
+	(search-forward "* ")
+	()
+      )
+    )
+    (cond
+     ((catch 'not-function
+	(progn
+	  (set-mark (point))
+	  (cond ((not (search-forward "(" nil t))
+		 (throw 'not-function t)))
+	  (beginning-of-line)
+	  (cond ((not (= (mark) (point)))
+		 (progn
+		   (goto-char (mark))
+		   (throw 'not-function t))))
+       	  ; It's a function: insert the comment template
+	  (search-forward "(")
+	  (re-search-backward "[^ ] *(")
+	  (forward-char)
+	  (set-mark (point))
+	  (re-search-backward " \\|^.")
+	  (re-search-forward "[^ ]")
+	  (backward-char)
+	  (copy-region-as-kill (mark) (point))
+	  (beginning-of-line)
+	  (insert-string
+"/*****************************************************************************/
+/*!
+ * Function: ")
+	  (yank)
+	  (insert-string "
+ *
+ * Author: ")
+          (insert-string (user-full-name))
+          (insert-string "
+ *
+ * Created: ")
+	  (insert-string (current-time-string))
+	  (insert-string "
+ *
+ * 
+ */
+/*****************************************************************************/
+")
+	  (forward-line -3)
+	  (search-forward "* ")
+	  ()
+	  )
+	)
+      (cond
+       ((catch 'not-class
+	  (progn
+	    (set-mark (point))
+	    (cond ((not (search-forward "class" nil t))
+		   (throw 'not-class t)))
+	    (beginning-of-line)
+	    (cond ((not (= (mark) (point)))
+		 (progn
+		   (goto-char (mark))
+		   (throw 'not-class t))))
+       	    ; It's a class definition: insert the comment template
+	    (forward-char 5)
+	    (re-search-forward "[^ ]")
+	    (backward-char)
+	    (set-mark (point))
+	    (re-search-forward "^\\| \\|{")
+	    (backward-char)
+	    (copy-region-as-kill (mark) (point))
+	    (beginning-of-line)
+	    (insert-string
+"/*****************************************************************************/
+/*!
+ *\\class ")
+	  (yank)
+	  (insert-string "
+ *\\brief ")
+          (yank)
+          (insert-string "
+ *
+ * Author: ")
+          (insert-string (user-full-name))
+          (insert-string "
+ *
+ * Created: ")
+	  (insert-string (current-time-string))
+	  (insert-string "
+ *
+ * 
+ */
+/*****************************************************************************/
+")
+	    (forward-line -4)
+	    (search-forward "* ")
+	    ()
+	    )
+	  )
+	(cond
+	 ((catch 'not-bof
+	    (progn
+	      (set-mark (point))
+	      (beginning-of-buffer)
+	      (cond ((not (= (mark) (point)))
+		     (progn
+		       (goto-char (mark))
+		       (throw 'not-bof t))))
+              ; At beginning of file: insert beginning of file comment
+	      (insert-string
+"/*****************************************************************************/
+/*!
+ *\\file ")
+              (insert-string (file-name-nondirectory (buffer-file-name)))
+	      (insert-string "
+ *\\brief 
+ *
+ * Author: ")
+          (insert-string (user-full-name))
+          (insert-string "
+ *
+ * Created: ")
+	      (insert-string (current-time-string))
+	      (insert-string "
+ */
+/*****************************************************************************/
+")
+	      (forward-line -7)
+	      (search-forward "brief ")
+	      ()
+	    )
+	  )
+          ; Insert default comment template
+	  (insert-string
+"/*****************************************************************************/
+/*
+ * 
+ */
+/*****************************************************************************/
+")
+	  (forward-line -3)
+	  (search-forward "* ")
+         )
+	)
+       )
+      )
+     )
+    )
+   )
+  )
+)
+
+(provide 'cvc-devel)
diff --git a/contrib/cvc-mode.el b/contrib/cvc-mode.el
new file mode 100644
index 000000000..f159944dd
--- /dev/null
+++ b/contrib/cvc-mode.el
@@ -0,0 +1,715 @@
+;;;; /*!
+;;;;  * \file cvc-mode.el
+;;;;  * \brief Emacs mode for CVC programs in presentation language
+;;;;  * 
+;;;;  * Author: Sergey Berezin
+;;;;  * 
+;;;;  * Created: Mon Aug 11 12:29:32 2003
+;;;;  *
+;;;;  * <hr>
+;;;;  *
+;;;;  * License to use, copy, modify, sell and/or distribute this software
+;;;;  * and its documentation for any purpose is hereby granted without
+;;;;  * royalty, subject to the terms and conditions defined in the \ref
+;;;;  * LICENSE file provided with this distribution.
+;;;;  *
+;;;;  * <hr>
+;;;;  * 
+;;;;  */
+
+;;;; To use this library, place the following lines into your ~/.emacs file:
+;;;;
+;;;; ;;; CVC mode
+;;;; (autoload 'cvc-mode "cvc-mode" "CVC specifications editing mode." t)
+;;;; (setq auto-mode-alist 
+;;;;       (append  (list '("\\.cvc$" . cvc-mode)) auto-mode-alist))
+;;;;
+;;;; Of course, the file cvc-mode.el must be in one of the directories in your
+;;;; `load-path'. C-h v load-path to see the list, or `cons' your own path:
+;;;; (setq load-path (cons "/the/full/path/to-your/dir" load-path))
+;;;;
+;;;; To turn the font-lock on by default, put in .emacs
+;;;; (global-font-lock-mode t) ;; if you use gnu-emacs, or
+;;;; (setq-default font-lock-auto-fontify t) ;; if you use xemacs.
+;;;;
+;;;; In GNU emacs faces `font-lock-preprocessor-face' and 
+;;;; `font-lock-variable-name-face' may not be predefined.
+;;;; In this case they are defined automatically when smv-mode.el
+;;;; is loaded the first time. You can also define them yourself in .emacs:
+;;;;
+;;;; ;;; Make faces that are not in gnu-emacs font-lock by default
+;;;; (defvar font-lock-preprocessor-face 'font-lock-preprocessor-face)
+;;;; (defvar font-lock-variable-name-face 'font-lock-variable-name-face)
+;;;; (make-face 'font-lock-preprocessor-face)
+;;;; (make-face 'font-lock-variable-name-face)
+
+(require 'font-lock)
+(require 'compile)
+
+(defvar cvc-font-lock-mode-on t
+  "If not nil, turn the fontification on.")
+
+;;;; Syntax definitions
+
+(defvar cvc-mode-syntax-table nil  "Syntax table used while in CVC mode.")
+
+(if cvc-mode-syntax-table ()
+    (let ((st (syntax-table)))
+      (unwind-protect
+	   (progn
+	     (setq cvc-mode-syntax-table (make-syntax-table))
+	     (set-syntax-table cvc-mode-syntax-table)
+	     (modify-syntax-entry ?_ "w")
+	     (modify-syntax-entry ?- "w")
+	     (modify-syntax-entry ?\? "w")
+	     (modify-syntax-entry ?: "." )
+	     (modify-syntax-entry ?% "<")
+	     (modify-syntax-entry ?\f ">")
+	     (modify-syntax-entry ?\n ">"))
+	(set-syntax-table st))))
+
+;;;; Fontification stuff
+
+(defun cvc-keyword-match (keyword)
+;  "Convert a string into a regexp matching any capitalization of that string."
+  "Convert a string into a regexp matching that string as a separate word."
+;  (let ((regexp "")
+;	(index 0)
+;	(len (length keyword)))
+;    (while (< index len)
+;      (let ((c (aref keyword index)))
+;	(setq regexp
+;	      (concat regexp (format "[%c%c]" (downcase c) (upcase c))))
+;	(setq index (+ index 1))))
+    (format "\\b%s\\b" keyword))
+;)
+
+(defvar cvc-font-lock-separator-face 'cvc-font-lock-separator-face)
+(defvar font-lock-preprocessor-face 'font-lock-preprocessor-face)
+(defvar font-lock-variable-name-face 'font-lock-variable-name-face)
+
+(if (facep 'font-lock-preprocessor-face) ()
+    (progn
+      (make-face 'font-lock-preprocessor-face)
+      (set-face-foreground 'font-lock-preprocessor-face "green4")))
+
+(if (facep 'font-lock-variable-name-face) ()
+    (progn
+      (make-face 'font-lock-variable-name-face)
+      (set-face-foreground 'font-lock-variable-name-face "deeppink")))
+
+(if (facep 'cvc-font-lock-separator-face) ()
+    (progn
+      (make-face 'cvc-font-lock-separator-face)
+      (set-face-foreground 'cvc-font-lock-separator-face "indianred")))
+
+(defvar cvc-mode-hook nil
+  "Functions to run when loading an CVC file.")
+
+(defconst cvc-keywords
+  '("ASSERT" "QUERY" "TRACE" "UNTRACE" "OPTION" "HELP" "TRANSFORM"
+    "PRINT" "ECHO" "INCLUDE" "DUMP_ASSUMPTIONS" "DUMP_PROOF" "DUMP_SIG"
+    "WHERE" "COUNTEREXAMPLE" "PUSH" "POP" "POP_SCOPE" "POPTO" "RESET"
+    "CONTEXT"
+    "TYPE" "DATATYPE" "SUBTYPE"
+    "REAL" "INT" "BOOLEAN" "ARRAY" "OF"
+    "TRUE" "FALSE" "FLOOR"
+    "IF" "THEN" "ELSIF" "ELSE" "ENDIF" "LET" "IN" "END" "LAMBDA" "WITH"
+    "FORALL" "EXISTS" 
+    "AND" "OR" "XOR" "NOT" )
+  "The list of CVC keywords.")
+
+(defconst cvc-declaration-keywords
+  '("ASSERT" "QUERY" "TRACE" "UNTRACE" "OPTION" "HELP" "TRANSFORM"
+    "PRINT" "ECHO" "INCLUDE" "DUMP_ASSUMPTIONS" "DUMP_PROOF" "DUMP_SIG"
+    "WHERE" "COUNTEREXAMPLE" "PUSH" "POP" "POP_SCOPE" "POPTO" "RESET"
+    "CONTEXT")
+  "The list of keywords that open a declaration. Used for indentation.")
+
+(defconst cvc-declaration-keywords-regexp
+  (mapconcat 'cvc-keyword-match cvc-declaration-keywords "\\|"))
+
+(defconst cvc-openning-keywords
+  '("case" "for" "next" "init")
+  "The list of keywords that open a subexpression. Used for indentation.")
+
+(defconst cvc-openning-keywords-regexp
+  (mapconcat 'cvc-keyword-match cvc-openning-keywords "\\|"))
+
+(defconst cvc-closing-keywords
+  '("esac")
+  "The list of keywords that close a subexpression. Used for indentation.")
+
+(defconst cvc-closing-keywords-regexp
+  (mapconcat 'cvc-keyword-match cvc-closing-keywords "\\|"))
+
+(defconst cvc-infix-operators
+  '("<->" "<-" "->" ":=" "<=w\\>" ">=w\\>" "<w\\>" ">w\\>" "=w\\>"
+    "+w\\>" "-w\\>" "*w\\>" "<=" ">=" "!=" "=" "\\[" "\\]"
+    "\\b-\\b" "+" "|" "&" "<" ">")
+  "The list of regexps that match CVC infix operators. The distinction
+is made primarily for indentation purposes.")
+
+(defconst cvc-infix-operators-regexp
+  (mapconcat 'identity cvc-infix-operators "\\|"))
+
+(defconst cvc-other-operators
+  '("!" "(#" "#)")
+  "Non-infix CVC operators that are not listed in `cvc-infix-operators'.")
+
+(defconst cvc-other-operators-regexp
+  (mapconcat 'identity cvc-other-operators "\\|"))
+
+(defconst cvc-operators (append cvc-infix-operators cvc-other-operators)
+  "The list of regexps that match CVC operators. It is set to the
+concatenation of `cvc-infix-operators' and `cvc-other-operators'.")
+
+(defconst cvc-separator-regexp "[,.;():]"
+  "A regexp that matches any separator in CVC mode.")
+
+(defconst cvc-font-lock-keywords-1
+  (purecopy
+   (list
+    (list (concat (cvc-keyword-match "MODULE") " *\\([-_?A-Za-z0-9]+\\)")
+	  1 'font-lock-preprocessor-face)
+    (list (concat "\\(" (cvc-keyword-match "init") "\\|"
+		  (cvc-keyword-match "next")
+		  "\\)(\\s-*\\([][_?.A-Za-z0-9-]+\\)\\s-*)\\s-*:=")
+	  2 'font-lock-variable-name-face)
+    ;;; For DEFINE and invar assignments
+    (list "\\([][_?.A-Za-z0-9-]+\\)\\s-*:="
+	  1 'font-lock-variable-name-face)
+    (list "\\<\\([Aa]\\|[Ee]\\)\\[" 1 'font-lock-keyword-face)
+    (list (concat "\\("
+		  (mapconcat 'identity cvc-operators "\\|")
+		  "\\)")
+	  1 'font-lock-function-name-face 'prepend)
+    (mapconcat 'cvc-keyword-match cvc-keywords "\\|")
+;; Fix the `%' comments
+    (list "\\(%.*$\\)" 1 'font-lock-comment-face t) ))
+  "Additional expressions to highlight in CVC mode.")
+
+(defconst cvc-font-lock-keywords-2
+  (purecopy 
+   (append cvc-font-lock-keywords-1
+	   (list
+	    (list "\\([{}]\\)" 1 'font-lock-type-face)
+	    (list (concat "\\(" cvc-separator-regexp "\\)")
+		  1 'cvc-font-lock-separator-face 'prepend))))
+  "Additional expressions to highlight in CVC mode.")
+  
+(defconst cvc-font-lock-keywords
+  (if font-lock-maximum-decoration
+      cvc-font-lock-keywords-2
+      cvc-font-lock-keywords-1))
+
+(defun cvc-minimal-decoration ()
+  (interactive)
+  (setq font-lock-keywords cvc-font-lock-keywords-1))
+
+(defun cvc-maximal-decoration ()
+  (interactive)
+  (setq font-lock-keywords cvc-font-lock-keywords-2))
+
+;;;; Running CVC 
+
+(defvar cvc-command "cvc3" 
+  "The command name to run CVC. The default is usually \"cvc3\"")
+
+(defvar cvc-sat-option nil
+  "Search Engine choice in CVC.  Valid values are nil,
+\"default\", \"simple\", and \"fast\", or any other values reported by
+cvc3 -h.")
+
+(defvar cvc-trace-flags nil
+  "List of trace flags given on the command line as +trace options")
+
+(defvar cvc-verbose-level nil
+"The verbose mode of CVC. Valid values are nil and \"quiet\".  This
+value is passed to the CVC process as +/-quiet opton.")
+
+(defvar cvc-command-line-args nil
+  "Miscellaneous CVC command line args.
+Must be a single string or nil.")
+
+(defvar cvc-compile-buffer nil
+  "The buffer associated with inferior CVC process.
+This variable is updated automatically each time CVC process takes off.")
+
+(defvar cvc-options-changed nil)
+
+(defvar cvc-current-buffer nil
+  "The current CVC editing buffer.
+This variable is buffer-local.")
+(make-local-variable 'cvc-current-buffer)
+
+(defun cvc-args (file &optional args)
+  "Compiles the string of CVC command line args from various variables."
+  (mapconcat 'identity
+	     (append
+	      (if cvc-sat-option (list "-sat" cvc-sat-option) nil)
+	      (if (eq cvc-verbose-level "quiet") (list "+quiet") nil)
+	      (mapcar '(lambda (str) (format "+trace \"%s\"" str)) cvc-trace-flags)
+	      (if cvc-command-line-args (list cvc-command-line-args))
+	      (if args (list args) nil)
+	      (list "<" file))
+	     " "))
+
+(defun cvc-run ()
+  "Runs CVC on the current buffer."
+  (interactive)
+  (let ((buffer (current-buffer)))
+    (if (buffer-file-name)
+	(progn
+	  (if (buffer-modified-p) (cvc-save-buffer))
+	  (setq cvc-compile-buffer 
+		(compile-internal
+		 (concat "time " cvc-command " " (cvc-args (buffer-file-name)))
+				  "No more errors"
+				  "CVC"))
+	  (set-buffer cvc-compile-buffer) ;;; Doesn't work???
+	  (end-of-buffer)
+	  (set-buffer buffer)
+	  )
+    (error "Buffer does not seem to be associated with any file"))) )
+
+
+(defun cvc-save-options ()
+  "Saves current options in *.opt file."
+  (interactive)
+  (let* ((buffer (current-buffer))
+	 (opt-file-name 
+	  (let ((match (string-match "\\.cvc$"
+				     (buffer-file-name))))
+	    (if match
+		(concat (substring (buffer-file-name)
+				   0 match)
+			".opt")
+	      (concat (buffer-file-name) ".opt"))))
+	 (opt-buffer-name 
+	  (let ((match (string-match "\\.cvc$"
+				     (buffer-name))))
+	    (if match
+		(concat (substring (buffer-name)
+				   0 match)
+			".opt")
+	      (concat (buffer-name) ".opt"))))
+	 (opt-buffer-exists (get-buffer opt-buffer-name))
+	 (opt-buffer (get-buffer-create opt-buffer-name))
+	 (save-options-from-buffer 
+	  (and opt-buffer-exists 
+	       (buffer-modified-p opt-buffer)
+	       (y-or-n-p (format "buffer %s is modified. Save options from that buffer?" 
+				 (buffer-name opt-buffer)))))
+	 (options (format ";;;; This file is generated automatically.\n(setq cvc-sat-option %S)\n(setq cvc-verbose-level %S)\n(setq cvc-trace-flags '%S)\n(setq cvc-command-line-args %S)\n"
+			  cvc-sat-option
+			  cvc-verbose-level
+			  cvc-trace-flags
+			  cvc-command-line-args)))
+    (set-buffer opt-buffer)
+    (if save-options-from-buffer (cvc-save-and-load-options)
+      (progn
+	(erase-buffer)
+	(insert options)
+	(write-file opt-file-name)
+	(kill-buffer opt-buffer)))
+    (set-buffer buffer)
+    (setq cvc-options-changed nil)
+    (message "Options are saved.")))
+
+(defun cvc-save-and-load-options ()
+  "Saves the current buffer and updates CVC options in the associated
+buffer.  This buffer is either the value of `cvc-current-buffer', or
+it tries to make a few reasonable guesses. If no CVC buffer is found,
+only saves the current buffer.
+
+Normally is called from the *.opt file while editing options for CVC
+specification." 
+  (interactive)
+  (let* ((buffer (current-buffer))
+	 (buffer-file (buffer-file-name))
+	 (cvc-buffer-name
+	  (let* ((match (string-match "\\.[^.]*$" (buffer-name))))
+	    (if match
+		(concat (substring (buffer-name) 0 match) ".cvc")
+	      (concat (buffer-name) ".cvc"))))
+	 (cvc-buffer (get-buffer cvc-buffer-name))
+	 (cvc-buffer
+	  (cond (cvc-buffer cvc-buffer)
+		((and (boundp 'cvc-current-buffer)
+		      (buffer-live-p cvc-current-buffer))
+		 cvc-current-buffer)
+		(t nil))))
+    (save-buffer)
+    (if cvc-buffer
+	(let ((cvc-window (get-buffer-window cvc-buffer))
+	      (window (get-buffer-window buffer)))
+	  (set-buffer cvc-buffer)
+	  (load buffer-file)
+	  (setq cvc-current-buffer cvc-buffer)
+	  (if cvc-window 
+	      (select-window cvc-window)
+	    (switch-to-buffer cvc-buffer))
+	  (if window
+	      (delete-window window))
+	  (setq cvc-options-changed nil)))) )
+
+(defun cvc-save-and-return ()
+  "Saves the current buffer and returns back to the associated CVC
+buffer.  The CVC buffer is either the value of `cvc-current-buffer', or
+it tries to make a few reasonable guesses. If no CVC buffer is found,
+only saves the current buffer.
+
+Normally is called from the *.ord buffer while editing variable ordering
+for CVC specification. Bound to \\[cvc-save-and-return]"
+  (interactive)
+  (let* ((buffer (current-buffer))
+	 (cvc-buffer-name
+	  (let* ((match (string-match "\\.[^.]*$" (buffer-name))))
+	    (if match
+		(concat (substring (buffer-name) 0 match) ".cvc")
+	      (concat (buffer-name) ".cvc"))))
+	 (cvc-buffer (get-buffer cvc-buffer-name))
+	 (cvc-buffer
+	  (cond (cvc-buffer cvc-buffer)
+		((and (boundp 'cvc-current-buffer)
+		      (buffer-live-p cvc-current-buffer))
+		 cvc-current-buffer)
+		(t nil))))
+    (save-buffer)
+    (if cvc-buffer
+	(let ((cvc-window (get-buffer-window cvc-buffer)))
+	  (setq cvc-current-buffer cvc-buffer)
+	  (if cvc-window 
+	      (select-window cvc-window)
+	    (switch-to-buffer cvc-buffer))
+	  (if (get-buffer-window buffer) 
+	      (delete-window (get-buffer-window buffer)))))) )
+
+(defun cvc-edit-options ()
+  "Loads current options in a new buffer and lets the user edit it.
+Run \\[eval-buffer] when done."
+  (interactive)
+  (let* ((buffer (current-buffer))
+	 (opt-buffer-name 
+	  (let ((match (string-match "\\.cvc$"
+				     (buffer-name))))
+	    (if match
+		(concat (substring (buffer-name)
+				   0 match)
+			".opt")
+	      (concat (buffer-name) ".opt"))))
+	 (opt-buffer (get-buffer-create opt-buffer-name))
+	 	 (options (format ";;;; This file is generated automatically.\n(setq cvc-sat-option %S)\n(setq cvc-verbose-level %S)\n(setq cvc-trace-flags '%S)\n(setq cvc-command-line-args %S)\n"
+			  cvc-sat-option
+			  cvc-verbose-level
+			  cvc-trace-flags
+			  cvc-command-line-args)))
+    (setq cvc-options-changed t)
+    (switch-to-buffer-other-window opt-buffer)
+    (set-visited-file-name opt-buffer-name)
+    (erase-buffer)
+    (insert options)
+    (make-local-variable 'cvc-currect-buffer)
+    (setq cvc-current-buffer buffer)
+    (cvc-options-edit-mode)))
+
+(defun cvc-interrupt ()
+  "Kills current CVC process."
+  (interactive)
+  (quit-process (get-buffer-process cvc-compile-buffer) t))
+
+(defun cvc-send-signal (sig)
+  "Sends signal SIG to the CVC process. SIG must be an integer."
+  (if (get-buffer-process cvc-compile-buffer)
+      (if (file-exists-p ".cvc-pid")
+	(save-excursion
+	  (let ((buf (get-buffer-create ".cvc-pid")))
+	    (set-buffer buf)
+	    (erase-buffer)
+	    (insert-file-contents ".cvc-pid")
+	    (let ((pid (read buf)))
+	      (if (integerp pid)
+		  (signal-process pid sig)
+		(error "The file .cvc-pid is screwed up: %s" pid)))
+	    (kill-buffer buf)))
+	(error "Your CVC version does not support signal handling"))
+    (error "CVC is not running")))
+
+(defun cvc-send-usr1 () 
+  "Sends SIGUSR1 to the current CVC process. I have a version of CVC
+that uses it to toggle dynamic variable ordering."
+  (interactive)
+  (cvc-send-signal 10))
+
+(defun cvc-send-usr2 () 
+  "Sends SIGUSR2 to the current CVC process. I have a version of CVC
+that uses it to force garbage collection."
+  (interactive)
+  (cvc-send-signal 12))
+
+(defun cvc-set-verbose-level (arg)
+  "Sets CVC verbose level to use in command line option +/-quiet.
+If empty line is given, use the default."
+  (interactive (list (read-from-minibuffer "Set verbose level to: "
+			       cvc-verbose-level)))
+  (if (stringp arg)
+      (progn
+	(if (string= arg "") (setq cvc-verbose-level nil)
+	  (setq cvc-verbose-level arg))
+	(setq cvc-options-changed t))
+    (error "Not a string. The value is not set.")))
+
+(defun cvc-set-command (arg)
+  "Sets the name of the CVC executable to run."
+  (interactive (list (read-file-name "CVC binary: "
+				     "" cvc-command nil cvc-command)))
+  (if (stringp arg)
+      (progn
+	(if (string= arg "") nil
+	  (setq cvc-command arg))
+	(setq cvc-options-changed t))
+    (error "Not a string. The value is not set.")))
+
+(defun cvc-trace (arg)
+  "Adds a CVC tracing flag to be given in the +trace command line option."
+  (interactive (list (read-from-minibuffer "Add trace flag: "
+			       cvc-verbose-level)))
+  (if (stringp arg)
+      (progn
+	(if (string= arg "") (error "Empty flag is not allowed")
+	  (setq cvc-trace-flags (add-to-list 'cvc-trace-flags arg)))
+	(setq cvc-options-changed t)
+	(message "%S" cvc-trace-flags))
+    (error "Not a string. The value is not set.")))
+
+(defun cvc-untrace (arg)
+  "Removes a CVC tracing flag given in the +trace command line option."
+  (interactive (list (completing-read "Remove trace flag: "
+				      (mapcar '(lambda (x) (cons x t)) cvc-trace-flags)
+				      nil t)))
+  (if (stringp arg)
+      (progn
+	(if (string= arg "") nil ; don't do anything on empty input
+	  (setq cvc-trace-flags (delete arg cvc-trace-flags)))
+	(setq cvc-options-changed t)
+	(message "%S" cvc-trace-flags))
+    (error "Not a string. The value is not set.")))
+
+(defun cvc-set-command-line-args (arg)
+  "Sets CVC command line options. Don't set -sat and +quiet
+options here, use corresponding special variables for that."
+  (interactive (list (read-from-minibuffer "Other arguments: "
+			       cvc-command-line-args)))
+  (if (stringp arg)
+      (progn 
+	(if (string= arg "") (setq cvc-command-line-args nil)
+	  (setq cvc-command-line-args arg))
+	(setq cvc-options-changed t))
+    (error "Not a string. The value is not set.")))
+
+;;;; Saving file
+(defun cvc-save-buffer ()
+  "Saves CVC file together with options. Prompts the user whether to
+override the *.opt file if the options have changed."
+  (interactive)
+  (let ((opt-file-name 
+	 (let ((match (string-match "\\.cvc$"
+				    (buffer-file-name))))
+	   (if match
+	       (concat (substring (buffer-file-name)
+				  0 match)
+		       ".opt")
+	     (concat (buffer-file-name) ".opt")))))
+    (cond ((and (file-exists-p opt-file-name)
+		cvc-options-changed)
+	     (if (y-or-n-p "Options have changed. Save them?")
+		 (progn
+		   (cvc-save-options)
+		   (setq cvc-options-changed nil))))
+	  (cvc-options-changed 
+	     (cvc-save-options)
+	     (setq cvc-options-changed nil))))
+    (save-buffer))
+
+;;;; Indentation
+
+(defun cvc-previous-line ()
+  "Moves the point to the fisrt non-comment non-blank string before
+the current one and positions the cursor on the first non-blank character."
+  (interactive)
+  (forward-line -1)
+  (beginning-of-line)
+  (skip-chars-forward " \t")
+  (while (and (not (bobp)) (looking-at "$\\|%"))
+    (forward-line -1)
+    (beginning-of-line)
+    (skip-chars-forward " \t")))
+
+(defun cvc-previous-indentation () 
+  "Returns a pair (INDENT . TYPE). INDENT is the indentation of the
+previous string, if there is one, and TYPE is 'openning, 'declaration
+or 'plain, depending on whether previous string starts with an
+openning, declarative keyword or neither. \"Previous string\" means
+the last string before the current that is not an empty string or a
+comment."
+  (if (bobp) '(0 . 'plain)
+    (save-excursion
+      (cvc-previous-line)
+      (let ((type (cond ((looking-at cvc-openning-keywords-regexp) 'openning)
+			((looking-at cvc-declaration-keywords-regexp)
+			 'declaration)
+			(t 'plain)))
+	    (indent (current-indentation)))
+	(cons indent type)))))
+
+(defun cvc-compute-indentation ()
+  "Computes the indentation for the current string based on the
+previous string. Current algorithm is too simple and needs
+improvement."
+  (save-excursion
+   (beginning-of-line)
+   (skip-chars-forward " \t")
+   (cond ((looking-at cvc-declaration-keywords-regexp) 0)
+	 (t (let* ((indent-data (cvc-previous-indentation))
+		   (indent (car indent-data))
+		   (type (cdr indent-data)))
+	      (setq indent
+		    (cond ((looking-at cvc-closing-keywords-regexp) 
+			   (if (< indent 2) 0 (- indent 2)))
+			  ((or (eq type 'openning) (eq type 'declaration))
+			   (+ indent 2))
+			  (t indent)))
+	      indent)))))
+
+(defun cvc-indent-line ()
+  "Indent the current line relative to the previous meaningful line."
+  (interactive)
+  (let* ((initial (point))
+	 (final (let ((case-fold-search nil))(cvc-compute-indentation)))
+	 (offset0 (save-excursion
+		    (beginning-of-line)
+		    (skip-chars-forward " \t")
+		    (- initial (point))))
+	 (offset (if (< offset0 0) 0 offset0)))
+    (indent-line-to final)
+    (goto-char (+ (point) offset))))
+
+;;;; Now define the keymap
+
+(defconst cvc-mode-map nil  "CVC keymap")
+
+(if cvc-mode-map ()
+  (progn
+    (setq cvc-mode-map (make-sparse-keymap))
+    (define-key cvc-mode-map [delete] 'backward-delete-char-untabify)
+    (define-key cvc-mode-map [backspace] 'backward-delete-char-untabify)
+    (define-key cvc-mode-map "\C-x\C-s"  'cvc-save-buffer)
+    (define-key cvc-mode-map "\C-c\C-e"  'cvc-edit-options)
+    (define-key cvc-mode-map "\C-c\C-f"  'cvc-run)
+    (define-key cvc-mode-map "\C-c\C-t"  'cvc-trace)
+    (define-key cvc-mode-map "\C-c\C-u"  'cvc-untrace)
+    (define-key cvc-mode-map "\C-c\C-r"  'cvc-set-command)
+    (define-key cvc-mode-map "\C-c\C-c"  'cvc-interrupt)
+    ;; (define-key cvc-mode-map "\C-c\C-r"  'cvc-send-usr1)
+    ;; (define-key cvc-mode-map "\C-c\C-s"  'cvc-send-usr2)
+    (define-key cvc-mode-map "\C-c;"  'comment-region)
+    (define-key cvc-mode-map "\t"  'cvc-indent-line)))
+
+(defun cvc-make-local-vars ()
+  "Create buffer-local variables for CVC modes"
+  (make-local-variable 'cvc-command)
+  (make-local-variable 'cvc-sat-option)
+  (make-local-variable 'cvc-verbose-level)
+  (make-local-variable 'cvc-trace-flags)
+  (make-local-variable 'cvc-command-line-args)
+  (make-local-variable 'cvc-options-changed)
+  (make-local-variable 'cvc-options-changed))
+
+(defun cvc-mode ()
+  "Major mode for CVC specification files. 
+
+\\{cvc-mode-map}
+
+\\[cvc-run] runs CVC on buffer, \\[cvc-interrupt] interrupts already
+running CVC process.
+
+\\[cvc-send-usr1] and \\[cvc-send-usr2] are used to send UNIX signals
+to CVC process to toggle dynamic variable ordering and force garbage
+collection respectively. Available only for a new (experimental) CVC
+version.
+
+Running CVC (\\[cvc-run]) creates a separate buffer where inferior CVC
+process will leave its output. Currently, each run of CVC clears the
+compilation buffer. If you need to save multiple runs, save them one
+at a time.
+
+Please report bugs to barrett@cs.nyu.edu."
+  (interactive)
+  (use-local-map cvc-mode-map)
+;;; Disable asking for the compile command
+  (make-local-variable 'compilation-read-command)
+  (setq compilation-read-command nil)
+;;; Make all the variables with CVC options local to the current buffer
+  (cvc-make-local-vars)
+  (setq cvc-options-changed nil)
+;;; Change the regexp search to be case sensitive
+;;  (setq case-fold-search nil)
+;;; Set syntax table
+  (set-syntax-table cvc-mode-syntax-table)
+  (make-local-variable 'comment-start)
+;; fix up comment handling
+  (setq comment-start "%")
+  (make-local-variable 'comment-end)
+  (setq comment-end "")
+  (make-local-variable 'comment-start-skip)
+  (setq comment-start-skip "%+\\s-*")
+  (setq require-final-newline t)
+;;; Define the major mode
+  (setq major-mode 'cvc-mode)
+  (setq mode-name "CVC")
+;;; Load command line options for CVC process
+  (let ((opt-file-name 
+	 (let ((match (string-match "\\.cvc$"
+				    (buffer-file-name))))
+	   (if match
+	       (concat (substring (buffer-file-name)
+				  0 match)
+		       ".opt")
+	     (concat (buffer-file-name) ".opt")))))
+    (if (file-exists-p opt-file-name)
+	(load opt-file-name)))
+;;; Do fontification, if necessary
+  (setq font-lock-keywords 
+	(if font-lock-maximum-decoration
+	    cvc-font-lock-keywords-2
+	  cvc-font-lock-keywords-1))
+  (if running-xemacs
+      (put 'cvc-mode 'font-lock-defaults
+	   '(cvc-font-lock-keywords nil nil nil nil))
+    (setq font-lock-defaults '(cvc-font-lock-keywords nil nil nil nil)))
+    (if (and cvc-font-lock-mode-on (or running-xemacs font-lock-global-modes)
+	     window-system)
+	(font-lock-mode 1))
+  (setq mode-line-process nil) ; put 'cvc-status when hooked up to inferior CVC
+  (run-hooks 'cvc-mode-hook))
+
+(defun cvc-options-edit-mode ()
+  "Major mode for editing CVC options. Actually, this is Emacs Lisp
+mode with a few changes. In particular, \\[cvc-save-and-load-options] will save the file, 
+find the associated CVC file and updates its options accordingly.  See
+`\\[describe-bindings]' for key bindings.  "
+  (interactive)
+  (emacs-lisp-mode)
+;;; Make all the variables with CVC options local to the current buffer
+;;; to avoid accidental override of the global values
+  (cvc-make-local-vars)
+  (setq major-mode 'cvc-options-edit-mode)
+  (setq mode-name "CVC Options")
+  (if (and cvc-font-lock-mode-on (or running-xemacs font-lock-global-modes)
+	   window-system)
+      (font-lock-mode t))
+  (use-local-map (copy-keymap (current-local-map)))
+  (local-set-key "\C-c\C-c" 'cvc-save-and-load-options))
+
+(provide 'cvc-mode)
diff --git a/README.emacs b/contrib/editing-with-emacs
index 277424230..277424230 100644
--- a/README.emacs
+++ b/contrib/editing-with-emacs
diff --git a/src/include/theory.h b/src/include/theory.h
index 6659dc680..5c50c7a37 100644
--- a/src/include/theory.h
+++ b/src/include/theory.h
@@ -60,7 +60,7 @@ public:
   /**
    * T-propagate new literal assignments in the current context.
    */
-  // TODO design decisoin: instead of returning a set of literals
+  // TODO design decision: instead of returning a set of literals
   // here, perhaps we have an interface back into the prop engine
   // where we assert directly.  we might sometimes unknowingly assert
   // something clearly inconsistent (esp. in a parallel context).