path: root/contrib/new-theory

#!/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