* This is a feature that Dejan and I want for the upcoming tutorial.
It allows rapid prototyping of new decision procedure implementations
(which we may choose to demonstrate), and a new --use-theory command-line
option to select from different available implementations. It has no
affect on the current set of theories, as no "alternates" are defined.
* Also update the new-theory script, which was broken and incomplete.
AC_CONFIG_FILES([
Makefile.builds
Makefile]
- m4_esyscmd([find contrib src test examples -name Makefile.am | grep -v '^contrib/theoryskel/' | sort | sed 's,\.am$,,'])
+ m4_esyscmd([find contrib src test examples -name Makefile.am | grep -v '^contrib/theoryskel/' | grep -v '^contrib/alttheoryskel/' | sort | sed 's,\.am$,,'])
)
if test $cvc4_has_threads = yes; then
theoryskel/theory_DIR.h \
theoryskel/theory_DIR_rewriter.h \
theoryskel/theory_DIR_type_rules.h
+ alttheoryskel/kinds \
+ alttheoryskel/Makefile \
+ alttheoryskel/Makefile.am \
+ alttheoryskel/README.WHATS-NEXT \
+ alttheoryskel/theory_DIR.cpp \
+ alttheoryskel/theory_DIR.h
--- /dev/null
+topdir = ../../..
+srcdir = src/theory/$dir
+
+include $(topdir)/Makefile.subdir
--- /dev/null
+AM_CPPFLAGS = \
+ -D__BUILDING_CVC4LIB \
+ -I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/../..
+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 = \
+ kinds \
+ options_handlers.h
--- /dev/null
+Congratulations, you now have a new theory of $dir !
+
+Your next steps will likely be:
+
+* to implement a decision procedure for your theory by implementing
+ Theory$camel::check() in theory_$dir.cpp. Before writing the actual
+ code, you will need :
+
+ * to determine which data structures are context dependent and use for
+ them context-dependent data structures (context/cd*.h)
+ * to choose which work will be done at QUICK_CHECK, STANDARD or at
+ FULL_EFFORT.
+
+You'll probably find the Developer's wiki useful:
+
+ http://cvc4.cs.nyu.edu/wiki/
+
+...and in particular the Developer's Guide:
+
+ http://cvc4.cs.nyu.edu/wiki/Developer%27s_Guide
+
+which contains coding guidelines for the CVC4 project.
+
+Good luck, and please contact cvc4-devel@cs.nyu.edu for assistance
+should you need it!
--- /dev/null
+# kinds -*- sh -*-
+#
+# For documentation on this file format, please refer to
+# src/theory/builtin/kinds.
+#
+
+alternate THEORY_$alt_id "$dir" ::CVC4::theory::$dir::Theory$camel "theory/$dir/theory_$dir.h"
+
--- /dev/null
+#
+# Option specification file for CVC4
+# See src/options/base_options for a description of this file format
+#
+
+module $id "theory/$dir/options.h" $camel
+
+endmodule
--- /dev/null
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__$id__OPTIONS_HANDLERS_H
+#define __CVC4__THEORY__$id__OPTIONS_HANDLERS_H
+
+namespace CVC4 {
+namespace theory {
+namespace $dir {
+
+}/* CVC4::theory::$dir namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__$id__OPTIONS_HANDLERS_H */
--- /dev/null
+#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,
+ const LogicInfo& logicInfo,
+ QuantifiersEngine* qe) :
+ Theory(THEORY_$alt_id, c, u, out, valuation, logicInfo, qe) {
+}/* 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 */
--- /dev/null
+#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 Theory$camel w.r.t. the provided contexts. */
+ Theory$camel(context::Context* c,
+ context::UserContext* u,
+ OutputChannel& out,
+ Valuation valuation,
+ const LogicInfo& logicInfo,
+ QuantifiersEngine* qe);
+
+ 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 */
#!/bin/bash
#
-# usage: new-theory theory-directory-name
+# usage: new-theory [--alternate existing-theory] new-theory-dir-name
#
cd "`dirname "$0"`/.."
exit 1
fi
+if [ $# -ge 1 -a "$1" = --alternate ]; then
+ shift
+ alternate=true
+ alttheory="$1"
+ shift
+else
+ alternate=false
+fi
+
if [ $# -ne 1 ]; then
- echo "usage: new-theory theory-directory-name" >&2
- echo "e.g.: new-theory arith" >&2
+ echo "usage: new-theory [--alternate existing-theory] new-theory-dir-name" >&2
echo "e.g.: new-theory arrays" >&2
echo "e.g.: new-theory sets" >&2
echo "e.g.: new-theory rewrite_rules" >&2
+ echo "e.g.: new-theory --alternate arith difference-logic" >&2
echo >&2
- echo "This tool will create a new src/theory/<theory-directory-name>" >&2
+ echo "This tool will create a new src/theory/<new-theory-dir-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."
- echo
+ echo "directory for tips on what to do next." >&2
+ echo >&2
echo "Theories with multiple words (e.g. \"rewrite_rules\") should have" >&2
echo "directories and namespaces separated by an underscore (_). The" >&2
echo "resulting class names created by this script will be in CamelCase" >&2
echo "(e.g. RewriteRules) if that convention is followed." >&2
+ echo >&2
+ echo "With --alternate, create a new theory directory that is declared as" >&2
+ echo "an alternate implementation of an existing host theory. Such" >&2
+ echo "\"alternates\" share preprocessing, typechecking, rewriting (i.e.," >&2
+ echo "normal form), and expression kinds with their host theories, but" >&2
+ echo "differ in decision procedure implementation. They are selectable" >&2
+ echo "at runtime with --use-theory." >&2
exit 1
fi
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
+ echo "ERROR: Or, if you'd like to create an alternate implementation of" >&2
+ echo "ERROR: $dir, use this program this way:" >&2
+ echo "ERROR: new-theory --alternate $dir new-implementation-name" >&2
exit 1
fi
exit 1
fi
+if $alternate; then
+ if ! [ -d "src/theory/$alttheory" -a -f "src/theory/$alttheory/kinds" ]; then
+ echo "ERROR: Theory \"$alttheory\" doesn't exist, or cannot read its kinds file." >&2
+ exit 1
+ fi
+ alt_id="$(
+ function theory() { echo $1 | sed 's,^THEORY_,,'; exit; }
+ source "src/theory/$alttheory/kinds"
+ )"
+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")
echo "Theory of $dir"
echo "Theory directory: src/theory/$dir"
echo "Theory id: THEORY_$id"
+$alternate && echo "Alternate for theory id: THEORY_$alt_id"
echo "Theory class: CVC4::theory::$dir::Theory$camel"
echo
> "src/theory/$dir/$dest"
}
+function copyaltskel {
+ 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;s/\$alt_id/$alt_id/g" \
+ contrib/alttheoryskel/$src \
+ > "src/theory/$dir/$dest"
+}
+
# copy files from the skeleton, with proper replacements
-for file in `ls contrib/theoryskel`; do
- copyskel "$file"
-done
+if $alternate; then
+ for file in `ls contrib/alttheoryskel`; do
+ copyaltskel "$file"
+ done
+else
+ for file in `ls contrib/theoryskel`; do
+ copyskel "$file"
+ done
+fi
echo
-echo "Adding $dir to SUBDIRS in src/theory/Makefile.am..."
+echo "Adding $dir to SUBDIRS 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
fi
fi
-echo "Adding lib$theory.la to LIBADD in src/theory/Makefile.am..."
+echo "Adding lib$dir.la to LIBADD to src/theory/Makefile.am..."
if grep -q '^ @builddir@/'"$dir"'/lib'"$dir"'\.la\>' src/theory/Makefile.am &>/dev/null; then
- echo "NOTE: src/theory/Makefile.am already seems to include lib$theory.la"
+ echo "NOTE: src/theory/Makefile.am already seems to include lib$dir.la"
else
awk '!/^libtheory_la_LIBADD = / {print$0} /^libtheory_la_LIBADD = / {while(/\\ *$/){print $0;getline} print $0,"\\";print "\t@builddir@/'"$dir"'/lib'"$dir"'.la"}' src/theory/Makefile.am > src/theory/Makefile.am.new-theory
if ! cp -f src/theory/Makefile.am src/theory/Makefile.am~; then
fi
fi
+echo "Adding ../theory/$dir/options.cpp to OPTIONS_FILES_SRCS"
+echo " and nodist_liboptions_la_SOURCES to src/options/Makefile.am..."
+if grep -q '^ \.\./theory/'"$dir"'/options\.cpp\>' src/options/Makefile.am &>/dev/null; then
+ echo "NOTE: src/options/Makefile.am already seems to link to $dir option files"
+else
+ awk '!/^OPTIONS_FILES_SRCS = \\|^nodist_liboptions_la_SOURCES = / {print$0} /^OPTIONS_FILES_SRCS = \\|^nodist_liboptions_la_SOURCES = / {while(/\\ *$/){print $0;getline} print $0,"\\";print "\t../theory/'"$dir"'/options.cpp","\\";print "\t../theory/'"$dir"'/options.h";}' src/options/Makefile.am > src/options/Makefile.am.new-theory
+ if ! cp -f src/options/Makefile.am src/options/Makefile.am~; then
+ echo "ERROR: cannot copy src/options/Makefile.am !" >&2
+ exit 1
+ fi
+ if ! mv -f src/options/Makefile.am.new-theory src/options/Makefile.am; then
+ echo "ERROR: cannot replace src/options/Makefile.am !" >&2
+ exit 1
+ fi
+fi
+
echo
echo "Rerunning autogen.sh..."
./autogen.sh
AM_CPPFLAGS = \
-D__BUILDING_CVC4LIB \
- -I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../..
+ -I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/../..
AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
noinst_LTLIBRARIES = lib$dir.la
theory_$dir_type_rules.h
EXTRA_DIST = \
- kinds
+ kinds \
+ options_handlers.h
Theory$camel::check() in theory_$dir.cpp. Before writing the actual
code, you will need :
- * to determine which datastructures are context dependent and use for them
- context dependent datastructures (context/cd*.h)
+ * to determine which data structures are context dependent and use for
+ them context-dependent data structures (context/cd*.h)
* to choose which work will be done at QUICK_CHECK, STANDARD or at
FULL_EFFORT.
You'll probably find the Developer's wiki useful:
- http://church.cims.nyu.edu/wiki/CVC_Portal
+ http://cvc4.cs.nyu.edu/wiki/
-...and in particular the Deverloper's Guide:
+...and in particular the Developer's Guide:
- http://church.cims.nyu.edu/wiki/Developer%27s_Guide
+ http://cvc4.cs.nyu.edu/wiki/Developer%27s_Guide
which contains coding guidelines for the CVC4 project.
--- /dev/null
+#
+# Option specification file for CVC4
+# See src/options/base_options for a description of this file format
+#
+
+module $id "theory/$dir/options.h" $camel
+
+endmodule
--- /dev/null
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__$id__OPTIONS_HANDLERS_H
+#define __CVC4__THEORY__$id__OPTIONS_HANDLERS_H
+
+namespace CVC4 {
+namespace theory {
+namespace $dir {
+
+}/* CVC4::theory::$dir namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__$id__OPTIONS_HANDLERS_H */
Theory$camel::Theory$camel(context::Context* c,
context::UserContext* u,
OutputChannel& out,
- Valuation valuation) :
- Theory(THEORY_$id, c, u, out, valuation) {
+ Valuation valuation,
+ const LogicInfo& logicInfo,
+ QuantifiersEngine* qe) :
+ Theory(THEORY_$id, c, u, out, valuation, logicInfo, qe) {
}/* Theory$camel::Theory$camel() */
void Theory$camel::check(Effort level) {
class Theory$camel : public Theory {
public:
- /** Constructs a new instance of Theory$camel w.r.t. the provided context.*/
+ /** Constructs a new instance of Theory$camel w.r.t. the provided contexts. */
Theory$camel(context::Context* c,
context::UserContext* u,
OutputChannel& out,
- Valuation valuation);
+ Valuation valuation,
+ const LogicInfo& logicInfo,
+ QuantifiersEngine* qe);
void check(Effort);
}/* CVC4::kind::metakind namespace */
}/* CVC4::kind namespace */
+
+#line 330 "${template}"
+
+namespace theory {
+
+static inline bool useTheoryValidate(std::string theory) {
+${use_theory_validations}
+ return false;
+}
+
+static const char *const useTheoryHelp = "\
+The following options are valid alternate implementations for use with\n\
+the --use-theory option:\n\
+\n\
+${theory_alternate_doc}";
+
+}/* CVC4::theory namespace */
}/* CVC4 namespace */
#endif /* __CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP */
seen_theory_builtin=false
function theory {
- # theory T header
+ # theory ID T header
lineno=${BASH_LINENO[0]}
+ if $seen_theory; then
+ echo "$kf:$lineno: error: multiple theories defined in one file !?" >&2
+ exit 1
+ fi
+
# this script doesn't care about the theory class information, but
# makes does make sure it's there
seen_theory=true
fi
}
+function alternate {
+ # alternate ID name T header
+
+ lineno=${BASH_LINENO[0]}
+
+ if $seen_theory; then
+ echo "$kf:$lineno: error: multiple theories defined in one file !?" >&2
+ exit 1
+ fi
+
+ seen_theory=true
+ seen_endtheory=true
+}
+
function rewriter {
# rewriter class header
lineno=${BASH_LINENO[0]}
theory_descriptions=
function theory {
- # theory T header
+ # theory ID T header
lineno=${BASH_LINENO[0]}
+ if $seen_theory; then
+ echo "$kf:$lineno: error: multiple theories defined in one file !?" >&2
+ exit 1
+ fi
+
# this script doesn't care about the theory class information, but
# makes does make sure it's there
seen_theory=true
"
}
+function alternate {
+ # alternate ID name T header
+
+ lineno=${BASH_LINENO[0]}
+
+ if $seen_theory; then
+ echo "$kf:$lineno: error: multiple theories defined in one file !?" >&2
+ exit 1
+ fi
+
+ seen_theory=true
+ seen_endtheory=true
+}
+
function properties {
# rewriter class header
lineno=${BASH_LINENO[0]}
metakind_lbchildren=
metakind_operatorKinds=
+use_theory_validations=
+theory_alternate_doc=
+
seen_theory=false
seen_theory_builtin=false
function theory {
- # theory T header
+ # theory ID T header
lineno=${BASH_LINENO[0]}
+ if $seen_theory; then
+ echo "$kf:$lineno: error: multiple theories defined in one file !?" >&2
+ exit 1
+ fi
+
# this script doesn't care about the theory class information, but
# makes does make sure it's there
seen_theory=true
// #include \"theory/$b/$2\""
}
+function alternate {
+ # alternate ID name T header
+
+ lineno=${BASH_LINENO[0]}
+
+ if $seen_theory; then
+ echo "$kf:$lineno: error: multiple theories defined in one file !?" >&2
+ exit 1
+ fi
+
+ seen_theory=true
+ seen_endtheory=true
+
+ theory_id="$1"
+ name="$2"
+ theory_class="$3"
+ theory_header="$4"
+ theory_includes="${theory_includes}#include \"$theory_header\"
+"
+
+ use_theory_validations="${use_theory_validations}
+ if(theory == \"$name\") {
+ return true;
+ }"
+ theory_alternate_doc="$theory_alternate_doc$name - alternate implementation for $theory_id\\n\\
+"
+}
+
function properties {
# properties prop*
lineno=${BASH_LINENO[0]}
nl -ba -s' ' "$template" | grep '^ *[0-9][0-9]* # *line' |
awk '{OFS="";if($1+1!=$3) print "'"$template"':",$1,": warning: incorrect annotation \"#line ",$3,"\" (it should be \"#line ",($1+1),"\")"}' >&2
+if [ -z "$theory_alternate_doc" ]; then
+ theory_alternate_doc="[none defined]"
+fi
+
text=$(cat "$template")
for var in \
metakind_includes \
metakind_ubchildren \
metakind_lbchildren \
metakind_operatorKinds \
+ use_theory_validations \
+ theory_alternate_doc \
template \
; do
eval text="\${text//\\\$\\{$var\\}/\${$var}}"
d_theoryEngine = new TheoryEngine(d_context, d_userContext, d_private->d_iteRemover, const_cast<const LogicInfo&>(d_logic));
// Add the theories
-#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
-#undef CVC4_FOR_EACH_THEORY_STATEMENT
-#endif
-#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
- d_theoryEngine->addTheory<TheoryTraits<THEORY>::theory_class>(THEORY);
- CVC4_FOR_EACH_THEORY;
+ for(TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
+ TheoryConstructor::addTheory(d_theoryEngine, id);
+ }
// global push/pop around everything, to ensure proper destruction
// of context-dependent data structures
seen_theory_builtin=false
function theory {
- # theory T header
+ # theory ID T header
lineno=${BASH_LINENO[0]}
if $seen_theory; then
- echo "$kf:$lineno: theory declaration can only appear once" >&2
- exit 1;
+ echo "$kf:$lineno: error: multiple theories defined in one file !?" >&2
+ exit 1
fi
# this script doesn't care about the theory class information, but
theory_id="$1"
}
+function alternate {
+ # alternate ID name T header
+
+ lineno=${BASH_LINENO[0]}
+
+ if $seen_theory; then
+ echo "$kf:$lineno: error: multiple theories defined in one file !?" >&2
+ exit 1
+ fi
+
+ seen_theory=true
+ seen_endtheory=true
+}
+
function properties {
# properties prop*
lineno=${BASH_LINENO[0]}
theory_traits=
theory_includes=
+theory_constructors=
theory_for_each_macro="#define CVC4_FOR_EACH_THEORY \\
"
seen_theory_builtin=false
function theory {
- # theory T header
+ # theory ID T header
lineno=${BASH_LINENO[0]}
if $seen_theory; then
- echo "$kf:$lineno: theory declaration can only appear once" >&2
- exit 1;
+ echo "$kf:$lineno: error: multiple theories defined in one file !?" >&2
+ exit 1
fi
# this script doesn't care about the theory class information, but
"
}
+function alternate {
+ # alternate ID name T header
+
+ lineno=${BASH_LINENO[0]}
+
+ if $seen_theory; then
+ echo "$kf:$lineno: error: multiple theories defined in one file !?" >&2
+ exit 1
+ fi
+
+ seen_theory=true
+ seen_endtheory=true
+
+ theory_header="$4"
+ theory_includes="${theory_includes}#include \"$theory_header\"
+"
+
+ eval "alternate_for_$1=\"\${alternate_for_$1}
+ if(options::theoryAlternates()[\\\"$2\\\"]) {
+ engine->addTheory< $3 >($1);
+ return;
+ }\""
+}
+
function rewriter {
# rewriter class header
lineno=${BASH_LINENO[0]}
seen_endtheory=true
+ theory_constructors="${theory_constructors}
+ case $theory_id:
+\$alternate_for_$theory_id
+ engine->addTheory< $theory_class >($theory_id);
+ return;
+"
+
theory_traits="${theory_traits}
template<>
struct TheoryTraits<${theory_id}> {
- typedef ${theory_class} theory_class;
+ // typedef ${theory_class} theory_class;
typedef ${rewriter_class} rewriter_class;
static const bool isStableInfinite = ${theory_stable_infinite};
## output
+eval "theory_constructors=\"$theory_constructors\""
+
# generate warnings about incorrect #line annotations in templates
nl -ba -s' ' "$template" | grep '^ *[0-9][0-9]* # *line' |
awk '{OFS="";if($1+1!=$3) print "'"$template"':",$1,": warning: incorrect annotation \"#line ",$3,"\" (it should be \"#line ",($1+1),"\")"}' >&2
theory_traits \
theory_for_each_macro \
theory_includes \
+ theory_constructors \
template \
type_enumerator_includes \
mk_type_enumerator_type_constant_cases \
expert-option theoryOfMode --theoryof-mode=MODE CVC4::theory::TheoryOfMode :handler CVC4::theory::stringToTheoryOfMode :handler-include "theory/options_handlers.h" :default CVC4::theory::THEORY_OF_TYPE_BASED :include "theory/theoryof_mode.h"
mode for theoryof
+option - use-theory --use-theory=NAME argument :handler CVC4::theory::useTheory :handler-include "theory/options_handlers.h"
+ use alternate theory implementation NAME (--use-theory=help for a list)
+option theoryAlternates ::std::map<std::string,bool> :include <map> :read-write
+
endmodule
#ifndef __CVC4__THEORY__OPTIONS_HANDLERS_H
#define __CVC4__THEORY__OPTIONS_HANDLERS_H
+#include "expr/metakind.h"
+
namespace CVC4 {
namespace theory {
}
}
+inline void useTheory(std::string option, std::string optarg, SmtEngine* smt) {
+ if(optarg == "help") {
+ puts(useTheoryHelp);
+ exit(1);
+ }
+ if(useTheoryValidate(optarg)) {
+ std::map<std::string, bool> m = options::theoryAlternates();
+ m[optarg] = true;
+ options::theoryAlternates.set(m);
+ } else {
+ throw OptionException(std::string("unknown option for ") + option + ": `" +
+ optarg + "'. Try --use-theory help.");
+ }
+}
+
}/* CVC4::theory namespace */
}/* CVC4 namespace */
#include "cvc4_private.h"
#include "theory/theory.h"
+#include "theory/options.h"
${theory_includes}
${theory_for_each_macro}
+#line 39 "${template}"
+
+struct TheoryConstructor {
+ static void addTheory(TheoryEngine* engine, TheoryId id) {
+ switch(id) {
+
+${theory_constructors}
+
+ default:
+ Unhandled(id);
+ }
+ }
+};/* struct CVC4::theory::TheoryConstructor */
+
}/* CVC4::theory namespace */
}/* CVC4 namespace */
projects / cvc5.git / commitdiff