* Type::getCardinality() returns the cardinality for for all types.
Theories give a cardinality in the their kinds file. For
cardinalities that depend on a type argument, a "cardinality
computer" function is named in the kinds file, which takes a
TypeNode and returns its cardinality.
* There's a bitmap for the set of "active theories" in the
TheoryEngine. Theories become "active" when a term that is owned by
them, or whose type is owned by them, is pre-registered (run CVC4
with --verbose to see theory activation). Non-active theories don't
get any calls for check() or propagate() or anything, and if we're
running in single-theory mode, the shared term manager doesn't have
to get involved. This is really important for get() performance
(which can only skimp on walking the entire sub-DAG only if the
theory doesn't require it AND the shared term manager doesn't
require it).
* TheoryEngine now does not call presolve(), registerTerm(),
notifyRestart(), etc., on a Theory if that theory doesn't declare
that property in its kinds file. To avoid coding errors,
mktheorytraits greps the theory header and gives warnings if:
+ the theory appears to declare one of the functions (check,
propagate, etc.) that isn't listed among its kinds file properties
(but probably should be)
+ the theory appears NOT to declare one of the functions listed in
its kinds file properties
* some bounded token stream work
check test units regress: all
(cd $(CURRENT_BUILD)/test && $(MAKE) $@)
+units%:
+ (cd $(CURRENT_BUILD)/test && $(MAKE) units TEST_PREFIX=$(subst units:,,$@))
regress%: all
(cd $(CURRENT_BUILD)/test && $(MAKE) $@)
nodist_libexpr_la_SOURCES = \
kind.h \
metakind.h \
+ type_properties.h \
expr.h \
expr.cpp \
expr_manager.h \
EXTRA_DIST = \
kind_template.h \
metakind_template.h \
+ type_properties_template.h \
expr_manager_template.h \
expr_manager_template.cpp \
expr_template.h \
BUILT_SOURCES = \
kind.h \
metakind.h \
+ type_properties.h \
expr.h \
expr.cpp \
expr_manager.h \
`cat @top_builddir@/src/theory/.subdirs` \
> $@) || (rm -f $@ && exit 1)
+type_properties.h: type_properties_template.h mkkind @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
+ $(AM_V_at)chmod +x @srcdir@/mkkind
+ $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
+ $(AM_V_GEN)(@srcdir@/mkkind \
+ $< \
+ `cat @top_builddir@/src/theory/.subdirs` \
+ > $@) || (rm -f $@ && exit 1)
+
expr.h: expr_template.h mkexpr @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
$(AM_V_at)chmod +x @srcdir@/mkexpr
$(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
*/
Expr mkAssociative(Kind kind, const std::vector<Expr>& children);
-
/** Make a function type from domain to range. */
FunctionType mkFunctionType(Type domain, Type range);
${getConst_instantiations}
-#line 758 "${template}"
+#line 762 "${template}"
namespace expr {
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
- ** \brief Template for the Node kind header.
+ ** \brief Template for the Node kind header
**
** Template for the Node kind header.
**/
# endtheory
lineno=${BASH_LINENO[0]}
check_theory_seen
+ seen_endtheory=true
}
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
}
}
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
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 \
includes \
getConst_instantiations \
getConst_implementations \
mkConst_instantiations \
- mkConst_implementations; do
+ mkConst_implementations \
+ ; do
eval text="\${text//\\\$\\{$var\\}/\${$var}}"
done
error=`expr "$text" : '.*\${\([^}]*\)}.*'`
# Morgan Deters <mdeters@cs.nyu.edu> for CVC4
# Copyright (c) 2010-2011 The CVC4 Project
#
-# The purpose of this script is to create kind.h from a template and a
-# list of theory kinds.
+# The purpose of this script is to create kind.h (and also
+# type_properties.h) from a template and a list of theory kinds.
#
# Invocation:
#
copyright=2010-2011
+filename=`basename "$1" | sed 's,_template,,'`
+
cat <<EOF
/********************* */
-/** kind.h
+/** $filename
**
** Copyright $copyright The AcSys Group, New York University, and as below.
**
** for the CVC4 project.
**/
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+
+/* Edit the template file instead: */
+/* $1 */
+
EOF
me=$(basename "$0")
type_constant_descriptions=
type_constant_list=
type_constant_to_theory_id=
+type_cardinalities=
+type_constant_cardinalities=
+type_cardinalities_includes=
seen_theory=false
seen_theory_builtin=false
# endtheory
lineno=${BASH_LINENO[0]}
check_theory_seen
+ seen_endtheory=true
}
function rewriter {
}
function sort {
- # sort TYPE ["comment"]
+ # sort TYPE cardinality ["comment"]
lineno=${BASH_LINENO[0]}
check_theory_seen
- register_sort "$1" "$2"
+ register_sort "$1" "$2" "$3"
+}
+
+function cardinality {
+ # cardinality TYPE cardinality-computer [header]
+ lineno=${BASH_LINENO[0]}
+ check_theory_seen
+ register_cardinality "$1" "$2" "$3"
}
function variable {
function register_sort {
id=$1
- comment=$2
+ cardinality=$2
+ comment=$3
type_constant_list="${type_constant_list} ${id}, /**< ${comment} */
"
type_constant_descriptions="${type_constant_descriptions} case $id: out << \"${comment}\"; break;
"
- type_constant_to_theory_id="${type_constant_to_theory_id} case $id: return $theory_id; break;
+ type_constant_to_theory_id="${type_constant_to_theory_id} case $id: return $theory_id;
+"
+ type_constant_cardinalities="${type_constant_cardinalities}#line $lineno \"$kf\"
+ case $id: return Cardinality($cardinality);
+"
+}
+
+function register_cardinality {
+ id=$1
+ cardinality_computer=$(sed 's,%TYPE%,typeNode,g' <<<"$2")
+ header=$3
+
+ type_cardinalities="${type_cardinalities}#line $lineno \"$kf\"
+ case $id: return $cardinality_computer;
+"
+ if [ -n "$header" ]; then
+ type_cardinalities_includes="${type_cardinalities_includes}#line $lineno \"$kf\"
+#include \"$header\"
"
+ fi
}
function register_kind {
"
kind_printers="${kind_printers} case $r: out << \"$r\"; break;
"
- kind_to_theory_id="${kind_to_theory_id} case kind::$r: return $theory_id; break;
+ kind_to_theory_id="${kind_to_theory_id} case kind::$r: return $theory_id;
"
}
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
while [ $# -gt 0 ]; do
kf=$1
seen_theory=false
+ seen_endtheory=false
b=$(basename $(dirname "$kf"))
kind_decls="${kind_decls}
/* from $b */
/* 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 kind_decls kind_printers kind_to_theory_id theory_enum type_constant_list type_constant_descriptions type_constant_to_theory_id theory_descriptions; do
+for var in \
+ kind_decls \
+ kind_printers \
+ kind_to_theory_id \
+ theory_enum \
+ type_constant_list \
+ type_constant_descriptions \
+ type_constant_to_theory_id \
+ type_cardinalities \
+ type_constant_cardinalities \
+ type_cardinalities_includes \
+ theory_descriptions \
+ template \
+ ; do
eval text="\${text//\\\$\\{$var\\}/\${$var}}"
done
error=`expr "$text" : '.*\${\([^}]*\)}.*'`
# endtheory
lineno=${BASH_LINENO[0]}
check_theory_seen
+ seen_endtheory=true
}
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
}
}
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
while [ $# -gt 0 ]; do
kf=$1
seen_theory=false
+ seen_endtheory=false
b=$(basename $(dirname "$kf"))
metakind_kinds="${metakind_kinds}
/* from $b */
/* 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 \
metakind_includes \
metakind_constDeleters \
metakind_ubchildren \
metakind_lbchildren \
- metakind_operatorKinds; do
+ metakind_operatorKinds \
+ template \
+ ; do
eval text="\${text//\\\$\\{$var\\}/\${$var}}"
done
error=`expr "$text" : '.*\${\([^}]*\)}.*'`
return d_typeNode->isNull();
}
+Cardinality Type::getCardinality() const {
+ NodeManagerScope nms(d_nodeManager);
+ return d_typeNode->getCardinality();
+}
+
Type& Type::operator=(const Type& t) {
Assert(d_typeNode != NULL, "Unexpected NULL typenode pointer!");
Assert(t.d_typeNode != NULL, "Unexpected NULL typenode pointer!");
#include <stdint.h>
#include "util/Assert.h"
+#include "util/cardinality.h"
namespace CVC4 {
*/
bool isNull() const;
+ /**
+ * Return the cardinality of this type.
+ */
+ Cardinality getCardinality() const;
+
/**
* Substitution of Types.
*/
#include <vector>
#include "expr/type_node.h"
+#include "expr/type_properties.h"
using namespace std;
return nb.constructTypeNode();
}
+Cardinality TypeNode::getCardinality() const {
+ return kind::getCardinality(*this);
+}
+
bool TypeNode::isBoolean() const {
return getKind() == kind::TYPE_CONSTANT &&
getConst<TypeConstant>() == BOOLEAN_TYPE;
#include "expr/kind.h"
#include "expr/metakind.h"
#include "util/Assert.h"
+#include "util/cardinality.h"
namespace CVC4 {
return d_nv == &expr::NodeValue::s_null;
}
+ /**
+ * Returns the cardinality of this type.
+ *
+ * @return a finite or infinite cardinality
+ */
+ Cardinality getCardinality() const;
+
/** Is this the Boolean type? */
bool isBoolean() const;
--- /dev/null
+/********************* */
+/*! \file type_properties_template.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Template for the Type properties header
+ **
+ ** Template for the Type properties header.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__TYPE_PROPERTIES_H
+#define __CVC4__TYPE_PROPERTIES_H
+
+#line 25 "${template}"
+
+#include "expr/type_node.h"
+#include "util/Assert.h"
+#include "expr/kind.h"
+#include "expr/expr.h"
+#include "util/language.h"
+
+#include <sstream>
+
+${type_cardinalities_includes}
+
+#line 37 "${template}"
+
+namespace CVC4 {
+namespace kind {
+
+/**
+ * Return the cardinality of the type constant represented by the
+ * TypeConstant argument. This function is auto-generated from Theory
+ * "kinds" files, so includes contributions from each theory regarding
+ * that theory's types.
+ */
+inline Cardinality getCardinality(TypeConstant tc) {
+ switch(tc) {
+${type_constant_cardinalities}
+#line 51 "${template}"
+ default: {
+ std::stringstream ss;
+ ss << "No cardinality known for type constant " << tc;
+ InternalError(ss.str());
+ }
+ }
+}/* getCardinality(TypeConstant) */
+
+/**
+ * Return the cardinality of the type represented by the TypeNode
+ * argument. This function is auto-generated from Theory "kinds"
+ * files, so includes contributions from each theory regarding that
+ * theory's types.
+ */
+inline Cardinality getCardinality(TypeNode typeNode) {
+ AssertArgument(!typeNode.isNull(), typeNode);
+ switch(Kind k = typeNode.getKind()) {
+ case TYPE_CONSTANT:
+ return getCardinality(typeNode.getConst<TypeConstant>());
+${type_cardinalities}
+#line 72 "${template}"
+ default: {
+ std::stringstream ss;
+ ss << Expr::setlanguage(language::toOutputLanguage
+ ( Options::current()->inputLanguage ));
+ ss << "A theory kinds file did not provide a cardinality "
+ << "or cardinality computer for type:\n" << typeNode
+ << "\nof kind " << k;
+ InternalError(ss.str());
+ }
+ }
+}/* getCardinality(TypeNode) */
+
+}/* CVC4::kind namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__TYPE_PROPERTIES_H */
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
** Common header for replacement function sources.
**/
+#include "cvc4_public.h"
+
#ifndef __CVC4__LIB__REPLACEMENTS_H
#define __CVC4__LIB__REPLACEMENTS_H
postfixTerm[CVC4::Expr& f]
@init {
Expr f2;
- bool extract, left;
+ bool extract = false, left = false;
std::vector<Expr> args;
std::string id;
}
constructorDef[CVC4::Datatype& type]
@init {
std::string id;
- CVC4::Datatype::Constructor* ctor;
+ CVC4::Datatype::Constructor* ctor = NULL;
}
: identifier[id,CHECK_UNDECLARED,SYM_SORT]
{
$< \
`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
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"
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 \
operator GT 2 "greater than, x > y"
operator GEQ 2 "greater than or equal, x >= y"
-endtheory
\ No newline at end of file
+endtheory
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"
# store a i e is a[i] <= e
operator STORE 3 "array store"
-endtheory
\ No newline at end of file
+endtheory
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() { }
** 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"
}
};/* 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 */
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 \
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"); }
# 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"]
#
# 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 \
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
"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
}
};/* 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 */
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"
"::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 \
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
void preRegisterTerm(TNode n);
- void registerTerm(TNode n) { }
+ //void registerTerm(TNode n) { }
void check(Effort e);
- void presolve() { }
+ //void presolve() { }
void propagate(Effort e) { }
}
};
+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 */
//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;
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();
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"); }
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
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
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 {
# 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]}
}
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
}
}
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
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" : '.*\${\([^}]*\)}.*'`
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"
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
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}) \\
"
lineno=${BASH_LINENO[0]}
check_theory_seen
+ seen_endtheory=true
+
theory_traits="${theory_traits}
template<>
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"
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 {
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;
"
}
}
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
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" : '.*\${\([^}]*\)}.*'`
* 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
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),
for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++theoryId) {
d_theoryTable[theoryId] = NULL;
+ d_theoryIsActive[theoryId] = false;
}
Rewriter::init();
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];
}
}
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
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);
}
}
#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; \
#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); \
}
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;
}
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
}
** 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.
**/
/** 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.
*/
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:
/**
/**
* 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);
** 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
AUG_LEMMA,
LEMMA,
EXPLANATION
-};
+};/* enum OutputChannelCallType */
}/* CVC4::theory namespace */
}
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 */
** 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
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
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 */
va_end(args);
}
+ InternalErrorException(const char* function, const char* file, unsigned line,
+ std::string fmt, ...) :
+ AssertionException() {
+ va_list args;
+ va_start(args, fmt);
+ construct("Internal error detected", "",
+ function, file, line, fmt.c_str(), args);
+ va_end(args);
+ }
+
};/* class InternalErrorException */
#ifdef CVC4_DEBUG
stats.cpp \
dynamic_array.h \
language.h \
+ language.cpp \
triple.h \
subrange_bound.h \
+ cardinality.h \
+ cardinality.cpp \
trans_closure.h \
trans_closure.cpp \
boolean_simplification.h \
--- /dev/null
+/********************* */
+/*! \file cardinality.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Representation of cardinality
+ **
+ ** Implementation of a simple class to represent a cardinality.
+ **/
+
+#include "util/cardinality.h"
+
+namespace CVC4 {
+
+const Integer Cardinality::s_intCard(-1);
+const Integer Cardinality::s_realCard(-2);
+
+const Cardinality Cardinality::INTEGERS(Cardinality::Beth(0));
+const Cardinality Cardinality::REALS(Cardinality::Beth(1));
+
+Cardinality& Cardinality::operator+=(const Cardinality& c) throw() {
+ if(isFinite() && c.isFinite()) {
+ d_card += c.d_card;
+ return *this;
+ }
+ if(*this >= c) {
+ return *this;
+ } else {
+ return *this = c;
+ }
+}
+
+/** Assigning multiplication of this cardinality with another. */
+Cardinality& Cardinality::operator*=(const Cardinality& c) throw() {
+ if(*this == 0 || c == 0) {
+ return *this = 0;
+ } else if(!isFinite() || !c.isFinite()) {
+ if(*this >= c) {
+ return *this;
+ } else {
+ return *this = c;
+ }
+ } else {
+ d_card *= c.d_card;
+ return *this;
+ }
+}
+
+/** Assigning exponentiation of this cardinality with another. */
+Cardinality& Cardinality::operator^=(const Cardinality& c)
+ throw(IllegalArgumentException) {
+ if(c == 0) {
+ // (anything) ^ 0 == 1
+ d_card = 1;
+ return *this;
+ } else if(*this == 0) {
+ // 0 ^ (>= 1) == 0
+ return *this;
+ } else if(*this == 1) {
+ // 1 ^ (>= 1) == 1
+ return *this;
+ } else if(c == 1) {
+ // (anything) ^ 1 == (that thing)
+ return *this;
+ } else if(isFinite() && c.isFinite()) {
+ // finite ^ finite == finite
+ //
+ // Note: can throw an assertion if c is too big for
+ // exponentiation
+ d_card = d_card.pow(c.d_card.getUnsignedLong());
+ return *this;
+ } else if(!isFinite() && c.isFinite()) {
+ // inf ^ finite == inf
+ return *this;
+ } else {
+ Assert(*this >= 2 && !c.isFinite(),
+ "fall-through case not as expected:\n%s\n%s",
+ this->toString().c_str(), c.toString().c_str());
+ // (>= 2) ^ beth_k == beth_(k+1)
+ // unless the base is already > the exponent
+ if(*this > c) {
+ return *this;
+ }
+ d_card = c.d_card - 1;
+ return *this;
+ }
+}
+
+
+std::string Cardinality::toString() const throw() {
+ std::stringstream ss;
+ ss << *this;
+ return ss.str();
+}
+
+
+std::ostream& operator<<(std::ostream& out,
+ Cardinality::Beth b)
+ throw() {
+ out << "beth[" << b.getNumber() << ']';
+
+ return out;
+}
+
+
+std::ostream& operator<<(std::ostream& out, const Cardinality& c)
+ throw() {
+ if(c.isFinite()) {
+ out << c.getFiniteCardinality();
+ } else {
+ out << Cardinality::Beth(c.getBethNumber());
+ }
+
+ return out;
+}
+
+
+}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file cardinality.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Representation of cardinality
+ **
+ ** Simple class to represent a cardinality; used by the CVC4 type system
+ ** give the cardinality of sorts.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__CARDINALITY_H
+#define __CVC4__CARDINALITY_H
+
+#include <iostream>
+#include <utility>
+
+#include "util/integer.h"
+#include "util/Assert.h"
+
+namespace CVC4 {
+
+/**
+ * A simple representation of a cardinality. We store an
+ * arbitrary-precision integer for finite cardinalities, and we
+ * distinguish infinite cardinalities represented as Beth numbers.
+ */
+class CVC4_PUBLIC Cardinality {
+ /** Cardinality of the integers */
+ static const Integer s_intCard;
+
+ /** Cardinality of the reals */
+ static const Integer s_realCard;
+
+ /**
+ * In the case of finite cardinality, this is >= 0, and is equal to
+ * the cardinality. If infinite, it is < 0, and is Beth[|card|-1].
+ * That is, "-1" means Beth 0 == |Z|, "-2" means Beth 1 == |R|, etc.
+ */
+ Integer d_card;
+
+public:
+
+ /** The cardinality of the set of integers. */
+ static const Cardinality INTEGERS;
+
+ /** The cardinality of the set of real numbers. */
+ static const Cardinality REALS;
+
+ /**
+ * Representation for a Beth number, used only to construct
+ * Cardinality objects.
+ */
+ class Beth {
+ Integer d_index;
+
+ public:
+ Beth(const Integer& beth) : d_index(beth) {
+ CheckArgument(beth >= 0, beth,
+ "Beth index must be a nonnegative integer, not %s.",
+ beth.toString().c_str());
+ }
+
+ const Integer& getNumber() const throw() {
+ return d_index;
+ }
+ };/* class Cardinality::Beth */
+
+ /**
+ * Construct a finite cardinality equal to the integer argument.
+ * The argument must be nonnegative. If we change this to an
+ * "unsigned" argument to enforce the restriction, we mask some
+ * errors that automatically convert, like "Cardinality(-1)".
+ */
+ Cardinality(long card) : d_card(card) {
+ CheckArgument(card >= 0, card,
+ "Cardinality must be a nonnegative integer, not %ld.", card);
+ Assert(isFinite());
+ }
+
+ /**
+ * Construct a finite cardinality equal to the integer argument.
+ * The argument must be nonnegative.
+ */
+ Cardinality(const Integer& card) : d_card(card) {
+ CheckArgument(card >= 0, card,
+ "Cardinality must be a nonnegative integer, not %s.",
+ card.toString().c_str());
+ Assert(isFinite());
+ }
+
+ /**
+ * Construct an infinite cardinality equal to the given Beth number.
+ */
+ Cardinality(Beth beth) : d_card(-beth.getNumber() - 1) {
+ Assert(!isFinite());
+ }
+
+ /** Returns true iff this cardinality is finite. */
+ bool isFinite() const throw() {
+ return d_card >= 0;
+ }
+
+ /**
+ * Returns true iff this cardinality is finite or countably
+ * infinite.
+ */
+ bool isCountable() const throw() {
+ return d_card >= s_intCard;
+ }
+
+ /**
+ * In the case that this cardinality is finite, return its
+ * cardinality. (If this cardinality is infinite, this function
+ * throws an IllegalArgumentException.)
+ */
+ const Integer& getFiniteCardinality() const throw(IllegalArgumentException) {
+ CheckArgument(isFinite(), *this, "This cardinality is not finite.");
+ return d_card;
+ }
+
+ /**
+ * In the case that this cardinality is infinite, return its Beth
+ * number. (If this cardinality is finite, this function throws an
+ * IllegalArgumentException.)
+ */
+ Integer getBethNumber() const throw(IllegalArgumentException) {
+ CheckArgument(!isFinite(), *this, "This cardinality is not infinite.");
+ return -d_card - 1;
+ }
+
+ /** Assigning addition of this cardinality with another. */
+ Cardinality& operator+=(const Cardinality& c) throw();
+
+ /** Assigning multiplication of this cardinality with another. */
+ Cardinality& operator*=(const Cardinality& c) throw();
+
+ /** Assigning exponentiation of this cardinality with another. */
+ Cardinality& operator^=(const Cardinality& c) throw(IllegalArgumentException);
+
+ /** Add two cardinalities. */
+ Cardinality operator+(const Cardinality& c) const throw() {
+ Cardinality card(*this);
+ card += c;
+ return card;
+ }
+
+ /** Multiply two cardinalities. */
+ Cardinality operator*(const Cardinality& c) const throw() {
+ Cardinality card(*this);
+ card *= c;
+ return card;
+ }
+
+ /**
+ * Exponentiation of two cardinalities. Throws an exception if both
+ * are finite and the exponent is too large.
+ */
+ Cardinality operator^(const Cardinality& c) const throw(IllegalArgumentException) {
+ Cardinality card(*this);
+ card ^= c;
+ return card;
+ }
+
+ /** Test for equality between cardinalities. */
+ bool operator==(const Cardinality& c) const throw() {
+ return d_card == c.d_card;
+ }
+
+ /** Test for disequality between cardinalities. */
+ bool operator!=(const Cardinality& c) const throw() {
+ return !(*this == c);
+ }
+
+ /** Test whether this cardinality is less than another. */
+ bool operator<(const Cardinality& c) const throw() {
+ return
+ ( isFinite() && !c.isFinite() ) ||
+ ( isFinite() && c.isFinite() && d_card < c.d_card ) ||
+ ( !isFinite() && !c.isFinite() && d_card > c.d_card );
+ }
+
+ /**
+ * Test whether this cardinality is less than or equal to
+ * another.
+ */
+ bool operator<=(const Cardinality& c) const throw() {
+ return *this < c || *this == c;
+ }
+
+ /** Test whether this cardinality is greater than another. */
+ bool operator>(const Cardinality& c) const throw() {
+ return !(*this <= c);
+ }
+
+ /**
+ * Test whether this cardinality is greater than or equal to
+ * another.
+ */
+ bool operator>=(const Cardinality& c) const throw() {
+ return !(*this < c);
+ }
+
+ /**
+ * Return a string representation of this cardinality.
+ */
+ std::string toString() const throw();
+
+};/* class Cardinality */
+
+
+/** Print an element of the InfiniteCardinality enumeration. */
+std::ostream& operator<<(std::ostream& out, Cardinality::Beth b)
+ throw() CVC4_PUBLIC;
+
+
+/** Print a cardinality in a human-readable fashion. */
+std::ostream& operator<<(std::ostream& out, const Cardinality& c)
+ throw() CVC4_PUBLIC;
+
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__CARDINALITY_H */
/** Get the name of this constructor argument. */
std::string getName() const throw();
+
/**
* Get the selector for this constructor argument; this call is
* only permitted after resolution.
* to this Datatype constructor.
*/
void addArg(std::string selectorName, Type selectorType);
+
/**
* Add an argument (i.e., a data field) of the given name to this
* Datatype constructor that refers to an as-yet-unresolved
* Datatype (which may be mutually-recursive).
*/
void addArg(std::string selectorName, Datatype::UnresolvedType selectorType);
+
/**
* Add a self-referential (i.e., a data field) of the given name
* to this Datatype constructor that refers to the enclosing
** util/Assert.h.
**/
+#include "cvc4_private.h"
+
#ifndef __CVC4__DEBUG_H
#define __CVC4__DEBUG_H
}
- Integer operator+(const Integer& y) const{
+ Integer operator+(const Integer& y) const {
return Integer( d_value + y.d_value );
}
+ Integer& operator+=(const Integer& y) {
+ d_value += y.d_value;
+ return *this;
+ }
Integer operator-(const Integer& y) const {
return Integer( d_value - y.d_value );
}
+ Integer& operator-=(const Integer& y) {
+ d_value -= y.d_value;
+ return *this;
+ }
Integer operator*(const Integer& y) const {
return Integer( d_value * y.d_value );
}
+ Integer& operator*=(const Integer& y) {
+ d_value *= y.d_value;
+ return *this;
+ }
Integer operator/(const Integer& y) const {
return Integer( cln::floor1(d_value, y.d_value) );
}
+ Integer& operator/=(const Integer& y) {
+ d_value = cln::floor1(d_value, y.d_value);
+ return *this;
+ }
Integer operator%(const Integer& y) const {
return Integer( cln::floor2(d_value, y.d_value).remainder );
}
+ Integer& operator%=(const Integer& y) {
+ d_value = cln::floor2(d_value, y.d_value).remainder;
+ return *this;
+ }
/** Raise this Integer to the power <code>exp</code>.
*
//friend std::ostream& operator<<(std::ostream& os, const Integer& n);
- long getLong() const { return cln::cl_I_to_long(d_value); }
- unsigned long getUnsignedLong() const {return cln::cl_I_to_ulong(d_value); }
+ long getLong() const {
+ // supposed to throw if not representable in type "long"
+ return cln::cl_I_to_long(d_value);
+ }
+
+ unsigned long getUnsignedLong() const {
+ // supposed to throw if not representable in type "unsigned long"
+ return cln::cl_I_to_ulong(d_value);
+ }
/**
* Computes the hash of the node from the first word of the
#include <string>
#include <iostream>
+#include "util/Assert.h"
#include "util/gmp_util.h"
namespace CVC4 {
return d_value == y.d_value;
}
- Integer operator-() const{
+ Integer operator-() const {
return Integer(-(d_value));
}
}
- Integer operator+(const Integer& y) const{
+ Integer operator+(const Integer& y) const {
return Integer( d_value + y.d_value );
}
+ Integer& operator+=(const Integer& y) {
+ d_value += y.d_value;
+ return *this;
+ }
Integer operator-(const Integer& y) const {
return Integer( d_value - y.d_value );
}
+ Integer& operator-=(const Integer& y) {
+ d_value -= y.d_value;
+ return *this;
+ }
Integer operator*(const Integer& y) const {
return Integer( d_value * y.d_value );
}
+ Integer& operator*=(const Integer& y) {
+ d_value *= y.d_value;
+ return *this;
+ }
+
Integer operator/(const Integer& y) const {
return Integer( d_value / y.d_value );
}
+ Integer& operator/=(const Integer& y) {
+ d_value /= y.d_value;
+ return *this;
+ }
+
Integer operator%(const Integer& y) const {
return Integer( d_value % y.d_value );
}
+ Integer& operator%=(const Integer& y) {
+ d_value %= y.d_value;
+ return *this;
+ }
/** Raise this Integer to the power <code>exp</code>.
*
//friend std::ostream& operator<<(std::ostream& os, const Integer& n);
- long getLong() const { return d_value.get_si(); }
- unsigned long getUnsignedLong() const {return d_value.get_ui(); }
+ long getLong() const {
+ long si = d_value.get_si();
+#ifdef CVC4_ASSERTIONS
+ // ensure there wasn't overflow
+ Assert(mpz_cmp_si(d_value.get_mpz_t(), si) == 0);
+#endif /* CVC4_ASSERTIONS */
+ return si;
+ }
+ unsigned long getUnsignedLong() const {
+ unsigned long ui = d_value.get_ui();
+#ifdef CVC4_ASSERTIONS
+ // ensure there wasn't overflow
+ Assert(mpz_cmp_ui(d_value.get_mpz_t(), ui) == 0);
+#endif /* CVC4_ASSERTIONS */
+ return ui;
+ }
/**
* Computes the hash of the node from the first word of the
--- /dev/null
+/********************* */
+/*! \file language.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Definition of input and output languages
+ **
+ ** Definition of input and output languages.
+ **/
+
+#include "util/language.h"
+
+namespace CVC4 {
+namespace language {
+
+InputLanguage toInputLanguage(OutputLanguage language) {
+ switch(language) {
+ case output::LANG_SMTLIB:
+ case output::LANG_SMTLIB_V2:
+ case output::LANG_CVC4:
+ // these entries directly correspond (by design)
+ return InputLanguage(int(language));
+
+ default: {
+ std::stringstream ss;
+ ss << "Cannot map output language `" << language
+ << "' to an input language.";
+ throw CVC4::Exception(ss.str());
+ }
+ }/* switch(language) */
+}/* toInputLanguage() */
+
+OutputLanguage toOutputLanguage(InputLanguage language) {
+ switch(language) {
+ case input::LANG_SMTLIB:
+ case input::LANG_SMTLIB_V2:
+ case input::LANG_CVC4:
+ // these entries directly correspond (by design)
+ return OutputLanguage(int(language));
+
+ default:
+ // Revert to the default (AST) language.
+ //
+ // We used to throw an exception here, but that's not quite right.
+ // We often call this while constructing exceptions, for one, and
+ // it's better to output SOMETHING related to the original
+ // exception rather than mask it with another exception. Also,
+ // the input language isn't always defined---e.g. during the
+ // initial phase of the main CVC4 driver while it determines which
+ // language is appropriate, and during unit tests. Also, when
+ // users are writing their own code against the library.
+ return output::LANG_AST;
+ }/* switch(language) */
+}/* toOutputLanguage() */
+
+}/* CVC4::language namespace */
+}/* CVC4 namespace */
namespace input {
-enum Language {
+enum CVC4_PUBLIC Language {
// SPECIAL "NON-LANGUAGE" LANGUAGES HAVE ENUM VALUE < 0
/** Auto-detect the language */
LANG_MAX
};/* enum Language */
+inline std::ostream& operator<<(std::ostream& out, Language lang) CVC4_PUBLIC;
inline std::ostream& operator<<(std::ostream& out, Language lang) {
switch(lang) {
case LANG_AUTO:
namespace output {
-enum Language {
+enum CVC4_PUBLIC Language {
// SPECIAL "NON-LANGUAGE" LANGUAGES HAVE ENUM VALUE < 0
// COMMON INPUT AND OUTPUT LANGUAGES HAVE ENUM VALUES IN [0,9]
LANG_MAX
};/* enum Language */
+inline std::ostream& operator<<(std::ostream& out, Language lang) CVC4_PUBLIC;
inline std::ostream& operator<<(std::ostream& out, Language lang) {
switch(lang) {
case LANG_SMTLIB:
namespace language {
-inline InputLanguage toInputLanguage(OutputLanguage language) {
- switch(language) {
- case output::LANG_SMTLIB:
- case output::LANG_SMTLIB_V2:
- case output::LANG_CVC4:
- // these entries directly correspond (by design)
- return InputLanguage(int(language));
-
- default: {
- std::stringstream ss;
- ss << "Cannot map output language `" << language
- << "' to an input language.";
- throw CVC4::Exception(ss.str());
- }
- }/* switch(language) */
-}/* toInputLanguage() */
-
-inline OutputLanguage toOutputLanguage(InputLanguage language) {
- switch(language) {
- case input::LANG_SMTLIB:
- case input::LANG_SMTLIB_V2:
- case input::LANG_CVC4:
- // these entries directly correspond (by design)
- return OutputLanguage(int(language));
-
- default: {
- std::stringstream ss;
- ss << "Cannot map input language `" << language
- << "' to an output language.";
- throw CVC4::Exception(ss.str());
- }
- }/* switch(language) */
-}/* toOutputLanguage() */
+InputLanguage toInputLanguage(OutputLanguage language) CVC4_PUBLIC;
+OutputLanguage toOutputLanguage(InputLanguage language) CVC4_PUBLIC;
}/* CVC4::language namespace */
}/* CVC4 namespace */
* an infinite bound). For example, the CVC language subrange [-5.._]
* has a lower bound of -5 and an infinite upper bound.
*/
-class SubrangeBound {
+class CVC4_PUBLIC SubrangeBound {
bool d_nobound;
Integer d_bound;
};/* class SubrangeBound */
+inline std::ostream&
+operator<<(std::ostream& out, const SubrangeBound& bound) throw() CVC4_PUBLIC;
+
inline std::ostream&
operator<<(std::ostream& out, const SubrangeBound& bound) throw() {
if(bound.hasBound()) {
expr/attribute_black \
expr/declaration_scope_black \
expr/node_self_iterator_black \
+ expr/type_cardinality_public \
parser/parser_black \
parser/parser_builder_black \
prop/cnf_stream_black \
util/trans_closure_black \
util/boolean_simplification_black \
util/subrange_bound_white \
+ util/cardinality_public \
main/interactive_shell_black
export VERBOSE = 1
--- /dev/null
+/********************* */
+/*! \file type_cardinality_public.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Public box testing of Type::getCardinality() for various Types
+ **
+ ** Public box testing of Type::getCardinality() for various Types.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include <iostream>
+#include <string>
+#include <sstream>
+
+#include "expr/kind.h"
+#include "expr/type.h"
+#include "expr/expr_manager.h"
+#include "util/cardinality.h"
+#include "util/Assert.h"
+
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace std;
+
+class TypeCardinalityPublic : public CxxTest::TestSuite {
+ ExprManager* d_em;
+
+public:
+
+ void setUp() {
+ d_em = new ExprManager();
+ }
+
+ void tearDown() {
+ delete d_em;
+ }
+
+ void testTheBasics() {
+ TS_ASSERT( d_em->booleanType().getCardinality() == 2 );
+ TS_ASSERT( d_em->integerType().getCardinality() == Cardinality::INTEGERS );
+ TS_ASSERT( d_em->realType().getCardinality() == Cardinality::REALS );
+ }
+
+ void testArrays() {
+ Type intToInt = d_em->mkArrayType(d_em->integerType(), d_em->integerType());
+ Type realToReal = d_em->mkArrayType(d_em->realType(), d_em->realType());
+ Type realToInt = d_em->mkArrayType(d_em->realType(), d_em->integerType());
+ Type intToReal = d_em->mkArrayType(d_em->integerType(), d_em->realType());
+ Type intToBool = d_em->mkArrayType(d_em->integerType(), d_em->booleanType());
+ Type realToBool = d_em->mkArrayType(d_em->realType(), d_em->booleanType());
+ Type boolToReal = d_em->mkArrayType(d_em->booleanType(), d_em->realType());
+ Type boolToInt = d_em->mkArrayType(d_em->booleanType(), d_em->integerType());
+ Type boolToBool = d_em->mkArrayType(d_em->booleanType(), d_em->booleanType());
+
+ TS_ASSERT( intToInt.getCardinality() == Cardinality::REALS );
+ TS_ASSERT( realToReal.getCardinality() > Cardinality::REALS );
+ TS_ASSERT( realToInt.getCardinality() > Cardinality::REALS );
+ TS_ASSERT( intToReal.getCardinality() == Cardinality::REALS );
+ TS_ASSERT( intToBool.getCardinality() == Cardinality::REALS );
+ TS_ASSERT( realToBool.getCardinality() > Cardinality::REALS );
+ TS_ASSERT( boolToReal.getCardinality() == Cardinality::REALS );
+ TS_ASSERT( boolToInt.getCardinality() == Cardinality::INTEGERS );
+ TS_ASSERT( boolToBool.getCardinality() == 4 );
+ }
+
+ void testUnaryFunctions() {
+ Type intToInt = d_em->mkFunctionType(d_em->integerType(), d_em->integerType());
+ Type realToReal = d_em->mkFunctionType(d_em->realType(), d_em->realType());
+ Type realToInt = d_em->mkFunctionType(d_em->realType(), d_em->integerType());
+ Type intToReal = d_em->mkFunctionType(d_em->integerType(), d_em->realType());
+ Type intToBool = d_em->mkFunctionType(d_em->integerType(), d_em->booleanType());
+ Type realToBool = d_em->mkFunctionType(d_em->realType(), d_em->booleanType());
+ Type boolToReal = d_em->mkFunctionType(d_em->booleanType(), d_em->realType());
+ Type boolToInt = d_em->mkFunctionType(d_em->booleanType(), d_em->integerType());
+ Type boolToBool = d_em->mkFunctionType(d_em->booleanType(), d_em->booleanType());
+
+ TS_ASSERT( intToInt.getCardinality() == Cardinality::REALS );
+ TS_ASSERT( realToReal.getCardinality() > Cardinality::REALS );
+ TS_ASSERT( realToInt.getCardinality() > Cardinality::REALS );
+ TS_ASSERT( intToReal.getCardinality() == Cardinality::REALS );
+ TS_ASSERT( intToBool.getCardinality() == Cardinality::REALS );
+ TS_ASSERT( realToBool.getCardinality() > Cardinality::REALS );
+ TS_ASSERT( boolToReal.getCardinality() == Cardinality::REALS );
+ TS_ASSERT( boolToInt.getCardinality() == Cardinality::INTEGERS );
+ TS_ASSERT( boolToBool.getCardinality() == 4 );
+ }
+
+ void testBinaryFunctions() {
+ vector<Type> boolbool; boolbool.push_back(d_em->booleanType()); boolbool.push_back(d_em->booleanType());
+ vector<Type> boolint; boolint.push_back(d_em->booleanType()); boolint.push_back(d_em->integerType());
+ vector<Type> intbool; intbool.push_back(d_em->integerType()); intbool.push_back(d_em->booleanType());
+ vector<Type> intint; intint.push_back(d_em->integerType()); intint.push_back(d_em->integerType());
+ vector<Type> intreal; intreal.push_back(d_em->integerType()); intreal.push_back(d_em->realType());
+ vector<Type> realint; realint.push_back(d_em->realType()); realint.push_back(d_em->integerType());
+ vector<Type> realreal; realreal.push_back(d_em->realType()); realreal.push_back(d_em->realType());
+ vector<Type> realbool; realbool.push_back(d_em->realType()); realbool.push_back(d_em->booleanType());
+ vector<Type> boolreal; boolreal.push_back(d_em->booleanType()); boolreal.push_back(d_em->realType());
+
+ Type boolboolToBool = d_em->mkFunctionType(boolbool, d_em->booleanType());
+ Type boolboolToInt = d_em->mkFunctionType(boolbool, d_em->integerType());
+ Type boolboolToReal = d_em->mkFunctionType(boolbool, d_em->realType());
+
+ Type boolintToBool = d_em->mkFunctionType(boolint, d_em->booleanType());
+ Type boolintToInt = d_em->mkFunctionType(boolint, d_em->integerType());
+ Type boolintToReal = d_em->mkFunctionType(boolint, d_em->realType());
+
+ Type intboolToBool = d_em->mkFunctionType(intbool, d_em->booleanType());
+ Type intboolToInt = d_em->mkFunctionType(intbool, d_em->integerType());
+ Type intboolToReal = d_em->mkFunctionType(intbool, d_em->realType());
+
+ Type intintToBool = d_em->mkFunctionType(intint, d_em->booleanType());
+ Type intintToInt = d_em->mkFunctionType(intint, d_em->integerType());
+ Type intintToReal = d_em->mkFunctionType(intint, d_em->realType());
+
+ Type intrealToBool = d_em->mkFunctionType(intreal, d_em->booleanType());
+ Type intrealToInt = d_em->mkFunctionType(intreal, d_em->integerType());
+ Type intrealToReal = d_em->mkFunctionType(intreal, d_em->realType());
+
+ Type realintToBool = d_em->mkFunctionType(realint, d_em->booleanType());
+ Type realintToInt = d_em->mkFunctionType(realint, d_em->integerType());
+ Type realintToReal = d_em->mkFunctionType(realint, d_em->realType());
+
+ Type realrealToBool = d_em->mkFunctionType(realreal, d_em->booleanType());
+ Type realrealToInt = d_em->mkFunctionType(realreal, d_em->integerType());
+ Type realrealToReal = d_em->mkFunctionType(realreal, d_em->realType());
+
+ Type realboolToBool = d_em->mkFunctionType(realbool, d_em->booleanType());
+ Type realboolToInt = d_em->mkFunctionType(realbool, d_em->integerType());
+ Type realboolToReal = d_em->mkFunctionType(realbool, d_em->realType());
+
+ Type boolrealToBool = d_em->mkFunctionType(boolreal, d_em->booleanType());
+ Type boolrealToInt = d_em->mkFunctionType(boolreal, d_em->integerType());
+ Type boolrealToReal = d_em->mkFunctionType(boolreal, d_em->realType());
+
+ TS_ASSERT( boolboolToBool.getCardinality() == 16 );
+ TS_ASSERT( boolboolToInt.getCardinality() == Cardinality::INTEGERS );
+ TS_ASSERT( boolboolToReal.getCardinality() == Cardinality::REALS );
+
+ TS_ASSERT( boolintToBool.getCardinality() == Cardinality::REALS );
+ TS_ASSERT( boolintToInt.getCardinality() == Cardinality::REALS );
+ TS_ASSERT( boolintToReal.getCardinality() == Cardinality::REALS );
+
+ TS_ASSERT( intboolToBool.getCardinality() == Cardinality::REALS );
+ TS_ASSERT( intboolToInt.getCardinality() == Cardinality::REALS );
+ TS_ASSERT( intboolToReal.getCardinality() == Cardinality::REALS );
+
+ TS_ASSERT( intintToBool.getCardinality() == Cardinality::REALS );
+ TS_ASSERT( intintToInt.getCardinality() == Cardinality::REALS );
+ TS_ASSERT( intintToReal.getCardinality() == Cardinality::REALS );
+
+ TS_ASSERT( intrealToBool.getCardinality() > Cardinality::REALS );
+ TS_ASSERT( intrealToInt.getCardinality() > Cardinality::REALS );
+ TS_ASSERT( intrealToReal.getCardinality() > Cardinality::REALS );
+
+ TS_ASSERT( realintToBool.getCardinality() > Cardinality::REALS );
+ TS_ASSERT( realintToInt.getCardinality() > Cardinality::REALS );
+ TS_ASSERT( realintToReal.getCardinality() > Cardinality::REALS );
+
+ TS_ASSERT( realrealToBool.getCardinality() > Cardinality::REALS );
+ TS_ASSERT( realrealToInt.getCardinality() > Cardinality::REALS );
+ TS_ASSERT( realrealToReal.getCardinality() > Cardinality::REALS );
+
+ TS_ASSERT( realboolToBool.getCardinality() > Cardinality::REALS );
+ TS_ASSERT( realboolToInt.getCardinality() > Cardinality::REALS );
+ TS_ASSERT( realboolToReal.getCardinality() > Cardinality::REALS );
+
+ TS_ASSERT( boolrealToBool.getCardinality() > Cardinality::REALS );
+ TS_ASSERT( boolrealToInt.getCardinality() > Cardinality::REALS );
+ TS_ASSERT( boolrealToReal.getCardinality() > Cardinality::REALS );
+ }
+
+ void testTernaryFunctions() {
+ vector<Type> boolbool; boolbool.push_back(d_em->booleanType()); boolbool.push_back(d_em->booleanType());
+ vector<Type> boolboolbool = boolbool; boolboolbool.push_back(d_em->booleanType());
+
+ Type boolboolTuple = d_em->mkTupleType(boolbool);
+ Type boolboolboolTuple = d_em->mkTupleType(boolboolbool);
+
+ Type boolboolboolToBool = d_em->mkFunctionType(boolboolbool, d_em->booleanType());
+ Type boolboolToBoolbool = d_em->mkFunctionType(boolbool, boolboolTuple);
+ Type boolToBoolboolbool = d_em->mkFunctionType(d_em->booleanType(), boolboolboolTuple);
+
+ TS_ASSERT( boolboolboolToBool.getCardinality() == /* 2 ^ 8 */ 1 << 8 );
+ TS_ASSERT( boolboolToBoolbool.getCardinality() == /* 4 ^ 4 */ 4 * 4 * 4 * 4 );
+ TS_ASSERT( boolToBoolboolbool.getCardinality() == /* 8 ^ 2 */ 8 * 8 );
+ }
+
+ void testUndefinedSorts() {
+ Type foo = d_em->mkSort("foo");
+ // We've currently assigned them a specific Beth number, which
+ // isn't really correct, but...
+ TS_ASSERT( !foo.getCardinality().isFinite() );
+ }
+
+ void testBitvectors() {
+ Debug.on("bvcard");
+ TS_ASSERT( d_em->mkBitVectorType(0).getCardinality() == 0 );
+ for(unsigned i = 1; i < 128; ++i) {
+ try {
+ Cardinality card = Cardinality(2) ^ i;
+ if( d_em->mkBitVectorType(i).getCardinality() != card ) {
+ stringstream ss;
+ ss << "test failed for bitvector(" << i << ")";
+ TS_FAIL(ss.str().c_str());
+ }
+ } catch(Exception& e) {
+ cout << endl << e << endl;
+ throw;
+ }
+ }
+ }
+
+};/* TypeCardinalityPublic */
--- /dev/null
+/********************* */
+/*! \file cardinality_public.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Public-box testing of CVC4::Cardinality
+ **
+ ** Public-box testing of CVC4::Cardinality.
+ **/
+
+#include "util/cardinality.h"
+#include "util/integer.h"
+
+#include <string>
+#include <sstream>
+
+using namespace CVC4;
+using namespace std;
+
+class CardinalityPublic : public CxxTest::TestSuite {
+ stringstream ss;
+
+public:
+
+ void testCardinalities() {
+ Cardinality zero(0);
+ Cardinality one(1);
+ Cardinality two(2);
+
+ Cardinality invalid(0);
+ TS_ASSERT_THROWS( invalid = Cardinality(-1), IllegalArgumentException);
+ TS_ASSERT_THROWS( invalid = Cardinality(-2), IllegalArgumentException);
+ TS_ASSERT_THROWS( invalid = Cardinality(Integer("-3983982192391747295721957")), IllegalArgumentException);
+ invalid = one; // test assignment
+ invalid = Cardinality(5); // test assignment to temporary
+
+ Cardinality copy(one); // test copy
+ Cardinality big(Integer("3983982192391747295721957"));
+ Cardinality r(Cardinality::REALS);
+ Cardinality i(Cardinality::INTEGERS);
+
+ TS_ASSERT( zero < one );
+ TS_ASSERT( one < two );
+ TS_ASSERT( two < invalid );
+ TS_ASSERT( invalid < big );
+ TS_ASSERT( big < i );
+ TS_ASSERT( i < r );
+
+ TS_ASSERT( zero <= one );
+ TS_ASSERT( zero <= zero );
+ TS_ASSERT( one <= two );
+ TS_ASSERT( one <= one );
+ TS_ASSERT( two <= invalid );
+ TS_ASSERT( two <= two );
+ TS_ASSERT( invalid <= big );
+ TS_ASSERT( invalid <= invalid );
+ TS_ASSERT( big <= i );
+ TS_ASSERT( big <= big );
+ TS_ASSERT( i <= r );
+ TS_ASSERT( i <= i );
+ TS_ASSERT( r <= r );
+
+ TS_ASSERT( zero == zero );
+ TS_ASSERT( one == one );
+ TS_ASSERT( two == two );
+ TS_ASSERT( invalid == invalid );
+ TS_ASSERT( copy == copy );
+ TS_ASSERT( copy == one );
+ TS_ASSERT( one == copy );
+ TS_ASSERT( big == big );
+ TS_ASSERT( i == i );
+ TS_ASSERT( r == r );
+
+ TS_ASSERT( zero != one );
+ TS_ASSERT( one != two );
+ TS_ASSERT( two != invalid );
+ TS_ASSERT( copy != r );
+ TS_ASSERT( copy != i );
+ TS_ASSERT( big != i );
+ TS_ASSERT( i != big );
+ TS_ASSERT( big != zero );
+ TS_ASSERT( r != i );
+ TS_ASSERT( i != r );
+
+ TS_ASSERT( r > zero );
+ TS_ASSERT( r > one );
+ TS_ASSERT( r > two );
+ TS_ASSERT( r > copy );
+ TS_ASSERT( r > invalid );
+ TS_ASSERT( r > big );
+ TS_ASSERT( r > i );
+ TS_ASSERT( !( r > r ) );
+ TS_ASSERT( r >= r );
+
+ TS_ASSERT( zero.isFinite() );
+ TS_ASSERT( one.isFinite() );
+ TS_ASSERT( two.isFinite() );
+ TS_ASSERT( copy.isFinite() );
+ TS_ASSERT( invalid.isFinite() );
+ TS_ASSERT( big.isFinite() );
+ TS_ASSERT( !i.isFinite() );
+ TS_ASSERT( !r.isFinite() );
+
+ TS_ASSERT( zero.getFiniteCardinality() == 0 );
+ TS_ASSERT( one.getFiniteCardinality() == 1 );
+ TS_ASSERT( two.getFiniteCardinality() == 2 );
+ TS_ASSERT( copy.getFiniteCardinality() == 1 );
+ TS_ASSERT( invalid.getFiniteCardinality() == 5 );
+ TS_ASSERT( big.getFiniteCardinality() == Integer("3983982192391747295721957") );
+ TS_ASSERT_THROWS( i.getFiniteCardinality(), IllegalArgumentException );
+ TS_ASSERT_THROWS( r.getFiniteCardinality(), IllegalArgumentException );
+
+ TS_ASSERT_THROWS( zero.getBethNumber(), IllegalArgumentException );
+ TS_ASSERT_THROWS( one.getBethNumber(), IllegalArgumentException );
+ TS_ASSERT_THROWS( two.getBethNumber(), IllegalArgumentException );
+ TS_ASSERT_THROWS( copy.getBethNumber(), IllegalArgumentException );
+ TS_ASSERT_THROWS( invalid.getBethNumber(), IllegalArgumentException );
+ TS_ASSERT_THROWS( big.getBethNumber(), IllegalArgumentException );
+ TS_ASSERT( i.getBethNumber() == 0 );
+ TS_ASSERT( r.getBethNumber() == 1 );
+
+ TS_ASSERT( zero != Cardinality::INTEGERS );
+ TS_ASSERT( one != Cardinality::INTEGERS );
+ TS_ASSERT( two != Cardinality::INTEGERS );
+ TS_ASSERT( copy != Cardinality::INTEGERS );
+ TS_ASSERT( invalid != Cardinality::INTEGERS );
+ TS_ASSERT( big != Cardinality::INTEGERS );
+ TS_ASSERT( r != Cardinality::INTEGERS );
+ TS_ASSERT( i == Cardinality::INTEGERS );
+
+ TS_ASSERT( zero != Cardinality::REALS );
+ TS_ASSERT( one != Cardinality::REALS );
+ TS_ASSERT( two != Cardinality::REALS );
+ TS_ASSERT( copy != Cardinality::REALS );
+ TS_ASSERT( invalid != Cardinality::REALS );
+ TS_ASSERT( big != Cardinality::REALS );
+ TS_ASSERT( i != Cardinality::REALS );
+ TS_ASSERT( r == Cardinality::REALS );
+
+ // should work the other way too
+
+ TS_ASSERT( Cardinality::INTEGERS != zero );
+ TS_ASSERT( Cardinality::INTEGERS != one );
+ TS_ASSERT( Cardinality::INTEGERS != two );
+ TS_ASSERT( Cardinality::INTEGERS != copy );
+ TS_ASSERT( Cardinality::INTEGERS != invalid );
+ TS_ASSERT( Cardinality::INTEGERS != big );
+ TS_ASSERT( Cardinality::INTEGERS != r );
+ TS_ASSERT( Cardinality::INTEGERS == i );
+
+ TS_ASSERT( Cardinality::REALS != zero );
+ TS_ASSERT( Cardinality::REALS != one );
+ TS_ASSERT( Cardinality::REALS != two );
+ TS_ASSERT( Cardinality::REALS != copy );
+ TS_ASSERT( Cardinality::REALS != invalid );
+ TS_ASSERT( Cardinality::REALS != big );
+ TS_ASSERT( Cardinality::REALS != i );
+ TS_ASSERT( Cardinality::REALS == r );
+
+ // finite cardinal arithmetic
+
+ TS_ASSERT( zero + zero == zero );
+ TS_ASSERT( zero * zero == zero );
+ TS_ASSERT( (zero ^ zero) == one );
+ TS_ASSERT( zero + one == one );
+ TS_ASSERT( zero * one == zero );
+ TS_ASSERT( (zero ^ one) == zero );
+ TS_ASSERT( one + zero == one );
+ TS_ASSERT( one * zero == zero );
+ TS_ASSERT( (one ^ zero) == one );
+ TS_ASSERT( two + two == 4 );
+ TS_ASSERT( (two ^ two) == 4 );
+ TS_ASSERT( two * two == 4 );
+ TS_ASSERT( (two += two) == 4 );
+ TS_ASSERT( two == 4 );
+ TS_ASSERT( (two = 2) == 2 );
+ TS_ASSERT( two == 2 );
+ TS_ASSERT( (two *= 2) == 4 );
+ TS_ASSERT( two == 4 );
+ TS_ASSERT( ((two = 2) ^= 2) == 4 );
+ TS_ASSERT( two == 4 );
+ TS_ASSERT( (two = 2) == 2 );
+
+ // infinite cardinal arithmetic
+
+ Cardinality x = i, y = Cardinality(2)^x, z = Cardinality(2)^y;
+
+ TS_ASSERT( x == i && y == r );
+ TS_ASSERT( x != r && y != i );
+ TS_ASSERT( x != z && y != z );
+ TS_ASSERT( x.isCountable() && !x.isFinite() );
+ TS_ASSERT( !y.isCountable() && !y.isFinite() );
+ TS_ASSERT( !z.isCountable() && !z.isFinite() );
+
+ TS_ASSERT( big < x );
+ TS_ASSERT( x < y );
+ TS_ASSERT( y < z );
+
+ TS_ASSERT_THROWS( big.getBethNumber(), IllegalArgumentException );
+ TS_ASSERT( x.getBethNumber() == 0 );
+ TS_ASSERT( y.getBethNumber() == 1 );
+ TS_ASSERT( z.getBethNumber() == 2 );
+
+ TS_ASSERT( (zero ^ x) == zero );
+ TS_ASSERT( (one ^ x) == one );
+ TS_ASSERT( (two ^ x) == y && (two ^ x) != x );
+ TS_ASSERT( (big ^ x) == y && (big ^ x) != x );
+ TS_ASSERT( (two ^ x) == (big ^ x) );
+
+ TS_ASSERT( (x ^ zero) == one );
+ TS_ASSERT( (x ^ one) == x );
+ TS_ASSERT( (x ^ two) == x );
+ TS_ASSERT( (x ^ big) == x );
+ TS_ASSERT( (x ^ big) == (x ^ two) );
+
+ TS_ASSERT( (zero ^ y) == zero );
+ TS_ASSERT( (one ^ y) == one );
+ TS_ASSERT( (two ^ y) != x && (two ^ y) != y );
+ TS_ASSERT( (big ^ y) != y && (big ^ y) != y );
+ TS_ASSERT( (big ^ y).getBethNumber() == 2 );
+ TS_ASSERT( (two ^ y) == (big ^ y) );
+
+ TS_ASSERT( (y ^ zero) == one );
+ TS_ASSERT( (y ^ one) == y );
+ TS_ASSERT( (y ^ two) == y );
+ TS_ASSERT( (y ^ big) == y );
+ TS_ASSERT( (y ^ big) == (y ^ two) );
+
+ TS_ASSERT( (x ^ x) == y );
+ TS_ASSERT( (y ^ x) == y );
+ TS_ASSERT( (x ^ y) == z );
+ TS_ASSERT( (y ^ y) == z );
+ TS_ASSERT( (z ^ x) == z );
+ TS_ASSERT( (z ^ y) == z );
+ TS_ASSERT( (zero ^ z) == 0 );
+ TS_ASSERT( (z ^ zero) == 1 );
+ TS_ASSERT( (z ^ 0) == 1 );
+ TS_ASSERT( (two ^ z) > z );
+ TS_ASSERT( (big ^ z) == (two ^ z) );
+ TS_ASSERT( (x ^ z) == (two ^ z) );
+ TS_ASSERT( (y ^ z) == (x ^ z) );
+ TS_ASSERT( (z ^ z) == (x ^ z) );
+ TS_ASSERT( (z ^ z).getBethNumber() == 3 );
+
+ }/* testCardinalities() */
+
+};/* class CardinalityPublic */
#include <cxxtest/TestSuite.h>
#include <sstream>
+#include <limits>
#include "util/integer.h"
TS_ASSERT_EQUALS( Integer(-1000), Integer(-10).pow(3) );
}
+ void testOverlyLong() {
+ unsigned long ul = numeric_limits<unsigned long>::max();
+ Integer i(ul);
+ TS_ASSERT(i.getUnsignedLong() == ul);
+ TS_ASSERT_THROWS_ANYTHING(i.getLong());
+ unsigned long ulplus1 = ul + 1;
+ TS_ASSERT(ulplus1 == 0);
+ i = i + 1;
+ TS_ASSERT_THROWS_ANYTHING(i.getUnsignedLong());
+ }
+
void testTestBit() {
TS_ASSERT( ! Integer(0).testBit(6) );
TS_ASSERT( ! Integer(0).testBit(5) );
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
- ** \brief White box testing of CVC4::SubrangeBound
+ ** \brief White-box testing of CVC4::SubrangeBound
**
- ** White box testing of CVC4::SubrangeBound.
+ ** White-box testing of CVC4::SubrangeBound.
**/
#include "util/subrange_bound.h"
projects / cvc5.git / commitdiff