parser and core support for SMT-LIBv2 commands get-info, set-option, get-option, get-assertions, get-value, define-sort, define-fun, and declare-sort with arity > 0; SmtEngine doesn't yet support most of these, but will shortly...

7 files changed, 18 insertions, 8 deletions

diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index 07d48b1f6..5cd4719b1 100644
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -1,7 +1,7 @@
 # kinds                                                               -*- sh -*-
 #
 # For documentation on this file format, please refer to
-# src/expr/builtin_kinds.
+# src/theory/builtin/kinds.
 #
 
 theory ::CVC4::theory::arith::TheoryArith "theory_arith.h"
diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds
index 68daa8cb5..4ad9c7463 100644
--- a/src/theory/arrays/kinds
+++ b/src/theory/arrays/kinds
@@ -1,7 +1,7 @@
 # kinds                                                               -*- sh -*-
 #
 # For documentation on this file format, please refer to
-# src/expr/builtin_kinds.
+# src/theory/builtin/kinds.
 #
 
 theory ::CVC4::theory::arrays::TheoryArrays "theory_arrays.h"
diff --git a/src/theory/booleans/kinds b/src/theory/booleans/kinds
index 43c37f4b7..ac6b05881 100644
--- a/src/theory/booleans/kinds
+++ b/src/theory/booleans/kinds
@@ -1,7 +1,7 @@
 # kinds                                                               -*- sh -*-
 #
 # For documentation on this file format, please refer to
-# src/expr/builtin_kinds.
+# src/theory/builtin/kinds.
 #
 
 theory ::CVC4::theory::booleans::TheoryBool "theory_bool.h"
diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds
index 54f861b76..cc6fe0c20 100644
--- a/src/theory/bv/kinds
+++ b/src/theory/bv/kinds
@@ -1,7 +1,7 @@
 # kinds                                                               -*- sh -*-
 #
 # For documentation on this file format, please refer to
-# src/expr/builtin_kinds.
+# src/theory/builtin/kinds.
 #
 
 theory ::CVC4::theory::bv::TheoryBV "theory_bv.h"
diff --git a/src/theory/interrupted.h b/src/theory/interrupted.h
index 616d3da74..d8a54b1e4 100644
--- a/src/theory/interrupted.h
+++ b/src/theory/interrupted.h
@@ -11,9 +11,19 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief The theory output channel interface.
+ ** \brief An exception signaling that a Theory should immediately
+ ** stop performing processing
  **
- ** The theory output channel interface.
+ ** An exception signaling that a Theory should immediately stop
+ ** performing processing and relinquish control to its caller (e.g.,
+ ** in a parallel environment).  A Theory might be interrupted if it
+ ** calls into its CVC4::theory::OutputChannel, and it should only
+ ** catch this exception to perform emergency repair of any invariants
+ ** it must re-establish.  Further, if this exception is caught by a
+ ** Theory, the Theory should rethrow the same exception (via "throw;"
+ ** in the exception block) rather than return, as the Interrupted
+ ** instance might contain additional information needed for the
+ ** proper management of CVC4 components.
  **/
 
 #include "cvc4_private.h"
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index fb2fde589..cdc1e1cc2 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -11,7 +11,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief The theory output channel interface.
+ ** \brief The theory output channel interface
  **
  ** The theory output channel interface.
  **/
diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds
index 4bfba382c..13cd5e91b 100644
--- a/src/theory/uf/kinds
+++ b/src/theory/uf/kinds
@@ -1,7 +1,7 @@
 # kinds                                                               -*- sh -*-
 #
 # For documentation on this file format, please refer to
-# src/expr/builtin_kinds.
+# src/theory/builtin/kinds.
 #
 
 theory ::CVC4::theory::uf::TheoryUF "theory_uf.h"