summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/Makefile.am12
-rw-r--r--src/theory/arith/kinds9
-rw-r--r--src/theory/arrays/kinds8
-rw-r--r--src/theory/arrays/theory_arrays.h6
-rw-r--r--src/theory/arrays/theory_arrays_type_rules.h15
-rw-r--r--src/theory/booleans/kinds4
-rw-r--r--src/theory/booleans/theory_bool.h9
-rw-r--r--src/theory/builtin/kinds114
-rw-r--r--src/theory/builtin/theory_builtin_type_rules.h33
-rw-r--r--src/theory/bv/kinds8
-rw-r--r--src/theory/bv/theory_bv.h4
-rw-r--r--src/theory/bv/theory_bv_type_rules.h14
-rw-r--r--src/theory/datatypes/theory_datatypes.cpp4
-rw-r--r--src/theory/datatypes/theory_datatypes.h4
-rwxr-xr-xsrc/theory/mkrewriter70
-rwxr-xr-xsrc/theory/mktheorytraits89
-rw-r--r--src/theory/theory_engine.cpp73
-rw-r--r--src/theory/theory_engine.h31
-rw-r--r--src/theory/theory_test_utils.h14
-rw-r--r--src/theory/theory_traits_template.h8
-rw-r--r--src/theory/uf/kinds13
-rw-r--r--src/theory/uf/theory_uf.h9
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback