diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-02-10 23:36:07 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-02-10 23:36:07 +0000 |
commit | 008b88abd1d1c2a4b44053bad71654fbade787b2 (patch) | |
tree | 8c4ee41079c3f1bf36422a5b5e68535d572b4d95 | |
parent | 91ab0391fe69419726448d634f8050c105035232 (diff) |
script to ease creating a new theory from scratch (will go along with new reference documentation)
-rw-r--r-- | contrib/Makefile.am | 2 | ||||
-rwxr-xr-x | contrib/new-theory | 329 |
2 files changed, 331 insertions, 0 deletions
diff --git a/contrib/Makefile.am b/contrib/Makefile.am index 42e3b6f9f..66d62f8b8 100644 --- a/contrib/Makefile.am +++ b/contrib/Makefile.am @@ -6,5 +6,7 @@ EXTRA_DIST = \ cvc-mode.el \ editing-with-emacs \ luby.c \ + addsourcedir \ + new-theory \ configure-in-place \ depgraph diff --git a/contrib/new-theory b/contrib/new-theory new file mode 100755 index 000000000..6488eaec9 --- /dev/null +++ b/contrib/new-theory @@ -0,0 +1,329 @@ +#!/bin/sh +# +# usage: new-theory theory-directory-name +# + +cd "`dirname "$0"`/.." + +if [ ! -e src/theory/theory_engine.h ]; then + echo "ERROR: This script doesn't appear to be the contrib/ subdirectory" >&2 + echo "ERROR: of the CVC4 source tree." >&2 + exit 1 +fi + +if [ $# -ne 1 ]; then + echo "usage: new-theory theory-directory-name" >&2 + echo "e.g.: new-theory arith" >&2 + echo "e.g.: new-theory arrays" >&2 + echo "e.g.: new-theory sets" >&2 + echo >&2 + echo "This tool will create a new src/theory/<theory-directory-name>" >&2 + echo "directory and fill in some infrastructural files in that directory." >&2 + echo "It also will incorporate that directory into the build process." >&2 + echo "Please refer to the file README.WHATS-NEXT file created in that" >&2 + echo "directory for tips on what to do next." + exit 1 +fi + +dir="$1" + +if [ -e "src/theory/$dir" ]; then + echo "ERROR: Theory \"$dir\" already exists." >&2 + echo "ERROR: Please choose a new directory name (or move that one aside)." >&2 + exit 1 +fi + +if ! expr "$dir" : '[a-zA-Z][a-zA-Z0-9_]*$' &>/dev/null || + expr "$dir" : '_$' &>/dev/null; then + echo "ERROR: \"$dir\" is not a valid theory name." >&2 + echo "ERROR:" >&2 + echo "ERROR: Theory names must start with a letter and be composed of" >&2 + echo "ERROR: letters, numbers, and the underscore (_) character; an" >&2 + echo "ERROR: underscore cannot be the final character." >&2 + exit 1 +fi + +id="`echo "$dir" | tr a-z A-Z`" +# convoluted, but should be relatively portable and give a CamelCase +# representation for a string. (e.g. "foo_bar" becomes "FooBar") +camel="`echo "$dir" | awk 'BEGIN { RS="_";ORS="";OFS="" } // {print toupper(substr($1,1,1)),substr($1,2,length($1))} END {print "\n"}'`" + +if ! mkdir "src/theory/$dir"; then + echo "ERROR: encountered an error creating directory src/theory/$dir" >&2 + exit 1 +fi + +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 + +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 + +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" +else + awk '/^SUBDIRS = / {print $0,"'"$dir"'"} !/^SUBDIRS = / {print$0}' src/theory/Makefile.am > src/theory/Makefile.am.new-theory + if ! cp -f src/theory/Makefile.am src/theory/Makefile.am~; then + echo "ERROR: cannot copy src/theory/Makefile.am !" >&2 + exit 1 + fi + if ! mv -f src/theory/Makefile.am.new-theory src/theory/Makefile.am; then + echo "ERROR: cannot replace src/theory/Makefile.am !" >&2 + exit 1 + fi +fi + |