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/theoryskel | |
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/theoryskel')
-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 |
8 files changed, 256 insertions, 0 deletions
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 */ |