From 76d8ab99b0a44a318e4bc49bd6203f6464d20d8e Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Sun, 12 Feb 2012 20:59:13 +0000 Subject: [PATCH] separate new-theory components into a "theoryskel" directory so that new files can be added to it without modifying the script. --- configure.ac | 2 +- contrib/Makefile.am | 10 +- contrib/new-theory | 269 ++------------------- contrib/theoryskel/Makefile | 4 + contrib/theoryskel/Makefile.am | 15 ++ contrib/theoryskel/README.WHATS-NEXT | 22 ++ contrib/theoryskel/kinds | 21 ++ contrib/theoryskel/theory_DIR.cpp | 40 +++ contrib/theoryskel/theory_DIR.h | 33 +++ contrib/theoryskel/theory_DIR_rewriter.h | 86 +++++++ contrib/theoryskel/theory_DIR_type_rules.h | 35 +++ 11 files changed, 283 insertions(+), 254 deletions(-) create mode 100644 contrib/theoryskel/Makefile create mode 100644 contrib/theoryskel/Makefile.am create mode 100644 contrib/theoryskel/README.WHATS-NEXT create mode 100644 contrib/theoryskel/kinds create mode 100644 contrib/theoryskel/theory_DIR.cpp create mode 100644 contrib/theoryskel/theory_DIR.h create mode 100644 contrib/theoryskel/theory_DIR_rewriter.h create mode 100644 contrib/theoryskel/theory_DIR_type_rules.h diff --git a/configure.ac b/configure.ac index 729544391..a36a38636 100644 --- a/configure.ac +++ b/configure.ac @@ -998,7 +998,7 @@ AC_SUBST(MAN_DATE) AC_CONFIG_FILES([ Makefile.builds Makefile] - m4_esyscmd([find contrib src test examples -name Makefile.am | sort | sed 's,\.am$,,']) + m4_esyscmd([find contrib src test examples -name Makefile.am | grep -v '^contrib/theoryskel/' | sort | sed 's,\.am$,,']) ) CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/rational.h]) 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" < "src/theory/$dir/$dest" +} -include \$(topdir)/Makefile.subdir -EOF - -echo "Creating src/theory/$dir/Makefile.am..." -cat > "src/theory/$dir/Makefile.am" < "src/theory/$dir/kinds" < "src/theory/$dir/theory_${dir}_type_rules.h" < "src/theory/$dir/theory_${dir}_rewriter.h" < "src/theory/$dir/theory_$dir.h" < "src/theory/$dir/theory_$dir.cpp" </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 */ -- 2.30.2