separate new-theory components into a "theoryskel" directory so that new files can be added to it without modifying the script.

10 files changed, 282 insertions, 253 deletions

diff --git a/contrib/Makefile.am b/contrib/Makefile.am
index 66d62f8b8..1439a1117 100644
--- a/contrib/Makefile.am
+++ b/contrib/Makefile.am
@@ -9,4 +9,12 @@ EXTRA_DIST = \
 	addsourcedir \
 	new-theory \
 	configure-in-place \
-	depgraph
+	depgraph \
+	theoryskel/kinds \
+	theoryskel/Makefile \
+	theoryskel/Makefile.am \
+	theoryskel/README.WHATS-NEXT \
+	theoryskel/theory_DIR.cpp \
+	theoryskel/theory_DIR.h \
+	theoryskel/theory_DIR_rewriter.h \
+	theoryskel/theory_DIR_type_rules.h
diff --git a/contrib/new-theory b/contrib/new-theory
index 0045e7b41..7ada1de6c 100755
--- a/contrib/new-theory
+++ b/contrib/new-theory
@@ -53,265 +53,27 @@ if ! mkdir "src/theory/$dir"; then
   exit 1
 fi
 
+echo "Theory of $dir"
 echo "Theory directory: src/theory/$dir"
 echo "Theory id: THEORY_$id"
 echo "Theory class: CVC4::theory::$dir::Theory$camel"
-echo "Theory string: Theory of $dir"
 echo
 
-echo "Creating src/theory/$dir/Makefile..."
-cat > "src/theory/$dir/Makefile" <<EOF
-topdir = ../../..
-srcdir = src/theory/$dir
+function copyskel {
+  src="$1"
+  dest="`echo "$src" | sed "s/DIR/$dir/g"`"
+  echo "Creating src/theory/$dir/$dest..."
+  sed "s/\$dir/$dir/g;s/\$camel/$camel/g;s/\$id/$id/g" \
+    contrib/theoryskel/$src \
+    > "src/theory/$dir/$dest"
+}
 
