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 | |
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')
-rw-r--r-- | contrib/Makefile.am | 10 | ||||
-rwxr-xr-x | contrib/new-theory | 269 | ||||
-rw-r--r-- | contrib/theoryskel/Makefile | 4 | ||||
-rw-r--r-- | contrib/theoryskel/Makefile.am | 15 | ||||
-rw-r--r-- | contrib/theoryskel/README.WHATS-NEXT | 22 | ||||
-rw-r--r-- | contrib/theoryskel/kinds | 21 | ||||
-rw-r--r-- | contrib/theoryskel/theory_DIR.cpp | 40 | ||||
-rw-r--r-- | contrib/theoryskel/theory_DIR.h | 33 | ||||
-rw-r--r-- | contrib/theoryskel/theory_DIR_rewriter.h | 86 | ||||
-rw-r--r-- | contrib/theoryskel/theory_DIR_type_rules.h | 35 |
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 */ |