#include "base/output.h"
#include "expr/expr_iomanip.h"
#include "expr/kind.h"
-#include "expr/predicate.h"
#include "options/options.h"
#include "options/set_language.h"
#include "parser/parser.h"
}
Type ValidityChecker::subrangeType(const Expr& l, const Expr& r) {
+/*
bool noLowerBound = l.getType().isString() && l.getConst<CVC4::String>() == "_NEGINF";
bool noUpperBound = r.getType().isString() && r.getConst<CVC4::String>() == "_POSINF";
CompatCheckArgument(noLowerBound || (l.getKind() == CVC4::kind::CONST_RATIONAL && l.getConst<Rational>().isIntegral()), l);
CVC4::SubrangeBound bl = noLowerBound ? CVC4::SubrangeBound() : CVC4::SubrangeBound(l.getConst<Rational>().getNumerator());
CVC4::SubrangeBound br = noUpperBound ? CVC4::SubrangeBound() : CVC4::SubrangeBound(r.getConst<Rational>().getNumerator());
return d_em->mkSubrangeType(CVC4::SubrangeBounds(bl, br));
+ */
+ Unimplemented("Subrange types not supported by CVC4 (sorry!)");
}
Type ValidityChecker::subtypeType(const Expr& pred, const Expr& witness) {
- Unimplemented("Predicate subtyping not supported by CVC4 yet (sorry!)");
+ Unimplemented("Predicate subtyping not supported by CVC4 (sorry!)");
/*
if(witness.isNull()) {
return d_em->mkPredicateSubtype(pred);
variable_type_map.h \
datatype.h \
datatype.cpp \
- predicate.h \
- predicate.cpp \
record.cpp \
record.h \
uninterpreted_constant.cpp \
kind.i \
expr.i \
record.i \
- predicate.i \
variable_type_map.i \
uninterpreted_constant.i
new TypeNode(d_nodeManager->mkSortConstructor(name, arity))));
}
-/* - not in release 1.0
-Type ExprManager::mkPredicateSubtype(Expr lambda)
- throw(TypeCheckingException) {
- NodeManagerScope nms(d_nodeManager);
- try {
- return PredicateSubtype(Type(d_nodeManager,
- new TypeNode(d_nodeManager->mkPredicateSubtype(lambda))));
- } catch (const TypeCheckingExceptionPrivate& e) {
- throw TypeCheckingException(this, &e);
- }
-}
-*/
-
-/* - not in release 1.0
-Type ExprManager::mkPredicateSubtype(Expr lambda, Expr witness)
- throw(TypeCheckingException) {
- NodeManagerScope nms(d_nodeManager);
- try {
- return PredicateSubtype(Type(d_nodeManager,
- new TypeNode(d_nodeManager->mkPredicateSubtype(lambda, witness))));
- } catch (const TypeCheckingExceptionPrivate& e) {
- throw TypeCheckingException(this, &e);
- }
-}
-*/
-
-Type ExprManager::mkSubrangeType(const SubrangeBounds& bounds)
- throw(TypeCheckingException) {
- NodeManagerScope nms(d_nodeManager);
- try {
- return SubrangeType(Type(d_nodeManager,
- new TypeNode(d_nodeManager->mkSubrangeType(bounds))));
- } catch (const TypeCheckingExceptionPrivate& e) {
- throw TypeCheckingException(this, &e);
- }
-}
-
/**
* Get the type for the given Expr and optionally do type checking.
*
return to->mkTypeConst(n.getConst<TypeConstant>());
} else if(n.getKind() == kind::BITVECTOR_TYPE) {
return to->mkBitVectorType(n.getConst<BitVectorSize>());
- } else if(n.getKind() == kind::SUBRANGE_TYPE) {
- return to->mkSubrangeType(n.getSubrangeBounds());
}
Type from_t = from->toType(n);
Type& to_t = vmap.d_typeMap[from_t];
/**
* Make an integer subrange type as defined by the argument.
*/
- Type mkSubrangeType(const SubrangeBounds& bounds)
- throw(TypeCheckingException);
+ //Type mkSubrangeType(const SubrangeBounds& bounds)
+ // throw(TypeCheckingException);
/** Get the type of an expression */
Type getType(Expr e, bool check = false)
return mkTypeNode(kind::CONSTRUCTOR_TYPE, sorts);
}
-TypeNode NodeManager::mkPredicateSubtype(Expr lambda)
- throw(TypeCheckingExceptionPrivate) {
-
- Node lambdan = Node::fromExpr(lambda);
-
- if(lambda.isNull()) {
- throw TypeCheckingExceptionPrivate(lambdan, "cannot make a predicate subtype based on null expression");
- }
-
- TypeNode tn = lambdan.getType();
- if(! tn.isPredicateLike() ||
- tn.getArgTypes().size() != 1) {
- stringstream ss;
- ss << "expected a predicate of one argument to define predicate subtype, but got type `" << tn << "'";
- throw TypeCheckingExceptionPrivate(lambdan, ss.str());
- }
-
- return TypeNode(mkTypeConst(Predicate(lambda)));
-}
-
-TypeNode NodeManager::mkPredicateSubtype(Expr lambda, Expr witness)
- throw(TypeCheckingExceptionPrivate) {
-
- Node lambdan = Node::fromExpr(lambda);
-
- if(lambda.isNull()) {
- throw TypeCheckingExceptionPrivate(lambdan, "cannot make a predicate subtype based on null expression");
- }
-
- TypeNode tn = lambdan.getType();
- if(! tn.isPredicateLike() ||
- tn.getArgTypes().size() != 1) {
- stringstream ss;
- ss << "expected a predicate of one argument to define predicate subtype, but got type `" << tn << "'";
- throw TypeCheckingExceptionPrivate(lambdan, ss.str());
- }
-
- return TypeNode(mkTypeConst(Predicate(lambda, witness)));
-}
-
-TypeNode NodeManager::mkSubrangeType(const SubrangeBounds& bounds)
- throw(TypeCheckingExceptionPrivate) {
- return TypeNode(mkTypeConst(bounds));
-}
-
TypeNode NodeManager::TupleTypeCache::getTupleType( NodeManager * nm, std::vector< TypeNode >& types, unsigned index ) {
if( index==types.size() ){
if( d_data.isNull() ){
/** Make a new sort with the given name and arity. */
TypeNode mkSortConstructor(const std::string& name, size_t arity);
- /**
- * Make a predicate subtype type defined by the given LAMBDA
- * expression. A TypeCheckingExceptionPrivate can be thrown if
- * lambda is not a LAMBDA, or is ill-typed, or if CVC4 fails at
- * proving that the resulting predicate subtype is inhabited.
- */
- TypeNode mkPredicateSubtype(Expr lambda)
- throw(TypeCheckingExceptionPrivate);
-
- /**
- * Make a predicate subtype type defined by the given LAMBDA
- * expression and whose non-emptiness is witnessed by the given
- * witness. A TypeCheckingExceptionPrivate can be thrown if lambda
- * is not a LAMBDA, or is ill-typed, or if the witness is not a
- * witness or ill-typed.
- */
- TypeNode mkPredicateSubtype(Expr lambda, Expr witness)
- throw(TypeCheckingExceptionPrivate);
-
- /**
- * Make an integer subrange type as defined by the argument.
- */
- TypeNode mkSubrangeType(const SubrangeBounds& bounds)
- throw(TypeCheckingExceptionPrivate);
-
/**
* Get the type for the given node and optionally do type checking.
*
+++ /dev/null
-/********************* */
-/*! \file predicate.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Tim King, Morgan Deters, Paul Meng
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Representation of predicates for predicate subtyping
- **
- ** Simple class to represent predicates for predicate subtyping.
- ** Instances of this class are carried as the payload of
- ** the CONSTANT-metakinded SUBTYPE_TYPE types.
- **/
-#include "expr/predicate.h"
-
-#include "base/cvc4_assert.h"
-#include "expr/expr.h"
-
-
-using namespace std;
-
-namespace CVC4 {
-
-Predicate::Predicate(const Predicate& p)
- : d_predicate(new Expr(p.getExpression()))
- , d_witness(new Expr(p.getWitness()))
-{}
-
-Predicate::Predicate(const Expr& e) throw(IllegalArgumentException)
- : d_predicate(new Expr(e))
- , d_witness(new Expr())
-{
- PrettyCheckArgument(! e.isNull(), e, "Predicate cannot be null");
- PrettyCheckArgument(e.getType().isPredicate(), e,
- "Expression given is not predicate");
- PrettyCheckArgument(FunctionType(e.getType()).getArgTypes().size() == 1, e,
- "Expression given is not predicate of a single argument");
-}
-
-Predicate::Predicate(const Expr& e, const Expr& w)
- throw(IllegalArgumentException)
- : d_predicate(new Expr(e))
- , d_witness(new Expr(w))
-{
- PrettyCheckArgument(! e.isNull(), e, "Predicate cannot be null");
- PrettyCheckArgument(e.getType().isPredicate(), e,
- "Expression given is not predicate");
- PrettyCheckArgument(FunctionType(e.getType()).getArgTypes().size() == 1, e,
- "Expression given is not predicate of a single argument");
-}
-
-Predicate::~Predicate() {
- delete d_predicate;
- delete d_witness;
-}
-
-Predicate& Predicate::operator=(const Predicate& p){
- (*d_predicate) = p.getExpression();
- (*d_witness) = p.getWitness();
- return *this;
-}
-
-
-// Predicate::operator Expr() const {
-// return d_predicate;
-// }
-
-const Expr& Predicate::getExpression() const {
- return *d_predicate;
-}
-
-const Expr& Predicate::getWitness() const {
- return *d_witness;
-}
-
-bool Predicate::operator==(const Predicate& p) const {
- return getExpression() == p.getExpression() &&
- getWitness() == p.getWitness();
-}
-
-std::ostream& operator<<(std::ostream& out, const Predicate& p) {
- out << p.getExpression();
- const Expr& witness = p.getWitness();
- if(! witness.isNull()) {
- out << " : " << witness;
- }
- return out;
-}
-
-size_t PredicateHashFunction::operator()(const Predicate& p) const {
- ExprHashFunction h;
- return h(p.getWitness()) * 5039 + h(p.getExpression());
-}
-
-}/* CVC4 namespace */
+++ /dev/null
-/********************* */
-/*! \file predicate.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Morgan Deters, Tim King, Paul Meng
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Representation of predicates for predicate subtyping
- **
- ** Simple class to represent predicates for predicate subtyping.
- ** Instances of this class are carried as the payload of
- ** the CONSTANT-metakinded SUBTYPE_TYPE types.
- **/
-
-#include "cvc4_public.h"
-
-#ifndef __CVC4__PREDICATE_H
-#define __CVC4__PREDICATE_H
-
-#include "base/exception.h"
-
-namespace CVC4 {
-
-class Predicate;
-
-std::ostream& operator<<(std::ostream& out, const Predicate& p) CVC4_PUBLIC;
-
-struct CVC4_PUBLIC PredicateHashFunction {
- size_t operator()(const Predicate& p) const;
-};/* class PredicateHashFunction */
-
-}/* CVC4 namespace */
-
-
-namespace CVC4 {
-class CVC4_PUBLIC Expr;
-}/* CVC4 namespace */
-
-
-namespace CVC4 {
-class CVC4_PUBLIC Predicate {
-public:
-
- Predicate(const Expr& e) throw(IllegalArgumentException);
- Predicate(const Expr& e, const Expr& w) throw(IllegalArgumentException);
-
- Predicate(const Predicate& p);
- ~Predicate();
- Predicate& operator=(const Predicate& p);
-
- //operator Expr() const;
-
- const Expr& getExpression() const;
- const Expr& getWitness() const;
-
- bool operator==(const Predicate& p) const;
-
- friend std::ostream& CVC4::operator<<(std::ostream& out, const Predicate& p);
- friend size_t PredicateHashFunction::operator()(const Predicate& p) const;
-
-private:
- Expr* d_predicate;
- Expr* d_witness;
-};/* class Predicate */
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__PREDICATE_H */
+++ /dev/null
-%{
-#include "expr/predicate.h"
-%}
-
-%rename(equals) CVC4::Predicate::operator==(const Predicate&) const;
-%rename(toExpr) CVC4::Predicate::operator Expr() const;
-
-%rename(apply) CVC4::PredicateHashFunction::operator()(const Predicate&) const;
-
-%ignore CVC4::operator<<(std::ostream&, const Predicate&);
-
-%include "expr/predicate.h"
return d_typeNode->isSortConstructor();
}
-/** Is this a predicate subtype */
-/* - not in release 1.0
-bool Type::isPredicateSubtype() const {
- NodeManagerScope nms(d_nodeManager);
- return d_typeNode->isPredicateSubtype();
-}
-*/
-
-/** Is this an integer subrange */
-bool Type::isSubrange() const {
- NodeManagerScope nms(d_nodeManager);
- return d_typeNode->isSubrange();
-}
-
size_t FunctionType::getArity() const {
return d_typeNode->getNumChildren() - 1;
}
PrettyCheckArgument(isNull() || isSortConstructor(), this);
}
-/* - not in release 1.0
-PredicateSubtype::PredicateSubtype(const Type& t)
- throw(IllegalArgumentException) :
- Type(t) {
- PrettyCheckArgument(isNull() || isPredicateSubtype(), this);
-}
-*/
-
-SubrangeType::SubrangeType(const Type& t)
- throw(IllegalArgumentException) :
- Type(t) {
- PrettyCheckArgument(isNull() || isSubrange(), this);
-}
-
unsigned BitVectorType::getSize() const {
return d_typeNode->getBitVectorSize();
}
}
*/
-SubrangeBounds SubrangeType::getSubrangeBounds() const {
- NodeManagerScope nms(d_nodeManager);
- return d_typeNode->getSubrangeBounds();
-}
-
size_t TypeHashFunction::operator()(const Type& t) const {
return TypeNodeHashFunction()(NodeManager::fromType(t));
}
* Is this an integer subrange type?
* @return true if this is an integer subrange type
*/
- bool isSubrange() const;
+ //bool isSubrange() const;
/**
* Outputs a string representation of this type to the stream.
Type getParentType() const;
};/* class PredicateSubtype */
-#endif /* 0 */
/**
* Class encapsulating an integer subrange type.
SubrangeBounds getSubrangeBounds() const;
};/* class SubrangeType */
+#endif /* 0 */
/**
* Class encapsulating the bit-vector type.
return false;
}
}
- if(isSubrange()) {
- if(t.isSubrange()) {
- return t.getSubrangeBounds() <= getSubrangeBounds();
- } else {
- return t.getKind() == kind::TYPE_CONSTANT &&
- ( t.getConst<TypeConstant>() == INTEGER_TYPE ||
- t.getConst<TypeConstant>() == REAL_TYPE );
- }
- }
if(isTuple() && t.isTuple()) {
const Datatype& dt1 = getDatatype();
const Datatype& dt2 = t.getDatatype();
}
return true;
}
- if(isPredicateSubtype()) {
- return getSubtypeParentType().isSubtypeOf(t);
- }
if(isSet() && t.isSet()) {
return getSetElementType().isSubtypeOf(t.getSetElementType());
}
if(isArray() && t.isArray()) {
return getArrayIndexType().isComparableTo(t.getArrayIndexType()) && getArrayConstituentType().isComparableTo(t.getArrayConstituentType());
}
- //if(isPredicateSubtype()) {
- // return t.isComparableTo(getSubtypeParentType());
- //}
return false;
}
-Node TypeNode::getSubtypePredicate() const {
- Assert(isPredicateSubtype());
- return Node::fromExpr(getConst<Predicate>().getExpression());
-}
-
-TypeNode TypeNode::getSubtypeParentType() const {
- Assert(isPredicateSubtype());
- return getSubtypePredicate().getType().getArgTypes()[0];
-}
-
TypeNode TypeNode::getBaseType() const {
TypeNode realt = NodeManager::currentNM()->realType();
if (isSubtypeOf(realt)) {
return realt;
- } else if (isPredicateSubtype()) {
- return getSubtypeParentType().getBaseType();
} else if (isParametricDatatype()) {
vector<Type> v;
for(size_t i = 1; i < getNumChildren(); ++i) {
/** Is this a tuple type? */
bool TypeNode::isTuple() const {
- return ( getKind() == kind::DATATYPE_TYPE && getDatatype().isTuple() ) ||
- ( isPredicateSubtype() && getSubtypeParentType().isTuple() );
+ return ( getKind() == kind::DATATYPE_TYPE && getDatatype().isTuple() );
}
/** Is this a record type? */
bool TypeNode::isRecord() const {
- return ( getKind() == kind::DATATYPE_TYPE && getDatatype().isRecord() ) ||
- ( isPredicateSubtype() && getSubtypeParentType().isRecord() );
+ return ( getKind() == kind::DATATYPE_TYPE && getDatatype().isRecord() );
}
size_t TypeNode::getTupleLength() const {
return TypeNode(); // null type
}
default:
- //if(t1.isPredicateSubtype() && t1.getSubtypeParentType().isSubtypeOf(t0)) {
- // return t0; // t0 is a constant type
- //} else {
- return TypeNode(); // null type
- //}
+ return TypeNode(); // null type
}
} else if(t1.getKind() == kind::TYPE_CONSTANT) {
return commonTypeNode(t1, t0, isLeast); // decrease the number of special cases
case kind::CONSTRUCTOR_TYPE:
case kind::SELECTOR_TYPE:
case kind::TESTER_TYPE:
- //if( t1.isPredicateSubtype() && t1.getSubtypeParentType().isSubtypeOf(t0)) {
- // return t0;
- //} else {
- return TypeNode();
- //}
+ return TypeNode();
case kind::FUNCTION_TYPE:
return TypeNode(); // Not sure if this is right
case kind::SET_TYPE: {
case kind::SEXPR_TYPE:
Unimplemented("haven't implemented leastCommonType for symbolic expressions yet");
return TypeNode();
- case kind::SUBTYPE_TYPE:
- //if(t1.isPredicateSubtype()){
- // // This is the case where both t0 and t1 are predicate subtypes.
- // return leastCommonPredicateSubtype(t0, t1);
- //}else{ // t0 is a predicate subtype and t1 is not
- // return commonTypeNode(t1, t0, isLeast); //decrease the number of special cases
- //}
- return TypeNode();
- case kind::SUBRANGE_TYPE:
- /*
- if(t1.isSubrange()) {
- const SubrangeBounds& t0SR = t0.getSubrangeBounds();
- const SubrangeBounds& t1SR = t1.getSubrangeBounds();
- if(SubrangeBounds::joinIsBounded(t0SR, t1SR)) {
- SubrangeBounds j = SubrangeBounds::join(t0SR, t1SR);
- return NodeManager::currentNM()->mkSubrangeType(j);
- } else {
- return NodeManager::currentNM()->integerType();
- }
- } else if(t1.isPredicateSubtype()) {
- // t0 is a subrange
- // t1 is not a subrange
- // t1 is a predicate subtype
- if(t1.isInteger()) {
- return NodeManager::currentNM()->integerType();
- } else if(t1.isReal()) {
- return NodeManager::currentNM()->realType();
- } else {
- return TypeNode();
- }
- } else {
- // t0 is a subrange
- // t1 is not a subrange
- // t1 is not a type constant && is not a predicate subtype
- // t1 cannot be real subtype or integer.
- Assert(t1.isReal());
- Assert(t1.isInteger());
- return TypeNode();
- }
-*/
- return TypeNode();
case kind::DATATYPE_TYPE:
if( t0.isTuple() && t1.isTuple() ){
const Datatype& dt1 = t0.getDatatype();
if(!t1.isParametricDatatype()) {
return TypeNode();
}
- while(t1.getKind() != kind::PARAMETRIC_DATATYPE) {
- t1 = t1.getSubtypeParentType();
- }
if(t0[0] != t1[0] || t0.getNumChildren() != t1.getNumChildren()) {
return TypeNode();
}
}
}
-TypeNode TypeNode::leastCommonPredicateSubtype(TypeNode t0, TypeNode t1){
- Assert(t0.isPredicateSubtype());
- Assert(t1.isPredicateSubtype());
-
- std::vector<TypeNode> t0stack;
- t0stack.push_back(t0);
- while(t0stack.back().isPredicateSubtype()){
- t0stack.push_back(t0stack.back().getSubtypeParentType());
- }
- std::vector<TypeNode> t1stack;
- t1stack.push_back(t1);
- while(t1stack.back().isPredicateSubtype()){
- t1stack.push_back(t1stack.back().getSubtypeParentType());
- }
-
- Assert(!t0stack.empty());
- Assert(!t1stack.empty());
-
- if(t0stack.back() == t1stack.back()){
- TypeNode mostGeneral = t1stack.back();
- t0stack.pop_back(); t1stack.pop_back();
- while(!t0stack.empty() && t1stack.empty() && t0stack.back() == t1stack.back()){
- mostGeneral = t0stack.back();
- t0stack.pop_back(); t1stack.pop_back();
- }
- return mostGeneral;
- }else{
- return leastCommonTypeNode(t0stack.back(), t1stack.back());
- }
-}
-
-
Node TypeNode::getEnsureTypeCondition( Node n, TypeNode tn ) {
TypeNode ntn = n.getType();
Assert( ntn.isComparableTo( tn ) );
/** Is this a sort kind */
bool TypeNode::isSort() const {
- return ( getKind() == kind::SORT_TYPE && !hasAttribute(expr::SortArityAttr()) ) ||
- ( isPredicateSubtype() && getSubtypeParentType().isSort() );
+ return ( getKind() == kind::SORT_TYPE && !hasAttribute(expr::SortArityAttr()) );
}
/** Is this a sort constructor kind */
/** Is this a sort constructor kind */
bool isSortConstructor() const;
- /** Is this a subtype predicate */
- bool isPredicateSubtype() const;
-
- /** Get the predicate defining this subtype */
- Node getSubtypePredicate() const;
-
- /**
- * Get the parent type of this subtype; note that it could be
- * another subtype.
- */
- TypeNode getSubtypeParentType() const;
-
/** Get the most general base type of the type */
TypeNode getBaseType() const;
- /** Is this a subrange */
- bool isSubrange() const;
-
- /** Get the bounds defining this subrange */
- const SubrangeBounds& getSubrangeBounds() const;
-
/**
* Returns the leastUpperBound in the extended type lattice of the two types.
* If this is \top, i.e. there is no inhabited type that contains both,
static Node getEnsureTypeCondition( Node n, TypeNode tn );
private:
static TypeNode commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast);
-
- /**
- * Returns the leastUpperBound in the extended type lattice of two
- * predicate subtypes.
- */
- static TypeNode leastCommonPredicateSubtype(TypeNode t0, TypeNode t1);
-
+
/**
* Indents the given stream a given amount of spaces.
*
inline bool TypeNode::isBoolean() const {
return
- ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == BOOLEAN_TYPE ) ||
- ( isPredicateSubtype() && getSubtypeParentType().isBoolean() );
+ ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == BOOLEAN_TYPE );
}
inline bool TypeNode::isInteger() const {
return
- ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == INTEGER_TYPE ) ||
- isSubrange() ||
- ( isPredicateSubtype() && getSubtypeParentType().isInteger() );
+ ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == INTEGER_TYPE );
}
inline bool TypeNode::isReal() const {
return
( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == REAL_TYPE ) ||
- isInteger() ||
- ( isPredicateSubtype() && getSubtypeParentType().isReal() );
+ isInteger();
}
inline bool TypeNode::isString() const {
/** Is this a symbolic expression type? */
inline bool TypeNode::isSExpr() const {
- return getKind() == kind::SEXPR_TYPE ||
- ( isPredicateSubtype() && getSubtypeParentType().isSExpr() );
-}
-
-/** Is this a predicate subtype */
-inline bool TypeNode::isPredicateSubtype() const {
- return getKind() == kind::SUBTYPE_TYPE;
-}
-
-/** Is this a subrange type */
-inline bool TypeNode::isSubrange() const {
- return getKind() == kind::SUBRANGE_TYPE ||
- ( isPredicateSubtype() && getSubtypeParentType().isSubrange() );
+ return getKind() == kind::SEXPR_TYPE;
}
/** Is this a floating-point type */
inline bool TypeNode::isFloatingPoint() const {
- return getKind() == kind::FLOATINGPOINT_TYPE ||
- ( isPredicateSubtype() && getSubtypeParentType().isFloatingPoint() );
+ return getKind() == kind::FLOATINGPOINT_TYPE;
}
/** Is this a bit-vector type */
inline bool TypeNode::isBitVector() const {
- return getKind() == kind::BITVECTOR_TYPE ||
- ( isPredicateSubtype() && getSubtypeParentType().isBitVector() );
+ return getKind() == kind::BITVECTOR_TYPE;
}
/** Is this a datatype type */
inline bool TypeNode::isDatatype() const {
- return getKind() == kind::DATATYPE_TYPE || getKind() == kind::PARAMETRIC_DATATYPE ||
- ( isPredicateSubtype() && getSubtypeParentType().isDatatype() );
+ return getKind() == kind::DATATYPE_TYPE || getKind() == kind::PARAMETRIC_DATATYPE;
}
/** Is this a parametric datatype type */
inline bool TypeNode::isParametricDatatype() const {
- return getKind() == kind::PARAMETRIC_DATATYPE ||
- ( isPredicateSubtype() && getSubtypeParentType().isParametricDatatype() );
+ return getKind() == kind::PARAMETRIC_DATATYPE;
}
/** Is this a codatatype type */
return
( getKind() == kind::FLOATINGPOINT_TYPE &&
getConst<FloatingPointSize>().exponent() == exp &&
- getConst<FloatingPointSize>().significand() == sig ) ||
- ( isPredicateSubtype() && getSubtypeParentType().isFloatingPoint(exp,sig) );
+ getConst<FloatingPointSize>().significand() == sig );
}
/** Is this a bit-vector type of size <code>size</code> */
inline bool TypeNode::isBitVector(unsigned size) const {
return
- ( getKind() == kind::BITVECTOR_TYPE && getConst<BitVectorSize>() == size ) ||
- ( isPredicateSubtype() && getSubtypeParentType().isBitVector(size) );
+ ( getKind() == kind::BITVECTOR_TYPE && getConst<BitVectorSize>() == size );
}
/** Get the datatype specification from a datatype type */
return getConst<BitVectorSize>();
}
-inline const SubrangeBounds& TypeNode::getSubrangeBounds() const {
- Assert(isSubrange());
- if(getKind() == kind::SUBRANGE_TYPE){
- return getConst<SubrangeBounds>();
- }else{
- Assert(isPredicateSubtype());
- return getSubtypeParentType().getSubrangeBounds();
- }
-}
-
#ifdef CVC4_DEBUG
/**
* Pretty printer for use within gdb. This is not intended to be used
<< "] inappropriate: range must be nonempty!";
PARSER_STATE->parseError(ss.str());
}
- t = EXPR_MANAGER->mkSubrangeType(SubrangeBounds(k1, k2));
+ PARSER_STATE->unimplementedFeature("subrange typing not supported in this release");
+ //t = EXPR_MANAGER->mkSubrangeType(SubrangeBounds(k1, k2));
}
/* tuple types / old-style function types */
}
break;
}
- case kind::SUBRANGE_TYPE:
- out << '[' << n.getConst<SubrangeBounds>() << ']';
- break;
- case kind::SUBTYPE_TYPE:
- out << "SUBTYPE(" << n.getConst<Predicate>() << ")";
- break;
case kind::TYPE_CONSTANT:
switch(TypeConstant tc = n.getConst<TypeConstant>()) {
case REAL_TYPE:
toStream(out, n[0], depth, types, true);
const Datatype& dt = ((DatatypeType)t.toType()).getDatatype();
int sindex = dt[0].getSelectorIndexInternal( opn.toExpr() );
+ Assert( sindex>=0 );
out << '.' << sindex;
}else if( t.isRecord() ){
toStream(out, n[0], depth, types, true);
const Record& rec = t.getRecord();
const Datatype& dt = ((DatatypeType)t.toType()).getDatatype();
int sindex = dt[0].getSelectorIndexInternal( opn.toExpr() );
+ Assert( sindex>=0 );
std::pair<std::string, Type> fld = rec[sindex];
out << '.' << fld.first;
}else{
break;
}
- case kind::SUBRANGE_TYPE: {
- const SubrangeBounds& bounds = n.getConst<SubrangeBounds>();
- // No way to represent subranges in SMT-LIBv2; this is inspired
- // by yices format (but isn't identical to it).
- out << "(subrange " << bounds.lower << ' ' << bounds.upper << ')';
- break;
- }
- case kind::SUBTYPE_TYPE:
- // No way to represent predicate subtypes in SMT-LIBv2; this is
- // inspired by yices format (but isn't identical to it).
- out << "(subtype " << n.getConst<Predicate>() << ')';
- break;
-
case kind::DATATYPE_TYPE:
{
const Datatype & dt = (NodeManager::currentNM()->getDatatypeForIndex( n.getConst< DatatypeIndexConstant >().getIndex() ));
/** TODO: whether certain preprocess steps are necessary */
//bool d_needsExpandDefs;
- //bool d_needsRewriteBoolTerms;
- //bool d_needsConstrainSubTypes;
public:
/**
*/
void compressBeforeRealAssertions(size_t before);
- /**
- * Any variable in an assertion that is declared as a subtype type
- * (predicate subtype or integer subrange type) must be constrained
- * to be in that type.
- */
- void constrainSubtypes(TNode n, AssertionPipeline& assertions)
- throw();
-
/**
* Trace nodes back to their assertions using CircuitPropagator's
* BackEdgesMap.
d_abstractValueMap(&d_fakeContext),
d_abstractValues(),
d_simplifyAssertionsDepth(0),
- //d_needsExpandDefs(true),
- //d_needsRewriteBoolTerms(true),
- //d_needsConstrainSubTypes(true), //TODO
+ //d_needsExpandDefs(true), //TODO?
d_iteSkolemMap(),
d_iteRemover(smt.d_userContext),
d_pbsProcessor(smt.d_userContext),
d_smt.d_theoryEngine->ppUnconstrainedSimp(d_assertions.ref());
}
-
-void SmtEnginePrivate::constrainSubtypes(TNode top, AssertionPipeline& assertions)
- throw() {
-
- Trace("constrainSubtypes") << "constrainSubtypes(): looking at " << top << endl;
-
- set<TNode> done;
- stack<TNode> worklist;
- worklist.push(top);
- done.insert(top);
-
- do {
- TNode n = worklist.top();
- worklist.pop();
-
- TypeNode t = n.getType();
- if(t.isPredicateSubtype()) {
- WarningOnce() << "Warning: CVC4 doesn't yet do checking that predicate subtypes are nonempty domains" << endl;
- Node pred = t.getSubtypePredicate();
- Kind k;
- // pred can be a LAMBDA, a function constant, or a datatype tester
- Trace("constrainSubtypes") << "constrainSubtypes(): pred.getType() == " << pred.getType() << endl;
- if(d_smt.d_definedFunctions->find(pred) != d_smt.d_definedFunctions->end()) {
- k = kind::APPLY;
- } else if(pred.getType().isTester()) {
- k = kind::APPLY_TESTER;
- } else {
- k = kind::APPLY_UF;
- }
- Node app = NodeManager::currentNM()->mkNode(k, pred, n);
- Trace("constrainSubtypes") << "constrainSubtypes(): assert(" << k << ") " << app << endl;
- assertions.push_back(app);
- } else if(t.isSubrange()) {
- SubrangeBounds bounds = t.getSubrangeBounds();
- Trace("constrainSubtypes") << "constrainSubtypes(): got bounds " << bounds << endl;
- if(bounds.lower.hasBound()) {
- Node c = NodeManager::currentNM()->mkConst(Rational(bounds.lower.getBound()));
- Node lb = NodeManager::currentNM()->mkNode(kind::LEQ, c, n);
- Trace("constrainSubtypes") << "constrainSubtypes(): assert " << lb << endl;
- assertions.push_back(lb);
- }
- if(bounds.upper.hasBound()) {
- Node c = NodeManager::currentNM()->mkConst(Rational(bounds.upper.getBound()));
- Node ub = NodeManager::currentNM()->mkNode(kind::LEQ, n, c);
- Trace("constrainSubtypes") << "constrainSubtypes(): assert " << ub << endl;
- assertions.push_back(ub);
- }
- }
-
- for(TNode::iterator i = n.begin(); i != n.end(); ++i) {
- if(done.find(*i) == done.end()) {
- worklist.push(*i);
- done.insert(*i);
- }
- }
- } while(! worklist.empty());
-}
-
void SmtEnginePrivate::traceBackToAssertions(const std::vector<Node>& nodes, std::vector<TNode>& assertions) {
const booleans::CircuitPropagator::BackEdgesMap& backEdges = d_propagator.getBackEdges();
for(vector<Node>::const_iterator i = nodes.begin(); i != nodes.end(); ++i) {
Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
- dumpAssertions("pre-constrain-subtypes", d_assertions);
- {
- // Any variables of subtype types need to be constrained properly.
- // Careful, here: constrainSubtypes() adds to the back of
- // d_assertions, but we don't need to reprocess those.
- // We also can't use an iterator, because the vector may be moved in
- // memory during this loop.
- Chat() << "constraining subtypes..." << endl;
- for(unsigned i = 0, i_end = d_assertions.size(); i != i_end; ++i) {
- constrainSubtypes(d_assertions[i], d_assertions);
- }
- }
- dumpAssertions("post-constrain-subtypes", d_assertions);
-
- Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
-
bool noConflict = true;
// Unconstrained simplification
"expr/node_manager.h" \
"integer type"
-constant SUBRANGE_TYPE \
- ::CVC4::SubrangeBounds \
- ::CVC4::SubrangeBoundsHashFunction \
- "util/subrange_bound.h" \
- "the type of an integer subrange"
-cardinality SUBRANGE_TYPE \
- "::CVC4::theory::arith::SubrangeProperties::computeCardinality(%TYPE%)" \
- "theory/arith/theory_arith_type_rules.h"
-well-founded SUBRANGE_TYPE \
- true \
- "::CVC4::theory::arith::SubrangeProperties::mkGroundTerm(%TYPE%)" \
- "theory/arith/theory_arith_type_rules.h"
-
constant CONST_RATIONAL \
::CVC4::Rational \
::CVC4::RationalHashFunction \
enumerator INTEGER_TYPE \
"::CVC4::theory::arith::IntegerEnumerator" \
"theory/arith/type_enumerator.h"
-enumerator SUBRANGE_TYPE \
- "::CVC4::theory::arith::SubrangeEnumerator" \
- "theory/arith/type_enumerator.h"
operator LT 2 "less than, x < y"
operator LEQ 2 "less than or equal, x <= y"
}
};/* class RealNullaryOperatorTypeRule */
-
-class SubrangeProperties {
-public:
- inline static Cardinality computeCardinality(TypeNode type) {
- Assert(type.getKind() == kind::SUBRANGE_TYPE);
-
- const SubrangeBounds& bounds = type.getConst<SubrangeBounds>();
- if(!bounds.lower.hasBound() || !bounds.upper.hasBound()) {
- return Cardinality::INTEGERS;
- }
- return Cardinality(bounds.upper.getBound() - bounds.lower.getBound());
- }
-
- inline static Node mkGroundTerm(TypeNode type) {
- Assert(type.getKind() == kind::SUBRANGE_TYPE);
-
- const SubrangeBounds& bounds = type.getConst<SubrangeBounds>();
- if(bounds.lower.hasBound()) {
- return NodeManager::currentNM()->mkConst(Rational(bounds.lower.getBound()));
- }
- if(bounds.upper.hasBound()) {
- return NodeManager::currentNM()->mkConst(Rational(bounds.upper.getBound()));
- }
- return NodeManager::currentNM()->mkConst(Rational(0));
- }
-};/* class SubrangeProperties */
-
}/* CVC4::theory::arith namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
};/* class IntegerEnumerator */
-class SubrangeEnumerator : public TypeEnumeratorBase<SubrangeEnumerator> {
- Integer d_int;
- SubrangeBounds d_bounds;
- bool d_direction;// true == +, false == -
-
-public:
-
- SubrangeEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) :
- TypeEnumeratorBase<SubrangeEnumerator>(type),
- d_int(0),
- d_bounds(type.getConst<SubrangeBounds>()),
- d_direction(d_bounds.lower.hasBound()) {
-
- d_int = d_direction ? d_bounds.lower.getBound() : d_bounds.upper.getBound();
-
- Assert(type.getKind() == kind::SUBRANGE_TYPE);
-
- // if we're counting down, there's no lower bound
- Assert(d_direction || !d_bounds.lower.hasBound());
- }
-
- Node operator*() throw(NoMoreValuesException) {
- if(isFinished()) {
- throw NoMoreValuesException(getType());
- }
- return NodeManager::currentNM()->mkConst(Rational(d_int));
- }
-
- SubrangeEnumerator& operator++() throw() {
- if(d_direction) {
- if(!d_bounds.upper.hasBound() || d_int <= d_bounds.upper.getBound()) {
- d_int += 1;
- }
- } else {
- // if we're counting down, there's no lower bound
- d_int -= 1;
- }
- return *this;
- }
-
- bool isFinished() throw() {
- // if we're counting down, there's no lower bound
- return d_direction &&
- d_bounds.upper.hasBound() &&
- d_int > d_bounds.upper.getBound();
- }
-
-};/* class SubrangeEnumerator */
-
}/* CVC4::theory::arith namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
throw TypeCheckingExceptionPrivate(n, "array select operating on non-array");
}
TypeNode indexType = n[1].getType(check);
- if(!indexType.isComparableTo(arrayType.getArrayIndexType())){
- //if(!indexType.isSubtypeOf(arrayType.getArrayIndexType())){ //FIXME:typing
+ if(!indexType.isSubtypeOf(arrayType.getArrayIndexType())){
throw TypeCheckingExceptionPrivate(n, "array select not indexed with correct type for array");
}
}
}
TypeNode indexType = n[1].getType(check);
TypeNode valueType = n[2].getType(check);
- if(!indexType.isComparableTo(arrayType.getArrayIndexType())){
- //if(!indexType.isSubtypeOf(arrayType.getArrayIndexType())){ //FIXME:typing
+ if(!indexType.isSubtypeOf(arrayType.getArrayIndexType())){
throw TypeCheckingExceptionPrivate(n, "array store not indexed with correct type for array");
}
- if(!valueType.isComparableTo(arrayType.getArrayConstituentType())){
- //if(!valueType.isSubtypeOf(arrayType.getArrayConstituentType())){ //FIXME:typing
+ if(!valueType.isSubtypeOf(arrayType.getArrayConstituentType())){
Debug("array-types") << "array type: "<< arrayType.getArrayConstituentType() << std::endl;
Debug("array-types") << "value types: " << valueType << std::endl;
throw TypeCheckingExceptionPrivate(n, "array store not assigned with correct type for array");
typerule CHAIN ::CVC4::theory::builtin::ChainTypeRule
typerule CHAIN_OP ::CVC4::theory::builtin::ChainedOperatorTypeRule
-constant SUBTYPE_TYPE \
- ::CVC4::Predicate \
- ::CVC4::PredicateHashFunction \
- "expr/predicate.h" \
- "predicate subtype; payload is an instance of the CVC4::Predicate class"
-cardinality SUBTYPE_TYPE \
- "::CVC4::theory::builtin::SubtypeProperties::computeCardinality(%TYPE%)" \
- "theory/builtin/theory_builtin_type_rules.h"
-well-founded SUBTYPE_TYPE \
- "::CVC4::theory::builtin::SubtypeProperties::isWellFounded(%TYPE%)" \
- "::CVC4::theory::builtin::SubtypeProperties::mkGroundTerm(%TYPE%)" \
- "theory/builtin/theory_builtin_type_rules.h"
-
endtheory
TypeNode lhsType = n[0].getType(check);
TypeNode rhsType = n[1].getType(check);
+ // TODO : we may want to limit cases where we have equalities between terms of different types
+ // equalities between (Set Int) and (Set Real) already cause strange issues in theory solver for sets
+ // one possibility is to only allow this for Int/Real
if ( TypeNode::leastCommonTypeNode(lhsType, rhsType).isNull() ) {
std::stringstream ss;
ss << "Subexpressions must have a common base type:" << std::endl;
}
};/* class SExprProperties */
-class SubtypeProperties {
-public:
-
- inline static Cardinality computeCardinality(TypeNode type) {
- Assert(type.getKind() == kind::SUBTYPE_TYPE);
- Unimplemented("Computing the cardinality for predicate subtype not yet supported.");
- }
-
- inline static bool isWellFounded(TypeNode type) {
- Assert(type.getKind() == kind::SUBTYPE_TYPE);
- Unimplemented("Computing the well-foundedness for predicate subtype not yet supported.");
- }
-
- inline static Node mkGroundTerm(TypeNode type) {
- Assert(type.getKind() == kind::SUBTYPE_TYPE);
- Unimplemented("Constructing a ground term for predicate subtype not yet supported.");
- }
-
-};/* class SubtypeProperties */
-
}/* CVC4::theory::builtin namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
Debug("typecheck-idt") << "typecheck cons arg: " << childType << " "
<< (*tchild_it) << std::endl;
TypeNode argumentType = *tchild_it;
- if (!childType.isComparableTo(argumentType)) {
- //if (!childType.isSubtypeOf(argumentType)) { //FIXME:typing
+ if (!childType.isSubtypeOf(argumentType)) {
std::stringstream ss;
ss << "bad type for constructor argument:\n"
<< "child type: " << childType << "\n"
throw TypeCheckingExceptionPrivate(n, "checking for membership in a non-set");
}
TypeNode elementType = n[0].getType(check);
+ // TODO : still need to be flexible here due to situations like:
+ //
+ // T : (Set Int)
+ // S : (Set Real)
+ // (= (as T (Set Real)) S)
+ // (member 0.5 S)
+ // ...where (member 0.5 T) is inferred
+ //
+ // or
+ //
+ // S : (Set Real)
+ // (not (member 0.5 s))
+ // (member 0.0 s)
+ // ...find model M where M( s ) = { 0 }, check model will generate (not (member 0.5 (singleton 0)))
+ //
if(!elementType.isComparableTo(setType.getSetElementType())) {
//if(!elementType.isSubtypeOf(setType.getSetElementType())) { //FIXME:typing
std::stringstream ss;
static inline TheoryId theoryOf(TypeNode typeNode) {
Trace("theory::internal") << "theoryOf(" << typeNode << ")" << std::endl;
TheoryId id;
- while (typeNode.isPredicateSubtype()) {
- typeNode = typeNode.getSubtypeParentType();
- }
if (typeNode.getKind() == kind::TYPE_CONSTANT) {
id = typeConstantToTheoryId(typeNode.getConst<TypeConstant>());
} else {
++argument_it, ++argument_type_it) {
TypeNode currentArgument = (*argument_it).getType();
TypeNode currentArgumentType = *argument_type_it;
- if (!currentArgument.isComparableTo(currentArgumentType)) {
- //if (!currentArgument.isSubtypeOf(currentArgumentType)) { //FIXME:typing
+ if (!currentArgument.isSubtypeOf(currentArgumentType)) {
std::stringstream ss;
ss << "argument type is not a subtype of the function's argument "
<< "type:\n"
bug576.smt2 \
bug576a.smt2 \
bug578.smt2 \
- bug585.cvc \
bug586.cvc \
bug593.smt2 \
bug595.cvc \
# bug512 -- taking too long, --time-per not working perhaps? in any case,
# we have a minimized version still getting tested
# bug639 -- still fails, reopened bug
+# bug585 -- contains subrange type (not supported)
DISABLED_TESTS = \
- bug512.smt2
+ bug512.smt2 \
+ bug585.cvc
EXTRA_DIST = $(TESTS) \
simplification_bug4.smt2.expect \
rec1.cvc \
rec2.cvc \
rec4.cvc \
- rec5.cvc \
datatype.cvc \
datatype0.cvc \
datatype1.cvc \
datatype2.cvc \
+ datatype3.cvc \
datatype4.cvc \
datatype13.cvc \
empty_tuprec.cvc \
tuple-no-clash.cvc \
jsat-2.6.smt2
+# rec5 -- no longer support subrange types
FAILING_TESTS = \
- datatype-dump.cvc
-
-# takes a long time to build model on debug : datatype3.cvc
+ datatype-dump.cvc \
+ rec5.cvc
EXTRA_DIST = $(TESTS)
projects / cvc5.git / commitdiff