-include \$(topdir)/Makefile.subdir
-EOF
-
-echo "Creating src/theory/$dir/Makefile.am..."
-cat > "src/theory/$dir/Makefile.am" <<EOF
-AM_CPPFLAGS = \\
-	-D__BUILDING_CVC4LIB \\
-	-I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../..
-AM_CXXFLAGS = -Wall -Wno-unknown-pragmas \$(FLAG_VISIBILITY_HIDDEN)
-
-noinst_LTLIBRARIES = lib$dir.la
-
-lib${dir}_la_SOURCES = \\
-	theory_$dir.h \\
-	theory_$dir.cpp
-
-EXTRA_DIST =
-EOF
-
-echo "Creating src/theory/$dir/kinds..."
-cat > "src/theory/$dir/kinds" <<EOF
-# kinds                                                               -*- sh -*-
-#
-# For documentation on this file format, please refer to
-# src/theory/builtin/kinds.
-#
-
-theory THEORY_$id ::CVC4::theory::$dir::Theory$camel "theory/arith/theory_$dir.h"
-typechecker "theory/$dir/theory_${dir}_type_rules.h"
-rewriter ::CVC4::theory::$dir::${camel}Rewriter "theory/$dir/${dir}_rewriter.h"
-
-properties check
-
-# theory content goes here
-# constants...
-# types...
-# operators...
-
-endtheory
-EOF
-
-echo "Creating src/theory/$dir/theory_${dir}_type_rules.h..."
-cat > "src/theory/$dir/theory_${dir}_type_rules.h" <<EOF
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__${id}__THEORY_${id}_TYPE_RULES_H
-#define __CVC4__THEORY__${id}__THEORY_${id}_TYPE_RULES_H
-
-namespace CVC4 {
-namespace theory {
-namespace $dir {
-
-class ${camel}TypeRule {
-public:
-
-  /**
-   * Compute the type for (and optionally typecheck) a term belonging
-   * to the theory of $dir.
-   *
-   * @param check if true, the node's type should be checked as well
-   * as computed.
-   */
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
-                                     bool check)
-    throw (TypeCheckingExceptionPrivate) {
-    // implement me!
-  }
-
-};/* class ${camel}TypeRule */
-
-}/* CVC4::theory::$dir namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__${id}__THEORY_${id}_TYPE_RULES_H */
-EOF
-
-echo "Creating src/theory/$dir/theory_${dir}_rewriter.h..."
-cat > "src/theory/$dir/theory_${dir}_rewriter.h" <<EOF
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__${id}__THEORY_${id}_REWRITER_H
-#define __CVC4__THEORY__${id}__THEORY_${id}_REWRITER_H
-
-#include "theory/rewriter.h"
-
-namespace CVC4 {
-namespace theory {
-namespace $dir {
-
-class Theory${camel}Rewriter {
-public:
-
-  /**
-   * Rewrite a node into the normal form for the theory of $dir.
-   * Called in post-order (really reverse-topological order) when
-   * traversing the expression DAG during rewriting.  This is the
-   * main function of the rewriter, and because of the ordering,
-   * it can assume its children are all rewritten already.
-   *
-   * This function can return one of three rewrite response codes
-   * along with the rewritten node:
-   *
-   *   REWRITE_DONE indicates that no more rewriting is needed.
-   *   REWRITE_AGAIN means that the top-level expression should be
-   *     rewritten again, but that its children are in final form.
-   *   REWRITE_AGAIN_FULL means that the entire returned expression
-   *     should be rewritten again (top-down with preRewrite(), then
-   *     bottom-up with postRewrite()).
-   *
-   * Even if this function returns REWRITE_DONE, if the returned
-   * expression belongs to a different theory, it will be fully
-   * rewritten by that theory's rewriter.
-   */
-  static RewriteResponse postRewrite(TNode node) {
-
-    // Implement me!
-
-    // This default implementation
-    return RewriteResponse(REWRITE_DONE, node);
-  }
-
-  /**
-   * Rewrite a node into the normal form for the theory of $dir
-   * in pre-order (really topological order)---meaning that the
-   * children may not be in the normal form.  This is an optimization
-   * for theories with cancelling terms (e.g., 0 * (big-nasty-expression)
-   * in arithmetic rewrites to 0 without the need to look at the big
-   * nasty expression).  Since it's only an optimization, the
-   * implementation here can do nothing.
-   */
-  static RewriteResponse preRewrite(TNode node) {
-    // do nothing
-    return RewriteResponse(REWRITE_DONE, node);
-  }
-
-  /**
-   * Rewrite an equality, in case special handling is required.
-   */
-  static Node rewriteEquality(TNode equality) {
-    // often this will suffice
-    return postRewrite(equality).node;
-  }
-
-  /**
-   * Initialize the rewriter.
-   */
-  static inline void init() {
-    // nothing to do
-  }
-
-  /**
-   * Shut down the rewriter.
-   */
-  static inline void shutdown() {
-    // nothing to do
-  }
-
-};/* class Theory${camel}Rewriter */
-
-}/* CVC4::theory::$dir namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__${id}__THEORY_${id}_REWRITER_H */
-EOF
-
-echo "Creating src/theory/$dir/theory_${dir}.h..."
-cat > "src/theory/$dir/theory_$dir.h" <<EOF
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__${id}__THEORY_${id}_H
-#define __CVC4__THEORY__${id}__THEORY_${id}_H
-
-#include "theory/theory.h"
-
-namespace CVC4 {
-namespace theory {
-namespace $dir {
-
-class Theory$camel : public Theory {
-public:
-
-  /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
-  Theory$camel(context::Context* c,
-               context::UserContext* u,
-               OutputChannel& out,
-               Valuation valuation);
-
-  void check(Effort);
-
-  std::string identify() const {
-    return "THEORY_$id";
-  }
-
-};/* class Theory$camel */
-
-}/* CVC4::theory::$dir namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__${id}__THEORY_${id}_H */
-EOF
-
-echo "Creating src/theory/$dir/theory_${dir}.cpp..."
-cat > "src/theory/$dir/theory_$dir.cpp" <<EOF
-#include "theory/$dir/theory_$dir.h"
-
-using namespace std;
-
-namespace CVC4 {
-namespace theory {
-namespace $dir {
-
-/** Constructs a new instance of Theory$camel w.r.t. the provided contexts. */
-Theory$camel::Theory$camel(context::Context* c,
-                           context::UserContext* u,
-                           OutputChannel& out,
-                           Valuation valuation) :
-  Theory(THEORY_UF, c, u, out, valuation) {
-}/* Theory$camel::Theory$camel() */
-
-void Theory$camel::check(Effort level) {
-
-  while(!done()) {
-    // Get all the assertions
-    Assertion assertion = get();
-    TNode fact = assertion.assertion;
-
-    Debug("$dir") << "Theory$camel::check(): processing " << fact << std::endl;
-
-    // Do the work
-    switch(fact.getKind()) {
-
-    /* cases for all the theory's kinds go here... */
-
-    default:
-      Unimplemented(fact.getKind());
-    }
-  }
-
-}/* Theory$camel::check() */
-
-}/* CVC4::theory::$dir namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-EOF
+# copy files from the skeleton, with proper replacements
+for file in `ls contrib/theoryskel`; do
+  copyskel "$file"
+done
 
+echo
 echo "Adding $dir to src/theory/Makefile.am..."
 if grep -q '^SUBDIRS = .*[^a-zA-Z0-9_]'"$dir"'\([^a-zA-Z0-9_]\|$\)' src/theory/Makefile.am &>/dev/null; then
   echo "NOTE: src/theory/Makefile.am already descends into dir $dir"
@@ -327,3 +89,6 @@ else
   fi
 fi
 
+echo
+echo "Rerunning autogen.sh..."
+./autogen.sh
diff --git a/contrib/theoryskel/Makefile b/contrib/theoryskel/Makefile
new file mode 100644
index 000000000..2aeda0cf8
--- /dev/null
+++ b/contrib/theoryskel/Makefile
@@ -0,0 +1,4 @@
+topdir = ../../..
+srcdir = src/theory/$dir
+
+include $(topdir)/Makefile.subdir
diff --git a/contrib/theoryskel/Makefile.am b/contrib/theoryskel/Makefile.am
new file mode 100644
index 000000000..d6b41ac03
--- /dev/null
+++ b/contrib/theoryskel/Makefile.am
@@ -0,0 +1,15 @@
+AM_CPPFLAGS = \
+	-D__BUILDING_CVC4LIB \
+	-I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../..
+AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
+
+noinst_LTLIBRARIES = lib$dir.la
+
+lib$dir_la_SOURCES = \
+	theory_$dir.h \
+	theory_$dir.cpp \
+	theory_$dir_rewriter.h \
+	theory_$dir_type_rules.h
+
+EXTRA_DIST = \
+	kinds
diff --git a/contrib/theoryskel/README.WHATS-NEXT b/contrib/theoryskel/README.WHATS-NEXT
new file mode 100644
index 000000000..ce07eafb9
--- /dev/null
+++ b/contrib/theoryskel/README.WHATS-NEXT
@@ -0,0 +1,22 @@
+Congratulations, you now have a new theory of $dir !
+
+Your next steps will likely be:
+
+* to specify theory constants, types, and operators in your \`kinds' file
+* to add typing rules to theory_${dir}_type_rules.h for your operators
+  and constants
+* to write code in theory_${dir}_rewriter.h to implement a normal form
+  for your theory's terms
+* to write parser rules in src/parser/cvc/Cvc.g to support the CVC input
+  language, src/parser/smt/Smt.g to support the (deprecated) SMT-LIBv1
+  language, and src/parser/smt2/Smt2.g to support SMT-LIBv2
+* to write printer code in src/printer/*/*_printer* to support printing
+  your theory terms and types in various output languages
+
+and finally:
+
+* to implement a decision procedure for your theory by implementing
+  Theory$camel::check() in theory_$dir.cpp
+
+Good luck, and please contact cvc4-devel@cs.nyu.edu for assistance
+should you need it!
diff --git a/contrib/theoryskel/kinds b/contrib/theoryskel/kinds
new file mode 100644
index 000000000..23e90c19a
--- /dev/null
+++ b/contrib/theoryskel/kinds
@@ -0,0 +1,21 @@
+# kinds                                                               -*- sh -*-
+#
+# For documentation on this file format, please refer to
+# src/theory/builtin/kinds.
+#
+
+theory THEORY_$id ::CVC4::theory::$dir::Theory$camel "theory/$dir/theory_$dir.h"
+typechecker "theory/$dir/theory_$dir_type_rules.h"
+rewriter ::CVC4::theory::$dir::Theory$camelRewriter "theory/$dir/theory_$dir_rewriter.h"
+
+properties check
+
+# Theory content goes here.
+
+# constants...
+
+# types...
+
+# operators...
+
+endtheory
diff --git a/contrib/theoryskel/theory_DIR.cpp b/contrib/theoryskel/theory_DIR.cpp
new file mode 100644
index 000000000..4d24f3e16
--- /dev/null
+++ b/contrib/theoryskel/theory_DIR.cpp
@@ -0,0 +1,40 @@
+#include "theory/$dir/theory_$dir.h"
+
+using namespace std;
+
+namespace CVC4 {
+namespace theory {
+namespace $dir {
+
+/** Constructs a new instance of Theory$camel w.r.t. the provided contexts. */
+Theory$camel::Theory$camel(context::Context* c,
+                           context::UserContext* u,
+                           OutputChannel& out,
+                           Valuation valuation) :
+  Theory(THEORY_UF, c, u, out, valuation) {
+}/* Theory$camel::Theory$camel() */
+
+void Theory$camel::check(Effort level) {
+
+  while(!done()) {
+    // Get all the assertions
+    Assertion assertion = get();
+    TNode fact = assertion.assertion;
+
+    Debug("$dir") << "Theory$camel::check(): processing " << fact << std::endl;
+
+    // Do the work
+    switch(fact.getKind()) {
+
+    /* cases for all the theory's kinds go here... */
+
+    default:
+      Unhandled(fact.getKind());
+    }
+  }
+
+}/* Theory$camel::check() */
+
+}/* CVC4::theory::$dir namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/contrib/theoryskel/theory_DIR.h b/contrib/theoryskel/theory_DIR.h
new file mode 100644
index 000000000..ed36193f7
--- /dev/null
+++ b/contrib/theoryskel/theory_DIR.h
@@ -0,0 +1,33 @@
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__$id__THEORY_$id_H
+#define __CVC4__THEORY__$id__THEORY_$id_H
+
+#include "theory/theory.h"
+
+namespace CVC4 {
+namespace theory {
+namespace $dir {
+
+class Theory$camel : public Theory {
+public:
+
+  /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
+  Theory$camel(context::Context* c,
+               context::UserContext* u,
+               OutputChannel& out,
+               Valuation valuation);
+
+  void check(Effort);
+
+  std::string identify() const {
+    return "THEORY_$id";
+  }
+
+};/* class Theory$camel */
+
+}/* CVC4::theory::$dir namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__$id__THEORY_$id_H */
diff --git a/contrib/theoryskel/theory_DIR_rewriter.h b/contrib/theoryskel/theory_DIR_rewriter.h
new file mode 100644
index 000000000..16859bc23
--- /dev/null
+++ b/contrib/theoryskel/theory_DIR_rewriter.h
@@ -0,0 +1,86 @@
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__$id__THEORY_$id_REWRITER_H
+#define __CVC4__THEORY__$id__THEORY_$id_REWRITER_H
+
+#include "theory/rewriter.h"
+
+namespace CVC4 {
+namespace theory {
+namespace $dir {
+
+class Theory$camelRewriter {
+public:
+
+  /**
+   * Rewrite a node into the normal form for the theory of $dir.
+   * Called in post-order (really reverse-topological order) when
+   * traversing the expression DAG during rewriting.  This is the
+   * main function of the rewriter, and because of the ordering,
+   * it can assume its children are all rewritten already.
+   *
+   * This function can return one of three rewrite response codes
+   * along with the rewritten node:
+   *
+   *   REWRITE_DONE indicates that no more rewriting is needed.
+   *   REWRITE_AGAIN means that the top-level expression should be
+   *     rewritten again, but that its children are in final form.
+   *   REWRITE_AGAIN_FULL means that the entire returned expression
+   *     should be rewritten again (top-down with preRewrite(), then
+   *     bottom-up with postRewrite()).
+   *
+   * Even if this function returns REWRITE_DONE, if the returned
+   * expression belongs to a different theory, it will be fully
+   * rewritten by that theory's rewriter.
+   */
+  static RewriteResponse postRewrite(TNode node) {
+
+    // Implement me!
+
+    // This default implementation
+    return RewriteResponse(REWRITE_DONE, node);
+  }
+
+  /**
+   * Rewrite a node into the normal form for the theory of $dir
+   * in pre-order (really topological order)---meaning that the
+   * children may not be in the normal form.  This is an optimization
+   * for theories with cancelling terms (e.g., 0 * (big-nasty-expression)
+   * in arithmetic rewrites to 0 without the need to look at the big
+   * nasty expression).  Since it's only an optimization, the
+   * implementation here can do nothing.
+   */
+  static RewriteResponse preRewrite(TNode node) {
+    // do nothing
+    return RewriteResponse(REWRITE_DONE, node);
+  }
+
+  /**
+   * Rewrite an equality, in case special handling is required.
+   */
+  static Node rewriteEquality(TNode equality) {
+    // often this will suffice
+    return postRewrite(equality).node;
+  }
+
+  /**
+   * Initialize the rewriter.
+   */
+  static inline void init() {
+    // nothing to do
+  }
+
+  /**
+   * Shut down the rewriter.
+   */
+  static inline void shutdown() {
+    // nothing to do
+  }
+
+};/* class Theory$camelRewriter */
+
+}/* CVC4::theory::$dir namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__$id__THEORY_$id_REWRITER_H */
diff --git a/contrib/theoryskel/theory_DIR_type_rules.h b/contrib/theoryskel/theory_DIR_type_rules.h
new file mode 100644
index 000000000..29be55686
--- /dev/null
+++ b/contrib/theoryskel/theory_DIR_type_rules.h
@@ -0,0 +1,35 @@
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__$id__THEORY_$id_TYPE_RULES_H
+#define __CVC4__THEORY__$id__THEORY_$id_TYPE_RULES_H
+
+namespace CVC4 {
+namespace theory {
+namespace $dir {
+
+class $camelTypeRule {
+public:
+
+  /**
+   * Compute the type for (and optionally typecheck) a term belonging
+   * to the theory of $dir.
+   *
+   * @param check if true, the node's type should be checked as well
+   * as computed.
+   */
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
+                                     bool check)
+    throw (TypeCheckingExceptionPrivate) {
+
+    // TODO: implement me!
+    Unimplemented();
+
+  }
+
+};/* class $camelTypeRule */
+
+}/* CVC4::theory::$dir namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__$id__THEORY_$id_TYPE_RULES_H */