diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-02-12 20:59:13 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-02-12 20:59:13 +0000 |
commit | 76d8ab99b0a44a318e4bc49bd6203f6464d20d8e (patch) | |
tree | 24b7df3085cbb3376e7b0366000540c134b91c65 /contrib/new-theory | |
parent | a25b07cd09b7723009acf4e95fe6575bac553fff (diff) |
separate new-theory components into a "theoryskel" directory so that new files can be added to it without modifying the script.
Diffstat (limited to 'contrib/new-theory')
-rwxr-xr-x | contrib/new-theory | 269 |
1 files changed, 17 insertions, 252 deletions
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 |