summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/arith/kinds14
-rw-r--r--src/theory/arrays/kinds1
-rw-r--r--src/theory/booleans/kinds9
-rw-r--r--src/theory/builtin/kinds32
-rw-r--r--src/theory/builtin/theory_builtin_type_rules.h50
-rw-r--r--src/theory/datatypes/kinds22
-rw-r--r--src/theory/datatypes/theory_datatypes.cpp16
-rw-r--r--src/theory/datatypes/theory_datatypes.h2
-rw-r--r--src/theory/datatypes/theory_datatypes_type_rules.h66
-rwxr-xr-xsrc/theory/mkrewriter8
-rwxr-xr-xsrc/theory/mktheorytraits14
-rw-r--r--src/theory/uf/kinds6
12 files changed, 212 insertions, 28 deletions
diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index a0fc71ab4..1871e897a 100644
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -18,8 +18,18 @@ operator MINUS 2 "arithmetic binary subtraction operator"
operator UMINUS 1 "arithmetic unary negation"
operator DIVISION 2 "arithmetic division"
-sort REAL_TYPE Cardinality::REALS "Real type"
-sort INTEGER_TYPE Cardinality::INTEGERS "Integer type"
+sort REAL_TYPE \
+ Cardinality::REALS \
+ well-founded \
+ "NodeManager::currentNM()->mkConst(Rational(0))" \
+ "expr/node_manager.h" \
+ "Real type"
+sort INTEGER_TYPE \
+ Cardinality::INTEGERS \
+ well-founded \
+ "NodeManager::currentNM()->mkConst(Integer(0))" \
+ "expr/node_manager.h" \
+ "Integer type"
constant CONST_RATIONAL \
::CVC4::Rational \
diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds
index 533145dc2..4c68fb5cb 100644
--- a/src/theory/arrays/kinds
+++ b/src/theory/arrays/kinds
@@ -15,6 +15,7 @@ operator ARRAY_TYPE 2 "array type"
cardinality ARRAY_TYPE \
"::CVC4::theory::arrays::CardinalityComputer::computeCardinality(%TYPE%)" \
"theory/arrays/theory_arrays_type_rules.h"
+well-founded ARRAY_TYPE false
# select a i is a[i]
operator SELECT 2 "array select"
diff --git a/src/theory/booleans/kinds b/src/theory/booleans/kinds
index ce7c9111a..d540d57f5 100644
--- a/src/theory/booleans/kinds
+++ b/src/theory/booleans/kinds
@@ -10,7 +10,12 @@ properties finite
rewriter ::CVC4::theory::booleans::TheoryBoolRewriter "theory/booleans/theory_bool_rewriter.h"
-sort BOOLEAN_TYPE 2 "Boolean type"
+sort BOOLEAN_TYPE \
+ 2 \
+ well-founded \
+ "NodeManager::currentNM()->mkConst(false)" \
+ "expr/node_manager.h" \
+ "Boolean type"
constant CONST_BOOLEAN \
bool \
@@ -26,4 +31,4 @@ operator OR 2: "logical or"
operator XOR 2 "exclusive or"
operator ITE 3 "if-then-else"
-endtheory \ No newline at end of file
+endtheory
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index a170ba145..f5195e256 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -122,7 +122,7 @@
# For consistency, constants taking a non-void payload should
# start with "CONST_", but this is not enforced.
#
-# sort K cardinality ["comment"]
+# sort K cardinality [well-founded ground-term header | not-well-founded] ["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
@@ -138,6 +138,13 @@
# cardinality as the integers, or Cardinality::REALS if the sort
# has the same cardinality as the reals.
#
+# If the sort is well-founded (i.e., there exist ground terms),
+# then the argument should be the string "well-founded"; if not,
+# it should be the string "not-well-founded". If well-founded,
+# two extra arguments immediately follow---a C++ expression that
+# constructs a ground term (as a Node), and the header that must
+# be #included for that expression to compile.
+#
# For consistency, sorts should end with "_TYPE", but this is not
# enforced.
#
@@ -168,6 +175,15 @@
# ::CVC4::theory::foo::TheoryFoo::CardinalityComputer(%TYPE%) \
# "theory/foo/theory_foo_type_rules.h"
#
+# well-founded K wellfoundedness-computer ground-term-computer [header]
+#
+# Analogous to the "cardinality" command above, the well-founded
+# command provides a well-foundedness computer for the type. A
+# ground term computer is required unless the
+# wellfoundedness-computer is the constant "false". The ground
+# term computer should return a Node, and it should return the
+# same Node each time for a given type (although usually it's only
+# ever called once anyway since the result is cached).
#
#
# Lines may be broken with a backslash between arguments; for example:
@@ -207,7 +223,10 @@ 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 Cardinality::INTEGERS "Built in type for built in operators"
+sort BUILTIN_OPERATOR_TYPE \
+ Cardinality::INTEGERS \
+ not-well-founded \
+ "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
@@ -235,11 +254,16 @@ constant TYPE_CONSTANT \
"basic types"
operator FUNCTION_TYPE 2: "function type"
cardinality FUNCTION_TYPE \
- "::CVC4::theory::builtin::FunctionCardinality::computeCardinality(%TYPE%)" \
+ "::CVC4::theory::builtin::FunctionProperties::computeCardinality(%TYPE%)" \
"theory/builtin/theory_builtin_type_rules.h"
+well-founded FUNCTION_TYPE false
operator TUPLE_TYPE 2: "tuple type"
cardinality TUPLE_TYPE \
- "::CVC4::theory::builtin::TupleCardinality::computeCardinality(%TYPE%)" \
+ "::CVC4::theory::builtin::TupleProperties::computeCardinality(%TYPE%)" \
+ "theory/builtin/theory_builtin_type_rules.h"
+well-founded TUPLE_TYPE \
+ "::CVC4::theory::builtin::TupleProperties::isWellFounded(%TYPE%)" \
+ "::CVC4::theory::builtin::TupleProperties::mkGroundTerm(%TYPE%)" \
"theory/builtin/theory_builtin_type_rules.h"
endtheory
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index bebfca9ab..cffc95ab2 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -128,10 +128,13 @@ public:
}
};/* class TupleTypeRule */
-class FunctionCardinality {
+class FunctionProperties {
public:
inline static Cardinality computeCardinality(TypeNode type) {
- Assert(type.getKind() == kind::FUNCTION_TYPE);
+ // Don't assert this; allow other theories to use this cardinality
+ // computation.
+ //
+ // Assert(type.getKind() == kind::FUNCTION_TYPE);
Cardinality argsCard(1);
// get the largest cardinality of function arguments/return type
@@ -143,12 +146,15 @@ public:
return valueCard ^ argsCard;
}
-};/* class FuctionCardinality */
+};/* class FuctionProperties */
-class TupleCardinality {
+class TupleProperties {
public:
inline static Cardinality computeCardinality(TypeNode type) {
- Assert(type.getKind() == kind::TUPLE_TYPE);
+ // Don't assert this; allow other theories to use this cardinality
+ // computation.
+ //
+ // Assert(type.getKind() == kind::TUPLE_TYPE);
Cardinality card(1);
for(TypeNode::iterator i = type.begin(),
@@ -160,7 +166,39 @@ public:
return card;
}
-};/* class TupleCardinality */
+
+ inline static bool isWellFounded(TypeNode type) {
+ // Don't assert this; allow other theories to use this
+ // wellfoundedness computation.
+ //
+ // Assert(type.getKind() == kind::TUPLE_TYPE);
+
+ for(TypeNode::iterator i = type.begin(),
+ i_end = type.end();
+ i != i_end;
+ ++i) {
+ if(! (*i).isWellFounded()) {
+ return false;
+ }
+ }
+
+ return true;
+ }
+
+ inline static Node mkGroundTerm(TypeNode type) {
+ Assert(type.getKind() == kind::TUPLE_TYPE);
+
+ std::vector<Node> children;
+ for(TypeNode::iterator i = type.begin(),
+ i_end = type.end();
+ i != i_end;
+ ++i) {
+ children.push_back((*i).mkGroundTerm());
+ }
+
+ return NodeManager::currentNM()->mkNode(kind::TUPLE, children);
+ }
+};/* class TupleProperties */
}/* CVC4::theory::builtin namespace */
}/* CVC4::theory namespace */
diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index 8cac2da62..37a65a2b0 100644
--- a/src/theory/datatypes/kinds
+++ b/src/theory/datatypes/kinds
@@ -12,12 +12,27 @@ rewriter ::CVC4::theory::datatypes::DatatypesRewriter "theory/datatypes/datatype
# constructor type has a list of selector types followed by a return type
operator CONSTRUCTOR_TYPE 1: "constructor"
+cardinality CONSTRUCTOR_TYPE \
+ "::CVC4::theory::datatypes::ConstructorProperties::computeCardinality(%TYPE%)" \
+ "theory/datatypes/theory_datatypes_type_rules.h"
+well-founded CONSTRUCTOR_TYPE \
+ "::CVC4::theory::datatypes::ConstructorProperties::isWellFounded(%TYPE%)" \
+ "::CVC4::theory::datatypes::ConstructorProperties::mkGroundTerm(%TYPE%)" \
+ "theory/datatypes/theory_datatypes_type_rules.h"
# selector type has domain type and a range type
operator SELECTOR_TYPE 2 "selector"
+# can re-use function cardinality
+cardinality SELECTOR_TYPE \
+ "::CVC4::theory::builtin::FunctionProperties::computeCardinality(%TYPE%)" \
+ "theory/builtin/theory_builtin_type_rules.h"
# tester type has a constructor type
operator TESTER_TYPE 1 "tester"
+# can re-use function cardinality
+cardinality TESTER_TYPE \
+ "::CVC4::theory::builtin::FunctionProperties::computeCardinality(%TYPE%)" \
+ "theory/builtin/theory_builtin_type_rules.h"
parameterized APPLY_CONSTRUCTOR CONSTRUCTOR_TYPE 0: "constructor application"
@@ -30,5 +45,12 @@ constant DATATYPE_TYPE \
"::CVC4::DatatypeHashStrategy" \
"util/datatype.h" \
"datatype type"
+cardinality DATATYPE_TYPE \
+ "%TYPE%.getConst<Datatype>().getCardinality()" \
+ "util/datatype.h"
+well-founded DATATYPE_TYPE \
+ "%TYPE%.getConst<Datatype>().isWellFounded()" \
+ "%TYPE%.getConst<Datatype>().mkGroundTerm()" \
+ "util/datatype.h"
endtheory
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 5e813b125..ee6f175dd 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -66,7 +66,7 @@ void TheoryDatatypes::checkFiniteWellFounded() {
vector<Node>::iterator itc;
// for each datatype...
for( it = d_cons.begin(); it != d_cons.end(); ++it ) {
- d_distinguishTerms[it->first] = Node::null();
+ //d_distinguishTerms[it->first] = Node::null();
d_finite[it->first] = false;
d_wellFounded[it->first] = false;
// for each ctor of that datatype...
@@ -137,15 +137,15 @@ void TheoryDatatypes::checkFiniteWellFounded() {
for( int c=0; c<(int)ct.getNumChildren()-1; c++ ) {
TypeNode ts = ct[c];
if( ts.isDatatype() ) {
- children.push_back( d_distinguishTerms[ts] );
+ //children.push_back( d_distinguishTerms[ts] );
} else {
//fix? this should be a ground term
children.push_back( nm->mkVar( ts ) );
}
}
- Node dgt = nm->mkNode( APPLY_CONSTRUCTOR, children );
- Debug("datatypes-finite") << "set distinguished ground term " << t << " to " << dgt << endl;
- d_distinguishTerms[t] = dgt;
+ //Node dgt = nm->mkNode( APPLY_CONSTRUCTOR, children );
+ //Debug("datatypes-finite") << "set distinguished ground term " << t << " to " << dgt << endl;
+ //d_distinguishTerms[t] = dgt;
}
}
}
@@ -882,8 +882,8 @@ Node TheoryDatatypes::collapseSelector( TNode t, bool useContext ) {
} else {
Debug("datatypes") << "Applied selector " << t << " to wrong constructor " << endl;
Debug("datatypes") << "Return distinguished term ";
- Debug("datatypes") << d_distinguishTerms[ selType[1] ] << " of type " << selType[1] << endl;
- retNode = d_distinguishTerms[ selType[1] ];
+ Debug("datatypes") << selType[1].mkGroundTerm() << " of type " << selType[1] << endl;
+ retNode = selType[1].mkGroundTerm();
}
if( useContext ) {
Node neq = NodeManager::currentNM()->mkNode( EQUAL, retNode, t );
@@ -900,7 +900,7 @@ Node TheoryDatatypes::collapseSelector( TNode t, bool useContext ) {
checkTester( tester, false );
if( !d_conflict.isNull() ) {
Debug("datatypes") << "Applied selector " << t << " to provably wrong constructor." << endl;
- retNode = d_distinguishTerms[ selType[1] ];
+ retNode = selType[1].mkGroundTerm();
Node neq = NodeManager::currentNM()->mkNode( EQUAL, retNode, t );
NodeBuilder<> nb(kind::AND);
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 36d1b3311..c3b9a0baf 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -56,7 +56,7 @@ private:
/** map from selectors to the constructors they are for */
std::map<Node, Node > d_sel_cons;
/** the distinguished ground term for each type */
- std::map<TypeNode, Node > d_distinguishTerms;
+ //std::map<TypeNode, Node > d_distinguishTerms;
/** finite datatypes/constructor */
std::map< TypeNode, bool > d_finite;
std::map< Node, bool > d_cons_finite;
diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index 1fd24cf53..bc1581f14 100644
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -22,9 +22,18 @@
#define __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H
namespace CVC4 {
+
+namespace expr {
+ namespace attr {
+ struct DatatypeConstructorTypeGroundTermTag {};
+ }/* CVC4::expr::attr namespace */
+}/* CVC4::expr namespace */
+
namespace theory {
namespace datatypes {
+typedef expr::Attribute<expr::attr::DatatypeConstructorTypeGroundTermTag, Node> GroundTermAttr;
+
struct DatatypeConstructorTypeRule {
inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
throw(TypeCheckingExceptionPrivate) {
@@ -47,7 +56,7 @@ struct DatatypeConstructorTypeRule {
}
}
}
- return consType.getConstructorReturnType();
+ return consType.getConstructorRangeType();
}
};/* struct DatatypeConstructorTypeRule */
@@ -91,6 +100,61 @@ struct DatatypeTesterTypeRule {
}
};/* struct DatatypeSelectorTypeRule */
+struct ConstructorProperties {
+ inline static Cardinality computeCardinality(TypeNode type) {
+ // Constructors aren't exactly functions, they're like
+ // parameterized ground terms. So the cardinality is more like
+ // that of a tuple than that of a function.
+ AssertArgument(type.isConstructor(), type);
+ Cardinality c = 1;
+ for(unsigned i = 0, i_end = type.getNumChildren(); i < i_end - 1; ++i) {
+ c *= type[i].getCardinality();
+ }
+ return c;
+ }
+
+ inline static bool isWellFounded(TypeNode type) {
+ // Constructors aren't exactly functions, they're like
+ // parameterized ground terms. So the wellfoundedness is more
+ // like that of a tuple than that of a function.
+ AssertArgument(type.isConstructor(), type);
+ for(unsigned i = 0, i_end = type.getNumChildren(); i < i_end - 1; ++i) {
+ if(!type[i].isWellFounded()) {
+ return false;
+ }
+ }
+ return true;
+ }
+
+ inline static Node mkGroundTerm(TypeNode type) {
+ AssertArgument(type.isConstructor(), type);
+
+ // is this already in the cache ?
+ Node groundTerm = type.getAttribute(GroundTermAttr());
+ if(!groundTerm.isNull()) {
+ return groundTerm;
+ }
+
+ // This is a bit tricky; Constructors have a unique index within
+ // their datatype, but Constructor *types* do not; multiple
+ // Constructors within the same Datatype could share the same
+ // type. So we scan through the datatype to find one that
+ // matches.
+ const Datatype& dt = type[type.getNumChildren() - 1].getConst<Datatype>();
+ for(Datatype::const_iterator i = dt.begin(),
+ i_end = dt.end();
+ i != i_end;
+ ++i) {
+ if(TypeNode::fromType((*i).getConstructor().getType()) == type) {
+ groundTerm = Node::fromExpr((*i).mkGroundTerm());
+ type.setAttribute(GroundTermAttr(), groundTerm);
+ return groundTerm;
+ }
+ }
+
+ InternalError("couldn't find a matching constructor?!");
+ }
+};/* struct ConstructorProperties */
}/* CVC4::theory::datatypes namespace */
}/* CVC4::theory namespace */
diff --git a/src/theory/mkrewriter b/src/theory/mkrewriter
index 78fc39984..ec659d0bb 100755
--- a/src/theory/mkrewriter
+++ b/src/theory/mkrewriter
@@ -125,7 +125,7 @@ function rewriter {
}
function sort {
- # sort TYPE cardinality ["comment"]
+ # sort TYPE cardinality [well-founded ground-term header | not-well-founded] ["comment"]
lineno=${BASH_LINENO[0]}
check_theory_seen
}
@@ -136,6 +136,12 @@ function cardinality {
check_theory_seen
}
+function well-founded {
+ # well-founded TYPE wellfoundedness-computer [header]
+ lineno=${BASH_LINENO[0]}
+ check_theory_seen
+}
+
function variable {
# variable K ["comment"]
lineno=${BASH_LINENO[0]}
diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits
index 9672fc871..2056c6306 100755
--- a/src/theory/mktheorytraits
+++ b/src/theory/mktheorytraits
@@ -197,10 +197,14 @@ function properties {
}
function sort {
- # sort TYPE cardinality ["comment"]
+ # sort TYPE cardinality [well-founded ground-term header | not-well-founded] ["comment"]
lineno=${BASH_LINENO[0]}
check_theory_seen
- register_sort "$1" "$2" "$3"
+ if [ "$3" = well-founded ]; then
+ register_sort "$1" "$2" "$6"
+ else
+ register_sort "$1" "$2" "$4"
+ fi
}
function cardinality {
@@ -209,6 +213,12 @@ function cardinality {
check_theory_seen
}
+function well-founded {
+ # well-founded TYPE wellfoundedness-computer [header]
+ lineno=${BASH_LINENO[0]}
+ check_theory_seen
+}
+
function variable {
# variable K ["comment"]
lineno=${BASH_LINENO[0]}
diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds
index d7f542038..9498fa6fb 100644
--- a/src/theory/uf/kinds
+++ b/src/theory/uf/kinds
@@ -13,7 +13,10 @@ rewriter ::CVC4::theory::uf::TheoryUfRewriter "theory/uf/theory_uf_rewriter.h"
# 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"
+sort KIND_TYPE \
+ Cardinality::INTEGERS \
+ not-well-founded \
+ "Uninterpreted Sort"
parameterized APPLY_UF VARIABLE 1: "uninterpreted function application"
@@ -23,5 +26,6 @@ parameterized SORT_TYPE SORT_TAG 0: "sort type"
# enough (for now) ? Once we support quantifiers, maybe reconsider
# this..
cardinality SORT_TYPE "Cardinality(Cardinality::INTEGERS)"
+well-founded SORT_TYPE false
endtheory
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback