diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/Makefile.am | 12 | ||||
-rw-r--r-- | src/theory/arith/kinds | 9 | ||||
-rw-r--r-- | src/theory/arrays/kinds | 8 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 6 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays_type_rules.h | 15 | ||||
-rw-r--r-- | src/theory/booleans/kinds | 4 | ||||
-rw-r--r-- | src/theory/booleans/theory_bool.h | 9 | ||||
-rw-r--r-- | src/theory/builtin/kinds | 114 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin_type_rules.h | 33 | ||||
-rw-r--r-- | src/theory/bv/kinds | 8 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 4 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_type_rules.h | 14 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 4 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.h | 4 | ||||
-rwxr-xr-x | src/theory/mkrewriter | 70 | ||||
-rwxr-xr-x | src/theory/mktheorytraits | 89 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 73 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 31 | ||||
-rw-r--r-- | src/theory/theory_test_utils.h | 14 | ||||
-rw-r--r-- | src/theory/theory_traits_template.h | 8 | ||||
-rw-r--r-- | src/theory/uf/kinds | 13 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.h | 9 |
22 files changed, 444 insertions, 107 deletions
diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index 0d680f4c9..eecf95875 100644 --- a/src/theory/Makefile.am +++ b/src/theory/Makefile.am @@ -71,3 +71,15 @@ theory_traits.h: theory_traits_template.h mktheorytraits @top_builddir@/src/theo $< \ `cat @top_builddir@/src/theory/.subdirs` \ > $@) || (rm -f $@ && exit 1) + +AM_V_CHECK = $(am__v_CHECK_$(V)) +am__v_CHECK_ = $(am__v_CHECK_$(AM_DEFAULT_VERBOSITY)) +am__v_CHECK_0 = @echo " CHECK " $@; + +.PHONY: theory-properties +theory-properties: + $(AM_V_CHECK)@srcdir@/mktheorytraits \ + theory_traits_template.h \ + `cat @top_builddir@/src/theory/.subdirs` \ + > /dev/null +all-local check-local: theory-properties diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index 9e2e3a3a7..a0fc71ab4 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -6,7 +6,8 @@ theory THEORY_ARITH ::CVC4::theory::arith::TheoryArith "theory/arith/theory_arith.h" -properties stable-infinite check propagate staticLearning presolve +properties stable-infinite +properties check propagate staticLearning presolve notifyRestart rewriter ::CVC4::theory::arith::ArithRewriter "theory/arith/arith_rewriter.h" @@ -17,8 +18,8 @@ operator MINUS 2 "arithmetic binary subtraction operator" operator UMINUS 1 "arithmetic unary negation" operator DIVISION 2 "arithmetic division" -sort REAL_TYPE "Real type" -sort INTEGER_TYPE "Integer type" +sort REAL_TYPE Cardinality::REALS "Real type" +sort INTEGER_TYPE Cardinality::INTEGERS "Integer type" constant CONST_RATIONAL \ ::CVC4::Rational \ @@ -37,4 +38,4 @@ operator LEQ 2 "less than or equal, x <= y" operator GT 2 "greater than, x > y" operator GEQ 2 "greater than or equal, x >= y" -endtheory
\ No newline at end of file +endtheory diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds index 7738f50ca..533145dc2 100644 --- a/src/theory/arrays/kinds +++ b/src/theory/arrays/kinds @@ -6,11 +6,15 @@ theory THEORY_ARRAY ::CVC4::theory::arrays::TheoryArrays "theory/arrays/theory_arrays.h" -properties polite stable-infinite +properties polite stable-infinite +properties check rewriter ::CVC4::theory::arrays::TheoryArraysRewriter "theory/arrays/theory_arrays_rewriter.h" operator ARRAY_TYPE 2 "array type" +cardinality ARRAY_TYPE \ + "::CVC4::theory::arrays::CardinalityComputer::computeCardinality(%TYPE%)" \ + "theory/arrays/theory_arrays_type_rules.h" # select a i is a[i] operator SELECT 2 "array select" @@ -18,4 +22,4 @@ operator SELECT 2 "array select" # store a i e is a[i] <= e operator STORE 3 "array store" -endtheory
\ No newline at end of file +endtheory diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 64fdd8303..fbbda9e44 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -34,14 +34,14 @@ public: TheoryArrays(context::Context* c, OutputChannel& out, Valuation valuation); ~TheoryArrays(); void preRegisterTerm(TNode n) { } - void registerTerm(TNode n) { } + //void registerTerm(TNode n) { } - void presolve() { } + //void presolve() { } void addSharedTerm(TNode t); void notifyEq(TNode lhs, TNode rhs); void check(Effort e); - void propagate(Effort e) { } + //void propagate(Effort e) { } void explain(TNode n) { } Node getValue(TNode n); void shutdown() { } diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h index 11e8a8443..bd3c8ad67 100644 --- a/src/theory/arrays/theory_arrays_type_rules.h +++ b/src/theory/arrays/theory_arrays_type_rules.h @@ -11,9 +11,9 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief Theory of arrays. + ** \brief Typing and cardinality rules for the theory of arrays ** - ** Theory of arrays. + ** Typing and cardinality rules for the theory of arrays. **/ #include "cvc4_private.h" @@ -65,6 +65,17 @@ struct ArrayStoreTypeRule { } };/* struct ArrayStoreTypeRule */ +struct CardinalityComputer { + inline static Cardinality computeCardinality(TypeNode type) { + Assert(type.getKind() == kind::ARRAY_TYPE); + + Cardinality indexCard = type[0].getCardinality(); + Cardinality valueCard = type[1].getCardinality(); + + return valueCard ^ indexCard; + } +};/* struct CardinalityComputer */ + }/* CVC4::theory::arrays namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/booleans/kinds b/src/theory/booleans/kinds index 25ca1cfe3..ce7c9111a 100644 --- a/src/theory/booleans/kinds +++ b/src/theory/booleans/kinds @@ -6,11 +6,11 @@ theory THEORY_BOOL ::CVC4::theory::booleans::TheoryBool "theory/booleans/theory_bool.h" -properties finite +properties finite rewriter ::CVC4::theory::booleans::TheoryBoolRewriter "theory/booleans/theory_bool_rewriter.h" -sort BOOLEAN_TYPE "Boolean type" +sort BOOLEAN_TYPE 2 "Boolean type" constant CONST_BOOLEAN \ bool \ diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h index dfcdd22b8..fd6d20e03 100644 --- a/src/theory/booleans/theory_bool.h +++ b/src/theory/booleans/theory_bool.h @@ -34,15 +34,6 @@ public: Theory(THEORY_BOOL, c, out, valuation) { } - void preRegisterTerm(TNode n) { - Debug("bool") << "bool: begin preRegisterTerm(" << n << ")" << std::endl; - Debug("bool") << "bool: end preRegisterTerm(" << n << ")" << std::endl; - } - void registerTerm(TNode n) { - Debug("bool") << "bool: begin preRegisterTerm(" << n << ")" << std::endl; - Debug("bool") << "bool: end preRegisterTerm(" << n << ")" << std::endl; - } - Node getValue(TNode n); std::string identify() const { return std::string("TheoryBool"); } diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index 2831161c3..a170ba145 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -6,12 +6,58 @@ # The first non-blank, non-comment line in this file must be a theory # declaration: # -# theory [builtin] T header +# theory ID T header # -# The special tag "builtin" declares that this is the builtin theory. -# There can be only one and it should be processed first. +# Thereafter, ID is bound to your theory. It becomes part of an +# enumeration that identifies all theories. If your theory has +# several, distinct implementations, they still all share a kinds +# file, a theory ID, all the defined kinds/operators/types for the +# theory, typechecker, etc. They should also share a base class +# (that's the T above). The header is the header for this base +# class. # -# There are four basic commands for declaring kinds: +# The very end of this file should end with: +# +# endtheory +# +# There are several basic commands: +# +# properties PROPERTIES... +# +# This command declares properties of the theory. It can occur +# more than once, in which case the effect is additive. +# +# The current set of properties and their meanings are: +# +# finite the theory is finite +# stable-infinite the theory is stably infinite +# polite the theory is polite +# +# check the theory supports the check() function +# propagate the theory supports propagate() (and explain()) +# staticLearning the theory supports staticLearning() +# registerTerm the theory supports registerTerm() +# notifyRestart the theory supports notifyRestart() +# presolve the theory supports presolve() +# +# In the case of the "theory-supports-function" properties, you +# need to declare these for your theory or the functions will not +# be called! This is used to speed up the core where functionality +# is not needed. +# +# rewriter T header +# +# This declares a rewriter class T for your theory, declared in +# header. Your rewriter class provides four functions: +# +# static void init(); +# static void shutdown(); +# static RewriteResponse preRewrite(TNode node); +# static RewriteResponse postRewrite(TNode node); +# +# ...BUT please note that init() and shutdown() may be removed in +# future, so if possible, do not rely on them being called (and +# implement them as a no-op). # # variable K ["comment"] # @@ -76,6 +122,54 @@ # For consistency, constants taking a non-void payload should # start with "CONST_", but this is not enforced. # +# sort K cardinality ["comment"] +# +# This creates a kind K that represents a sort (a "type constant"). +# These kinds of types are "atomic" types; if you need to describe +# a complex type that takes type arguments (like arrays), use +# "operator"; if you need to describe one that takes "constant" +# arguments (like bitvectors), use "constant", and if you invent +# one that takes both, you could try "parameterized". In those +# cases, you'll want to provide a cardinality separately for your +# type. +# +# The cardinality argument is a nonnegative number (if the sort is +# finite), or Cardinality::INTEGERS if the sort has the same +# cardinality as the integers, or Cardinality::REALS if the sort +# has the same cardinality as the reals. +# +# For consistency, sorts should end with "_TYPE", but this is not +# enforced. +# +# cardinality K cardinality-computer [header] +# +# This command does not define a kind; the kind K needs to be +# defined by one of the other commands above. This command just +# provides a cardinality for types of kind K. The +# "cardinality-computer" is a C++ expression that will yield a +# Cardinality for the type. In that expression, the sequence of +# characters "%TYPE%" will be rewritten with a variable containing +# a TypeNode of kind K. The optional "header" argument is an +# include file necessary to compile the cardinality-computer +# expression. +# +# If the cardinality need not be computed per-type (i.e., it's the +# same for all types of kind K, but the "sort" gesture above could +# not be used---in which case it doesn't already have a registered +# cardinality), you can simply construct a Cardinality temporary. +# For example: +# +# cardinality MY_TYPE Cardinality(Cardinality::INTEGERS) +# +# If not, you might opt to use a computer; a common place to put it +# is with your type checker: +# +# cardinality MY_TYPE \ +# ::CVC4::theory::foo::TheoryFoo::CardinalityComputer(%TYPE%) \ +# "theory/foo/theory_foo_type_rules.h" +# +# +# # Lines may be broken with a backslash between arguments; for example: # # constant CONST_INT \ @@ -108,12 +202,12 @@ theory THEORY_BUILTIN ::CVC4::theory::builtin::TheoryBuiltin "theory/builtin/theory_builtin.h" -properties stable-infinite +properties stable-infinite # Rewriter responisble for all the terms of the theory rewriter ::CVC4::theory::builtin::TheoryBuiltinRewriter "theory/builtin/theory_builtin_rewriter.h" -sort BUILTIN_OPERATOR_TYPE "Built in type for built in operators" +sort BUILTIN_OPERATOR_TYPE Cardinality::INTEGERS "Built in type for built in operators" # A kind representing "inlined" operators defined with OPERATOR # Conceptually, (EQUAL a b) is actually an (APPLY EQUAL a b), but it's @@ -140,6 +234,12 @@ constant TYPE_CONSTANT \ "expr/kind.h" \ "basic types" operator FUNCTION_TYPE 2: "function type" +cardinality FUNCTION_TYPE \ + "::CVC4::theory::builtin::FunctionCardinality::computeCardinality(%TYPE%)" \ + "theory/builtin/theory_builtin_type_rules.h" operator TUPLE_TYPE 2: "tuple type" +cardinality TUPLE_TYPE \ + "::CVC4::theory::builtin::TupleCardinality::computeCardinality(%TYPE%)" \ + "theory/builtin/theory_builtin_type_rules.h" -endtheory
\ No newline at end of file +endtheory diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 0d313594c..bebfca9ab 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -128,6 +128,39 @@ public: } };/* class TupleTypeRule */ +class FunctionCardinality { +public: + inline static Cardinality computeCardinality(TypeNode type) { + Assert(type.getKind() == kind::FUNCTION_TYPE); + + Cardinality argsCard(1); + // get the largest cardinality of function arguments/return type + for(unsigned i = 0, i_end = type.getNumChildren() - 1; i < i_end; ++i) { + argsCard *= type[i].getCardinality(); + } + + Cardinality valueCard = type[type.getNumChildren() - 1].getCardinality(); + + return valueCard ^ argsCard; + } +};/* class FuctionCardinality */ + +class TupleCardinality { +public: + inline static Cardinality computeCardinality(TypeNode type) { + Assert(type.getKind() == kind::TUPLE_TYPE); + + Cardinality card(1); + for(TypeNode::iterator i = type.begin(), + i_end = type.end(); + i != i_end; + ++i) { + card *= (*i).getCardinality(); + } + + return card; + } +};/* class TupleCardinality */ }/* CVC4::theory::builtin namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index 381e90d47..d10e32ee0 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -6,7 +6,8 @@ theory THEORY_BV ::CVC4::theory::bv::TheoryBV "theory/bv/theory_bv.h" -properties finite check propagate +properties finite +properties check propagate rewriter ::CVC4::theory::bv::TheoryBVRewriter "theory/bv/theory_bv_rewriter.h" @@ -15,6 +16,9 @@ constant BITVECTOR_TYPE \ "::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorSize >" \ "util/bitvector.h" \ "bit-vector type" +cardinality BITVECTOR_TYPE \ + "::CVC4::theory::bv::CardinalityComputer::computeCardinality(%TYPE%)" \ + "theory/bv/theory_bv_type_rules.h" constant CONST_BITVECTOR \ ::CVC4::BitVector \ @@ -95,4 +99,4 @@ parameterized BITVECTOR_SIGN_EXTEND BITVECTOR_SIGN_EXTEND_OP 1 "bit-vector sign- parameterized BITVECTOR_ROTATE_LEFT BITVECTOR_ROTATE_LEFT_OP 1 "bit-vector rotate left" parameterized BITVECTOR_ROTATE_RIGHT BITVECTOR_ROTATE_RIGHT_OP 1 "bit-vector rotate right" -endtheory
\ No newline at end of file +endtheory diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index d65f0388b..748352321 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -113,11 +113,11 @@ public: void preRegisterTerm(TNode n); - void registerTerm(TNode n) { } + //void registerTerm(TNode n) { } void check(Effort e); - void presolve() { } + //void presolve() { } void propagate(Effort e) { } diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h index a27fd351c..613df47f3 100644 --- a/src/theory/bv/theory_bv_type_rules.h +++ b/src/theory/bv/theory_bv_type_rules.h @@ -189,6 +189,20 @@ public: } }; +class CardinalityComputer { +public: + inline static Cardinality computeCardinality(TypeNode type) { + Assert(type.getKind() == kind::BITVECTOR_TYPE); + + unsigned size = type.getConst<BitVectorSize>(); + if(size == 0) { + return 0; + } + Integer i = Integer(2).pow(size); + return i; + } +};/* class CardinalityComputer */ + }/* CVC4::theory::bv namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index e7a559fc6..5e813b125 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -64,10 +64,12 @@ void TheoryDatatypes::checkFiniteWellFounded() { //check well-founded and finite, create distinguished ground terms map<TypeNode, vector<Node> >::iterator it; vector<Node>::iterator itc; + // for each datatype... for( it = d_cons.begin(); it != d_cons.end(); ++it ) { d_distinguishTerms[it->first] = Node::null(); d_finite[it->first] = false; d_wellFounded[it->first] = false; + // for each ctor of that datatype... for( itc = it->second.begin(); itc != it->second.end(); ++itc ) { d_cons_finite[*itc] = false; d_cons_wellFounded[*itc] = false; @@ -76,10 +78,12 @@ void TheoryDatatypes::checkFiniteWellFounded() { bool changed; do{ changed = false; + // for each datatype... for( it = d_cons.begin(); it != d_cons.end(); ++it ) { TypeNode t = it->first; Debug("datatypes-finite") << "Check type " << t << endl; bool typeFinite = true; + // for each ctor of that datatype... for( itc = it->second.begin(); itc != it->second.end(); ++itc ) { Node cn = *itc; TypeNode ct = cn.getType(); diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 7b74bfece..36d1b3311 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -152,15 +152,11 @@ public: addDatatypeDefinitions(type); } } - void registerTerm(TNode n) { } - void presolve(); void addSharedTerm(TNode t); void notifyEq(TNode lhs, TNode rhs); void check(Effort e); - void propagate(Effort e) { } - void explain(TNode n, Effort e) { } Node getValue(TNode n); void shutdown() { } std::string identify() const { return std::string("TheoryDatatypes"); } diff --git a/src/theory/mkrewriter b/src/theory/mkrewriter index a53da2022..78fc39984 100755 --- a/src/theory/mkrewriter +++ b/src/theory/mkrewriter @@ -35,16 +35,16 @@ me=$(basename "$0") template=$1; shift -rewriter_includes= +rewriter_includes= rewrite_init= rewrite_shutdown= -pre_rewrite_calls= -pre_rewrite_get_cache= +pre_rewrite_calls= +pre_rewrite_get_cache= pre_rewrite_set_cache= post_rewrite_calls= -post_rewrite_get_cache= +post_rewrite_get_cache= post_rewrite_set_cache= seen_theory=false @@ -55,6 +55,11 @@ function theory { lineno=${BASH_LINENO[0]} + if $seen_theory; then + echo "$kf:$lineno: theory declaration can only appear once" >&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 @@ -72,8 +77,8 @@ function theory { elif ! expr "$2" : '\(::CVC4::theory::*\)' >/dev/null; then echo "$kf:$lineno: warning: theory class not under ::CVC4::theory namespace" >&2 fi - - theory_id="$1" + + theory_id="$1" } function properties { @@ -86,32 +91,33 @@ function endtheory { # endtheory lineno=${BASH_LINENO[0]} check_theory_seen + seen_endtheory=true } function rewriter { # rewriter class header - class="$1" + class="$1" header="$2" rewriter_includes="${rewriter_includes}#include \"$header\" " rewrite_init="${rewrite_init} ${class}::init(); " - rewrite_shutdown="${rewrite_shutdown} ${class}::shutdown(); + rewrite_shutdown="${rewrite_shutdown} ${class}::shutdown(); " pre_rewrite_calls="${pre_rewrite_calls} case ${theory_id}: return ${class}::preRewrite(node); " - pre_rewrite_get_cache="${pre_rewrite_get_cache} case ${theory_id}: return RewriteAttibute<${theory_id}>::getPreRewriteCache(node); + pre_rewrite_get_cache="${pre_rewrite_get_cache} case ${theory_id}: return RewriteAttibute<${theory_id}>::getPreRewriteCache(node); " - pre_rewrite_set_cache="${pre_rewrite_set_cache} case ${theory_id}: return RewriteAttibute<${theory_id}>::setPreRewriteCache(node, cache); + pre_rewrite_set_cache="${pre_rewrite_set_cache} case ${theory_id}: return RewriteAttibute<${theory_id}>::setPreRewriteCache(node, cache); " post_rewrite_calls="${post_rewrite_calls} case ${theory_id}: return ${class}::postRewrite(node); " - post_rewrite_get_cache="${post_rewrite_get_cache} case ${theory_id}: return RewriteAttibute<${theory_id}>::getPostRewriteCache(node); -" - post_rewrite_set_cache="${post_rewrite_set_cache} case ${theory_id}: return RewriteAttibute<${theory_id}>::setPostRewriteCache(node, cache); + post_rewrite_get_cache="${post_rewrite_get_cache} case ${theory_id}: return RewriteAttibute<${theory_id}>::getPostRewriteCache(node); +" + post_rewrite_set_cache="${post_rewrite_set_cache} case ${theory_id}: return RewriteAttibute<${theory_id}>::setPostRewriteCache(node, cache); " lineno=${BASH_LINENO[0]} @@ -119,7 +125,13 @@ function rewriter { } function sort { - # sort TYPE ["comment"] + # sort TYPE cardinality ["comment"] + lineno=${BASH_LINENO[0]} + check_theory_seen +} + +function cardinality { + # cardinality TYPE cardinality-computer [header] lineno=${BASH_LINENO[0]} check_theory_seen } @@ -149,6 +161,10 @@ function constant { } function check_theory_seen { + if $seen_endtheory; then + echo "$kf:$lineno: error: command after \"endtheory\" declaration (endtheory has to be last)" >&2 + exit 1 + fi if ! $seen_theory; then echo "$kf:$lineno: error: no \"theory\" declaration found (it has to be first)" >&2 exit 1 @@ -164,17 +180,39 @@ function check_builtin_theory_seen { while [ $# -gt 0 ]; do kf=$1 seen_theory=false + seen_endtheory=false b=$(basename $(dirname "$kf")) source "$kf" - check_theory_seen + if ! $seen_theory; then + echo "$kf: error: no theory content found in file!" >&2 + exit 1 + fi + if ! $seen_endtheory; then + echo "$kf:$lineno: error: no \"endtheory\" declaration found (it is required at the end)" >&2 + exit 1 + fi shift done check_builtin_theory_seen ## output +# 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 + text=$(cat "$template") -for var in rewriter_includes pre_rewrite_calls post_rewrite_calls pre_rewrite_get_cache post_rewrite_get_cache pre_rewrite_set_cache post_rewrite_set_cache rewrite_init rewrite_shutdown; do +for var in \ + rewriter_includes \ + pre_rewrite_calls \ + post_rewrite_calls \ + pre_rewrite_get_cache \ + post_rewrite_get_cache \ + pre_rewrite_set_cache \ + post_rewrite_set_cache \ + rewrite_init rewrite_shutdown \ + template \ + ; do eval text="\${text//\\\$\\{$var\\}/\${$var}}" done error=`expr "$text" : '.*\${\([^}]*\)}.*'` diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits index c06770a51..9672fc871 100755 --- a/src/theory/mktheorytraits +++ b/src/theory/mktheorytraits @@ -42,7 +42,9 @@ theory_for_each_macro="#define CVC4_FOR_EACH_THEORY \\ theory_has_check="false" theory_has_propagate="false" -theory_has_static_learning="false" +theory_has_staticLearning="false" +theory_has_registerTerm="false" +theory_has_notifyRestart="false" theory_has_presolve="false" theory_stable_infinite="false" @@ -63,6 +65,11 @@ function theory { lineno=${BASH_LINENO[0]} + if $seen_theory; then + echo "$kf:$lineno: theory declaration can only appear once" >&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 @@ -84,7 +91,8 @@ function theory { theory_id="$1" theory_class="$2" - theory_includes="${theory_includes}#include \"$3\" + 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}) \\ " @@ -107,6 +115,8 @@ function endtheory { lineno=${BASH_LINENO[0]} check_theory_seen + seen_endtheory=true + theory_traits="${theory_traits} template<> struct TheoryTraits<${theory_id}> { @@ -119,14 +129,34 @@ struct TheoryTraits<${theory_id}> { static const bool hasCheck = ${theory_has_check}; static const bool hasPropagate = ${theory_has_propagate}; - static const bool hasStaticLearning = ${theory_has_static_learning}; + static const bool hasStaticLearning = ${theory_has_staticLearning}; + static const bool hasRegisterTerm = ${theory_has_registerTerm}; + static const bool hasNotifyRestart = ${theory_has_staticLearning}; static const bool hasPresolve = ${theory_has_presolve}; }; " + # warnings about theory content and properties + dir="$(dirname "$kf")/../../" + if [ -e "$dir/$theory_header" ]; then + for function in check propagate staticLearning registerTerm notifyRestart presolve; do + if eval "\$theory_has_$function"; then + grep '\<'"$function"' *\((\|;\)' "$dir/$theory_header" | grep -vq '^ */\(/\|\*\)' || + echo "$kf: warning: $theory_class has property \"$function\" in its kinds file but doesn't appear to declare the function" >&2 + else + grep '\<'"$function"' *\((\|;\)' "$dir/$theory_header" | grep -vq '^ */\(/\|\*\)' && + echo "$kf: warning: $theory_class does not have property \"$function\" in its kinds file but appears to declare the function" >&2 + fi + done + else + echo "$me: warning: theory header \"$theory_header\" does not exist or is unreadable" >&2 + fi + theory_has_check="false" theory_has_propagate="false" - theory_has_static_learning="false" + theory_has_staticLearning="false" + theory_has_registerTerm="false" + theory_has_notifyRestart="false" theory_has_presolve="false" theory_stable_infinite="false" @@ -156,18 +186,27 @@ function properties { polite) theory_polite="true";; check) theory_has_check="true";; propagate) theory_has_propagate="true";; - staticLearning) theory_has_static_learning="true";; - presolve) theory_has_presolve="true"; + staticLearning) theory_has_staticLearning="true";; + presolve) theory_has_presolve="true";; + registerTerm) theory_has_registerTerm="true";; + notifyRestart) theory_has_notifyRestart="true";; + *) echo "$kf:$lineno: error: unknown theory property \"$property\"" >&2; exit 1;; esac shift done } function sort { - # sort TYPE ["comment"] + # sort TYPE cardinality ["comment"] + lineno=${BASH_LINENO[0]} + check_theory_seen + register_sort "$1" "$2" "$3" +} + +function cardinality { + # cardinality TYPE cardinality-computer [header] lineno=${BASH_LINENO[0]} check_theory_seen - register_sort "$1" "$2" } function variable { @@ -200,7 +239,8 @@ function constant { function register_sort { id=$1 - comment=$2 + cardinality=$2 + comment=$3 type_constant_to_theory_id="${type_constant_to_theory_id} case $id: return $theory_id; break; " } @@ -214,6 +254,10 @@ function register_kind { } function check_theory_seen { + if $seen_endtheory; then + echo "$kf:$lineno: error: command after \"endtheory\" declaration (endtheory has to be last)" >&2 + exit 1 + fi if ! $seen_theory; then echo "$kf:$lineno: error: no \"theory\" declaration found (it has to be first)" >&2 exit 1 @@ -229,23 +273,34 @@ function check_builtin_theory_seen { while [ $# -gt 0 ]; do kf=$1 seen_theory=false + seen_endtheory=false b=$(basename $(dirname "$kf")) - kind_decls="${kind_decls} - /* from $b */ -" - kind_printers="${kind_printers} - /* from $b */ -" source "$kf" - check_theory_seen + if ! $seen_theory; then + echo "$kf: error: no theory content found in file!" >&2 + exit 1 + fi + if ! $seen_endtheory; then + echo "$kf:$lineno: error: no \"endtheory\" declaration found (it is required at the end)" >&2 + exit 1 + fi shift done check_builtin_theory_seen ## output +# 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 + text=$(cat "$template") -for var in theory_traits theory_for_each_macro theory_includes; do +for var in \ + theory_traits \ + theory_for_each_macro \ + theory_includes \ + template \ + ; do eval text="\${text//\\\$\\{$var\\}/\${$var}}" done error=`expr "$text" : '.*\${\([^}]*\)}.*'` diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index d37916515..b4d6654b1 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -117,7 +117,7 @@ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) { * twice. */ // FIXME when ExprSets are online, use one of those to avoid // duplicates in the above? - // Actually, that doesn't work because you have to make sure + // Actually, that doesn't work because you have to make sure // that the *last* occurrence is the one that gets processed first @CB // This could be a big performance problem though because it requires // traversing a DAG as a tree and that can really blow up @CB @@ -132,6 +132,7 @@ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) { TheoryEngine::TheoryEngine(context::Context* ctxt) : d_propEngine(NULL), d_context(ctxt), + d_activeTheories(0), d_theoryOut(this, ctxt), d_hasShutDown(false), d_incomplete(ctxt, false), @@ -139,6 +140,7 @@ TheoryEngine::TheoryEngine(context::Context* ctxt) : for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++theoryId) { d_theoryTable[theoryId] = NULL; + d_theoryIsActive[theoryId] = false; } Rewriter::init(); @@ -150,7 +152,7 @@ TheoryEngine::~TheoryEngine() { Assert(d_hasShutDown); for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++theoryId) { - if(d_theoryTable[theoryId]) { + if(d_theoryTable[theoryId] != NULL) { delete d_theoryTable[theoryId]; } } @@ -163,7 +165,7 @@ struct preprocess_stack_element { bool children_added; preprocess_stack_element(TNode node) : node(node), children_added(false) {} -}; +};/* struct preprocess_stack_element */ Node TheoryEngine::preprocess(TNode node) { // Make sure the node is type-checked first (some rewrites depend on @@ -198,24 +200,29 @@ void TheoryEngine::preRegister(TNode preprocessed) { if (current.getKind() == kind::EQUAL) { TheoryId theoryLHS = Theory::theoryOf(current[0]); Debug("register") << "preregistering " << current << " with " << theoryLHS << std::endl; + markActive(theoryLHS); d_theoryTable[theoryLHS]->preRegisterTerm(current); // TheoryId theoryRHS = Theory::theoryOf(current[1]); // if (theoryLHS != theoryRHS) { +// markActive(theoryRHS); // d_theoryTable[theoryRHS]->preRegisterTerm(current); // Debug("register") << "preregistering " << current << " with " << theoryRHS << std::endl; // } // TheoryId typeTheory = Theory::theoryOf(current[0].getType()); // if (typeTheory != theoryLHS && typeTheory != theoryRHS) { +// markActive(typeTheory); // d_theoryTable[typeTheory]->preRegisterTerm(current); // Debug("register") << "preregistering " << current << " with " << typeTheory << std::endl; // } } else { TheoryId theory = Theory::theoryOf(current); Debug("register") << "preregistering " << current << " with " << theory << std::endl; + markActive(theory); d_theoryTable[theory]->preRegisterTerm(current); TheoryId typeTheory = Theory::theoryOf(current.getType()); if (theory != typeTheory) { Debug("register") << "preregistering " << current << " with " << typeTheory << std::endl; + markActive(typeTheory); d_theoryTable[typeTheory]->preRegisterTerm(current); } } @@ -248,7 +255,7 @@ bool TheoryEngine::check(theory::Theory::Effort effort) { #undef CVC4_FOR_EACH_THEORY_STATEMENT #endif #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ - if (theory::TheoryTraits<THEORY>::hasCheck) { \ + if (theory::TheoryTraits<THEORY>::hasCheck && d_theoryIsActive[THEORY]) { \ reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->check(effort); \ if (!d_theoryOut.d_conflictNode.get().isNull()) { \ return false; \ @@ -271,7 +278,7 @@ void TheoryEngine::propagate() { #undef CVC4_FOR_EACH_THEORY_STATEMENT #endif #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ - if (theory::TheoryTraits<THEORY>::hasPropagate) { \ + if (theory::TheoryTraits<THEORY>::hasPropagate && d_theoryIsActive[THEORY]) { \ reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->propagate(theory::Theory::FULL_EFFORT); \ } @@ -359,13 +366,22 @@ Node TheoryEngine::getValue(TNode node) { bool TheoryEngine::presolve() { d_theoryOut.d_conflictNode = Node::null(); d_theoryOut.d_propagatedLiterals.clear(); + try { - for(unsigned i = 0; i < THEORY_LAST; ++ i) { - d_theoryTable[i]->presolve(); - if(!d_theoryOut.d_conflictNode.get().isNull()) { - return true; - } - } + // Definition of the statement that is to be run by every theory +#ifdef CVC4_FOR_EACH_THEORY_STATEMENT +#undef CVC4_FOR_EACH_THEORY_STATEMENT +#endif +#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ + if (theory::TheoryTraits<THEORY>::hasPresolve && d_theoryIsActive[THEORY]) { \ + reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->presolve(); \ + if(!d_theoryOut.d_conflictNode.get().isNull()) { \ + return true; \ + } \ + } + + // Presolve for each theory using the statement above + CVC4_FOR_EACH_THEORY } catch(const theory::Interrupted&) { Debug("theory") << "TheoryEngine::presolve() => interrupted" << endl; } @@ -375,20 +391,37 @@ bool TheoryEngine::presolve() { void TheoryEngine::notifyRestart() { - for(unsigned i = 0; i < THEORY_LAST; ++ i) { - if (d_theoryTable[i]) { - d_theoryTable[i]->notifyRestart(); - } + // Definition of the statement that is to be run by every theory +#ifdef CVC4_FOR_EACH_THEORY_STATEMENT +#undef CVC4_FOR_EACH_THEORY_STATEMENT +#endif +#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ + if (theory::TheoryTraits<THEORY>::hasNotifyRestart && d_theoryIsActive[THEORY]) { \ + reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->notifyRestart(); \ } -} + // notify each theory using the statement above + CVC4_FOR_EACH_THEORY +} void TheoryEngine::staticLearning(TNode in, NodeBuilder<>& learned) { - for(unsigned i = 0; i < THEORY_LAST; ++ i) { - if (d_theoryTable[i]) { - d_theoryTable[i]->staticLearning(in, learned); - } + // NOTE that we don't look at d_theoryIsActive[] here. First of + // all, we haven't done any pre-registration yet, so we don't know + // which theories are active. Second, let's give each theory a shot + // at doing something with the input formula, even if it wouldn't + // otherwise be active. + + // Definition of the statement that is to be run by every theory +#ifdef CVC4_FOR_EACH_THEORY_STATEMENT +#undef CVC4_FOR_EACH_THEORY_STATEMENT +#endif +#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ + if (theory::TheoryTraits<THEORY>::hasStaticLearning) { \ + reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->staticLearning(in, learned); \ } + + // notify each theory using the statement above + CVC4_FOR_EACH_THEORY } diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 85f26f012..19374d6db 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -11,7 +11,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief The theory engine. + ** \brief The theory engine ** ** The theory engine. **/ @@ -51,10 +51,24 @@ class TheoryEngine { /** Our context */ context::Context* d_context; - /** A table of from theory ifs to theory pointers */ + /** A table of from theory IDs to theory pointers */ theory::Theory* d_theoryTable[theory::THEORY_LAST]; /** + * A bitmap of theories that are "active" for the current run. We + * mark a theory active when we firt see a term or type belonging to + * it. This is important because we can optimize for single-theory + * runs (no sharing), can reduce the cost of walking the DAG on + * registration, etc. + */ + bool d_theoryIsActive[theory::THEORY_LAST]; + + /** + * The count of active theories in the d_theoryIsActive bitmap. + */ + size_t d_activeTheories; + + /** * An output channel for Theory that passes messages * back to a TheoryEngine. */ @@ -159,6 +173,17 @@ class TheoryEngine { */ Node removeITEs(TNode t); + /** + * Mark a theory active if it's not already. + */ + void markActive(theory::TheoryId th) { + if(!d_theoryIsActive[th]) { + d_theoryIsActive[th] = true; + ++d_activeTheories; + Notice() << "Theory " << th << " has been activated." << std::endl; + } + } + public: /** @@ -249,7 +274,7 @@ public: /** * Preprocess a node. This involves theory-specific rewriting, then - * calling preRegisterTerm() on what's left over. + * calling preRegister() on what's left over. * @param n the node to preprocess */ Node preprocess(TNode n); diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h index 8c34370d7..0b377fb11 100644 --- a/src/theory/theory_test_utils.h +++ b/src/theory/theory_test_utils.h @@ -11,17 +11,13 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief [[ Add one-line brief description here ]] + ** \brief Common utilities for testing theories ** - ** [[ Add lengthier description here ]] - ** \todo document this file + ** Common utilities for testing theories. **/ - - #include "cvc4_public.h" - #ifndef __CVC4__THEORY__THEORY_TEST_UTILS_H #define __CVC4__THEORY__ITHEORY_TEST_UTILS_H @@ -48,7 +44,7 @@ enum OutputChannelCallType { AUG_LEMMA, LEMMA, EXPLANATION -}; +};/* enum OutputChannelCallType */ }/* CVC4::theory namespace */ @@ -121,9 +117,11 @@ public: } private: + void push(OutputChannelCallType call, TNode n) { - d_callHistory.push_back(std::make_pair(call,n)); + d_callHistory.push_back(std::make_pair(call, n)); } + };/* class TestOutputChannel */ }/* CVC4::theory namespace */ diff --git a/src/theory/theory_traits_template.h b/src/theory/theory_traits_template.h index c6541dbea..525c06b3c 100644 --- a/src/theory/theory_traits_template.h +++ b/src/theory/theory_traits_template.h @@ -11,10 +11,12 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief [[ Add one-line brief description here ]] + ** \brief A template for the theory_traits.h header, defining various + ** (static) aspects of theories ** - ** [[ Add lengthier description here ]] - ** \todo document this file + ** This file is a template for the theory_traits.h header, defining + ** various (static) aspects of theories, combined with the theory + ** kinds files to produce the final header. **/ #pragma once diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds index a1fcac1df..d7f542038 100644 --- a/src/theory/uf/kinds +++ b/src/theory/uf/kinds @@ -6,15 +6,22 @@ theory THEORY_UF ::CVC4::theory::uf::TheoryUF "theory/uf/theory_uf.h" -properties stable-infinite check propagate staticLearning presolve +properties stable-infinite +properties check propagate staticLearning presolve notifyRestart rewriter ::CVC4::theory::uf::TheoryUfRewriter "theory/uf/theory_uf_rewriter.h" -sort KIND_TYPE "Uninterpreted Sort" +# Justified because we can have an unbounded-but-finite number of +# sorts. Assuming we have |Z| is probably ok for now.. +sort KIND_TYPE Cardinality::INTEGERS "Uninterpreted Sort" parameterized APPLY_UF VARIABLE 1: "uninterpreted function application" variable SORT_TAG "sort tag" parameterized SORT_TYPE SORT_TAG 0: "sort type" +# This is really "unknown" cardinality, but maybe this will be good +# enough (for now) ? Once we support quantifiers, maybe reconsider +# this.. +cardinality SORT_TYPE "Cardinality(Cardinality::INTEGERS)" -endtheory
\ No newline at end of file +endtheory diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 9746b38ab..34d6df881 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -40,6 +40,15 @@ public: TheoryUF(context::Context* ctxt, OutputChannel& out, Valuation valuation) : Theory(THEORY_UF, ctxt, out, valuation) { } + // We declare these here (even though it's not terribly useful) for + // documentation reasons, and to keep mktheorytraits from issuing a + // spurious warning. + virtual void check(Effort) = 0; + virtual void propagate(Effort) {} + virtual void staticLearning(TNode in, NodeBuilder<>& learned) {} + virtual void notifyRestart() {} + virtual void presolve() {} + };/* class TheoryUF */ }/* CVC4::theory::uf namespace */ |