From 5b5474281c4cdc880bff8b9e38b84dc84f88e50c Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 9 Nov 2009 21:47:30 +0000 Subject: [PATCH] minor fixes, added contrib directory --- DESIGN_QUESTIONS | 16 +- Makefile.am | 2 +- configure.ac | 1 + contrib/Makefile.am | 1 + contrib/README | 4 + contrib/cvc-devel.el | 218 +++++++ contrib/cvc-mode.el | 715 +++++++++++++++++++++ README.emacs => contrib/editing-with-emacs | 0 src/include/theory.h | 2 +- 9 files changed, 956 insertions(+), 3 deletions(-) create mode 100644 contrib/Makefile.am create mode 100644 contrib/README create mode 100644 contrib/cvc-devel.el create mode 100644 contrib/cvc-mode.el rename README.emacs => contrib/editing-with-emacs (100%) 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 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 +;;;; * +;;;; *
+;;;; * +;;;; * 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. +;;;; * +;;;; *
+;;;; * +;;;; */ + +;;;; 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\\>" "<=" ">=" "!=" "=" "\\[" "\\]" + "\\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 similarity index 100% rename from README.emacs rename to 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). -- 2.30.2