diff options
| -rw-r--r-- | src/CMakeLists.txt | 7 | ||||
| -rw-r--r-- | src/cvc4.i | 1 | ||||
| -rw-r--r-- | src/expr/expr_template.h | 2 | ||||
| -rw-r--r-- | src/expr/kind_template.cpp | 37 | ||||
| -rw-r--r-- | src/expr/kind_template.h | 32 | ||||
| -rwxr-xr-x | src/expr/mkkind | 14 | ||||
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 3 | ||||
| -rwxr-xr-x | src/theory/mktheorytraits | 5 | ||||
| -rw-r--r-- | src/theory/theory.h | 1 | ||||
| -rw-r--r-- | src/theory/theory_engine.cpp | 28 | ||||
| -rw-r--r-- | src/theory/theory_id.cpp | 56 | ||||
| -rw-r--r-- | src/theory/theory_id.h | 46 | ||||
| -rw-r--r-- | src/theory/theory_id.i | 5 | ||||
| -rw-r--r-- | src/theory/theory_traits_template.h | 4 |
14 files changed, 164 insertions, 77 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 0a6dec216..a24a2e31a 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -682,6 +682,8 @@ libcvc4_add_sources( theory/theory.h theory/theory_engine.cpp theory/theory_engine.h + theory/theory_id.cpp + theory/theory_id.h theory/theory_model.cpp theory/theory_model.h theory/theory_model_builder.cpp @@ -717,10 +719,6 @@ include_directories(include) include_directories(. ${CMAKE_CURRENT_BINARY_DIR}) #-----------------------------------------------------------------------------# -# IMPORTANT: The order of the theories is important. It affects the order in -# which theory solvers are called/initialized internally. For example, strings -# depends on arith, quantifiers needs to come as the very last. -# See issue https://github.com/CVC4/CVC4/issues/2517 for more details. set(KINDS_FILES ${PROJECT_SOURCE_DIR}/src/theory/builtin/kinds @@ -928,6 +926,7 @@ install(FILES ${INCLUDE_INSTALL_DIR}/cvc4/smt_util) install(FILES theory/logic_info.h + theory/theory_id.h DESTINATION ${INCLUDE_INSTALL_DIR}/cvc4/theory) install(FILES diff --git a/src/cvc4.i b/src/cvc4.i index 166514bc9..69041b277 100644 --- a/src/cvc4.i +++ b/src/cvc4.i @@ -357,6 +357,7 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters; %include "smt/command.i" %include "smt/logic_exception.i" %include "theory/logic_info.i" +%include "theory/theory_id.i" // Tim: This should come after "theory/logic_info.i". %include "smt/smt_engine.i" diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 2c52e5b72..4ca22459b 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -621,7 +621,7 @@ private: ${getConst_instantiations} -#line 616 "${template}" +#line 609 "${template}" inline size_t ExprHashFunction::operator()(CVC4::Expr e) const { return (size_t) e.getId(); diff --git a/src/expr/kind_template.cpp b/src/expr/kind_template.cpp index e1a933e7b..d325d24b4 100644 --- a/src/expr/kind_template.cpp +++ b/src/expr/kind_template.cpp @@ -74,48 +74,29 @@ ${type_constant_descriptions} namespace theory { -std::ostream& operator<<(std::ostream& out, TheoryId theoryId) { - switch(theoryId) { -${theory_descriptions} -#line 81 "${template}" - default: - out << "UNKNOWN_THEORY"; - break; - } - return out; -} - TheoryId kindToTheoryId(::CVC4::Kind k) { switch(k) { case kind::UNDEFINED_KIND: case kind::NULL_EXPR: break; ${kind_to_theory_id} -#line 95 "${template}" +#line 84 "${template}" case kind::LAST_KIND: break; } throw IllegalArgumentException("", "k", __PRETTY_FUNCTION__, "bad kind"); } -TheoryId typeConstantToTheoryId(::CVC4::TypeConstant typeConstant) { - switch(typeConstant) { +TheoryId typeConstantToTheoryId(::CVC4::TypeConstant typeConstant) +{ + switch (typeConstant) + { ${type_constant_to_theory_id} -#line 105 "${template}" - case LAST_TYPE: - break; - } - throw IllegalArgumentException("", "k", __PRETTY_FUNCTION__, "bad type constant"); -} - -std::string getStatsPrefix(TheoryId theoryId) { - switch(theoryId) { -${theory_stats_prefixes} -#line 115 "${template}" - default: - break; +#line 94 "${template}" + case LAST_TYPE: break; } - return "unknown"; + throw IllegalArgumentException( + "", "k", __PRETTY_FUNCTION__, "bad type constant"); } }/* CVC4::theory namespace */ diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h index 93c37f6cc..0168363d4 100644 --- a/src/expr/kind_template.h +++ b/src/expr/kind_template.h @@ -22,6 +22,7 @@ #include <iosfwd> #include "base/exception.h" +#include "theory/theory_id.h" namespace CVC4 { namespace kind { @@ -44,7 +45,7 @@ namespace kind { std::ostream& operator<<(std::ostream&, CVC4::Kind) CVC4_PUBLIC; -#line 48 "${template}" +#line 49 "${template}" /** Returns true if the given kind is associative. This is used by ExprManager to * decide whether it's safe to modify big expressions by changing the grouping of @@ -64,11 +65,12 @@ struct KindHashFunction { /** * The enumeration for the built-in atomic types. */ -enum CVC4_PUBLIC TypeConstant { -${type_constant_list} -#line 70 "${template}" +enum CVC4_PUBLIC TypeConstant +{ + ${type_constant_list} +#line 71 "${template}" LAST_TYPE -};/* enum TypeConstant */ +}; /* enum TypeConstant */ /** * We hash the constants with their values. @@ -83,23 +85,9 @@ std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant); namespace theory { -enum TheoryId { -${theory_enum} -#line 89 "${template}" - THEORY_LAST -};/* enum TheoryId */ - -const TheoryId THEORY_FIRST = static_cast<TheoryId>(0); -const TheoryId THEORY_SAT_SOLVER = THEORY_LAST; - -CVC4_PUBLIC inline TheoryId& operator++(TheoryId& id) { - return id = static_cast<TheoryId>(static_cast<int>(id) + 1); -} - -std::ostream& operator<<(std::ostream& out, TheoryId theoryId); -TheoryId kindToTheoryId(::CVC4::Kind k) CVC4_PUBLIC; -TheoryId typeConstantToTheoryId(::CVC4::TypeConstant typeConstant) CVC4_PUBLIC; -std::string getStatsPrefix(TheoryId theoryId) CVC4_PUBLIC; +::CVC4::theory::TheoryId kindToTheoryId(::CVC4::Kind k) CVC4_PUBLIC; +::CVC4::theory::TheoryId typeConstantToTheoryId( + ::CVC4::TypeConstant typeConstant) CVC4_PUBLIC; }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/expr/mkkind b/src/expr/mkkind index 5e5be7c45..a8a74b5a6 100755 --- a/src/expr/mkkind +++ b/src/expr/mkkind @@ -73,9 +73,6 @@ type_properties_includes= seen_theory=false seen_theory_builtin=false -theory_enum= -theory_descriptions= -theory_stats_prefixes= function theory { # theory ID T header @@ -88,7 +85,7 @@ function theory { fi # this script doesn't care about the theory class information, but - # makes does make sure it's there + # makes sure it's there seen_theory=true if [ "$1" = THEORY_BUILTIN ]; then if $seen_theory_builtin; then @@ -106,13 +103,7 @@ function theory { fi theory_id="$1" - theory_enum="${theory_enum} $1, -" - theory_descriptions="${theory_descriptions} case ${theory_id}: out << \"${theory_id}\"; break; -" prefix=$(echo "$theory_id" | tr '[:upper:]' '[:lower:]') - theory_stats_prefixes="${theory_stats_prefixes} case ${theory_id}: return \"theory::${prefix#theory_}\"; break; -" } function alternate { @@ -408,7 +399,6 @@ for var in \ kind_decls \ kind_printers \ kind_to_theory_id \ - theory_enum \ type_constant_list \ type_constant_descriptions \ type_constant_to_theory_id \ @@ -419,8 +409,6 @@ for var in \ type_groundterms \ type_constant_groundterms \ type_properties_includes \ - theory_descriptions \ - theory_stats_prefixes \ template \ ; do eval text="\${text//\\\$\\{$var\\}/\${$var}}" diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index ffda05d1a..47ac2a11b 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -837,7 +837,8 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) addTheory(THEORY_SEP); } - Command* cmd = new SetBenchmarkLogicCommand(sygus() ? d_logic.getLogicString() : name); + Command* cmd = + new SetBenchmarkLogicCommand(sygus() ? d_logic.getLogicString() : name); cmd->setMuted(!fromCommand); return cmd; } /* Smt2::setLogic() */ diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits index 456a4b0ea..8a900e1e7 100755 --- a/src/theory/mktheorytraits +++ b/src/theory/mktheorytraits @@ -41,8 +41,6 @@ template=$1; shift theory_traits= theory_includes= theory_constructors= -theory_for_each_macro="#define CVC4_FOR_EACH_THEORY \\ -" type_enumerator_includes= mk_type_enumerator_cases= @@ -105,8 +103,6 @@ function theory { theory_header="$3" theory_includes="${theory_includes}#include \"$theory_header\" " - theory_for_each_macro="${theory_for_each_macro} CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::${theory_id}) \\ -" } function alternate { @@ -412,7 +408,6 @@ nl -ba -s' ' "$template" | grep '^ *[0-9][0-9]* # *line' | text=$(cat "$template") for var in \ theory_traits \ - theory_for_each_macro \ theory_includes \ theory_constructors \ template \ diff --git a/src/theory/theory.h b/src/theory/theory.h index b5cc16fc8..f6f1de69c 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -42,6 +42,7 @@ #include "theory/decision_manager.h" #include "theory/logic_info.h" #include "theory/output_channel.h" +#include "theory/theory_id.h" #include "theory/valuation.h" #include "util/statistics_registry.h" diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 5d185ad9d..ac3c63d55 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -59,6 +59,34 @@ using namespace CVC4::theory; namespace CVC4 { +/* -------------------------------------------------------------------------- */ + +namespace theory { + +/** + * IMPORTANT: The order of the theories is important. For example, strings + * depends on arith, quantifiers needs to come as the very last. + * Do not change this order. + */ + +#define CVC4_FOR_EACH_THEORY \ + CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_BUILTIN) \ + CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_BOOL) \ + CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_UF) \ + CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_ARITH) \ + CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_BV) \ + CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_FP) \ + CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_ARRAYS) \ + CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_DATATYPES) \ + CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_SEP) \ + CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_SETS) \ + CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_STRINGS) \ + CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_QUANTIFIERS) + +} // namespace theory + +/* -------------------------------------------------------------------------- */ + inline void flattenAnd(Node n, std::vector<TNode>& out){ Assert(n.getKind() == kind::AND); for(Node::iterator i=n.begin(), i_end=n.end(); i != i_end; ++i){ diff --git a/src/theory/theory_id.cpp b/src/theory/theory_id.cpp new file mode 100644 index 000000000..260bec418 --- /dev/null +++ b/src/theory/theory_id.cpp @@ -0,0 +1,56 @@ +#include "theory/theory_id.h" + +namespace CVC4 { +namespace theory { + +TheoryId& operator++(TheoryId& id) +{ + return id = static_cast<TheoryId>(static_cast<int>(id) + 1); +} + +std::ostream& operator<<(std::ostream& out, TheoryId theoryId) +{ + switch (theoryId) + { + case THEORY_BUILTIN: out << "THEORY_BUILTIN"; break; + case THEORY_BOOL: out << "THEORY_BOOL"; break; + case THEORY_UF: out << "THEORY_UF"; break; + case THEORY_ARITH: out << "THEORY_ARITH"; break; + case THEORY_BV: out << "THEORY_BV"; break; + case THEORY_FP: out << "THEORY_FP"; break; + case THEORY_ARRAYS: out << "THEORY_ARRAYS"; break; + case THEORY_DATATYPES: out << "THEORY_DATATYPES"; break; + case THEORY_SEP: out << "THEORY_SEP"; break; + case THEORY_SETS: out << "THEORY_SETS"; break; + case THEORY_STRINGS: out << "THEORY_STRINGS"; break; + case THEORY_QUANTIFIERS: out << "THEORY_QUANTIFIERS"; break; + + default: out << "UNKNOWN_THEORY"; break; + } + return out; +} + +std::string getStatsPrefix(TheoryId theoryId) +{ + switch (theoryId) + { + case THEORY_BUILTIN: return "theory::builtin"; break; + case THEORY_BOOL: return "theory::bool"; break; + case THEORY_UF: return "theory::uf"; break; + case THEORY_ARITH: return "theory::arith"; break; + case THEORY_BV: return "theory::bv"; break; + case THEORY_FP: return "theory::fp"; break; + case THEORY_ARRAYS: return "theory::arrays"; break; + case THEORY_DATATYPES: return "theory::datatypes"; break; + case THEORY_SEP: return "theory::sep"; break; + case THEORY_SETS: return "theory::sets"; break; + case THEORY_STRINGS: return "theory::strings"; break; + case THEORY_QUANTIFIERS: return "theory::quantifiers"; break; + + default: break; + } + return "unknown"; +} + +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/theory_id.h b/src/theory/theory_id.h new file mode 100644 index 000000000..7ca5916fa --- /dev/null +++ b/src/theory/theory_id.h @@ -0,0 +1,46 @@ +#include "cvc4_public.h" + +#ifndef CVC4__THEORY__THEORY_ID_H +#define CVC4__THEORY__THEORY_ID_H + +#include <iostream> + +namespace CVC4 { + +namespace theory { + +/** + * IMPORTANT: The order of the theories is important. For example, strings + * depends on arith, quantifiers needs to come as the very last. + * Do not change this order. + */ +enum TheoryId +{ + THEORY_BUILTIN, + THEORY_BOOL, + THEORY_UF, + THEORY_ARITH, + THEORY_BV, + THEORY_FP, + THEORY_ARRAYS, + THEORY_DATATYPES, + THEORY_SEP, + THEORY_SETS, + THEORY_STRINGS, + THEORY_QUANTIFIERS, + + THEORY_LAST +}; + +const TheoryId THEORY_FIRST = static_cast<TheoryId>(0); +const TheoryId THEORY_SAT_SOLVER = THEORY_LAST; + +TheoryId& operator++(TheoryId& id) CVC4_PUBLIC; + +std::ostream& operator<<(std::ostream& out, TheoryId theoryId); + +std::string getStatsPrefix(TheoryId theoryId) CVC4_PUBLIC; + +} // namespace theory +} // namespace CVC4 +#endif diff --git a/src/theory/theory_id.i b/src/theory/theory_id.i new file mode 100644 index 000000000..afe01d7b2 --- /dev/null +++ b/src/theory/theory_id.i @@ -0,0 +1,5 @@ +%{ +#include "theory/theory_id.h" +%} + +%include "theory/theory_id.h" diff --git a/src/theory/theory_traits_template.h b/src/theory/theory_traits_template.h index 00ad7656d..564864f19 100644 --- a/src/theory/theory_traits_template.h +++ b/src/theory/theory_traits_template.h @@ -34,9 +34,7 @@ struct TheoryTraits; ${theory_traits} -${theory_for_each_macro} - -#line 40 "${template}" +#line 38 "${template}" struct TheoryConstructor { static void addTheory(TheoryEngine* engine, TheoryId id) { |