#include "smt/command.h"
#include "util/bitvector.h"
#include "util/sexpr.h"
-#include "util/subrange_bound.h"
using namespace std;
}
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);
- CompatCheckArgument(noUpperBound || (r.getKind() == CVC4::kind::CONST_RATIONAL && r.getConst<Rational>().isIntegral()), r);
- 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!)");
}
%include "util/result.i"
%include "util/sexpr.i"
%include "util/statistics.i"
-%include "util/subrange_bound.i"
%include "util/tuple.i"
%include "util/unsafe_interrupt_exception.i"
%template(getConstBitVectorSize) CVC4::Expr::getConst<CVC4::BitVectorSize>;
%template(getConstAscriptionType) CVC4::Expr::getConst<CVC4::AscriptionType>;
%template(getConstBitVectorBitOf) CVC4::Expr::getConst<CVC4::BitVectorBitOf>;
-%template(getConstSubrangeBounds) CVC4::Expr::getConst<CVC4::SubrangeBounds>;
%template(getConstBitVectorRepeat) CVC4::Expr::getConst<CVC4::BitVectorRepeat>;
%template(getConstBitVectorExtract) CVC4::Expr::getConst<CVC4::BitVectorExtract>;
%template(getConstBitVectorRotateLeft) CVC4::Expr::getConst<CVC4::BitVectorRotateLeft>;
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorSize>;
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::AscriptionType>;
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorBitOf>;
-%template(mkConst) CVC4::ExprManager::mkConst<CVC4::SubrangeBounds>;
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorRepeat>;
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorExtract>;
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorRotateLeft>;
#include "expr/kind.h"
#include "expr/type.h"
#include "util/statistics.h"
-#include "util/subrange_bound.h"
${includes}
// compiler directs the user to the template file instead of the
// generated one. We don't want the user to modify the generated one,
// since it'll get overwritten on a later build.
-#line 37 "${template}"
+#line 36 "${template}"
namespace CVC4 {
//Type mkPredicateSubtype(Expr lambda, Expr witness)
// throw(TypeCheckingException);
- /**
- * Make an integer subrange type as defined by the argument.
- */
- //Type mkSubrangeType(const SubrangeBounds& bounds)
- // throw(TypeCheckingException);
-
/** Get the type of an expression */
Type getType(Expr e, bool check = false)
throw(TypeCheckingException);
#include "expr/kind.h"
#include "expr/metakind.h"
#include "expr/node_value.h"
-#include "util/subrange_bound.h"
#include "options/options.h"
namespace CVC4 {
#include <stdint.h>
#include "util/cardinality.h"
-#include "util/subrange_bound.h"
namespace CVC4 {
Type getParentType() const;
};/* class PredicateSubtype */
-
-/**
- * Class encapsulating an integer subrange type.
- */
-class CVC4_PUBLIC SubrangeType : public Type {
-
-public:
-
- /** Construct from the base type */
- SubrangeType(const Type& type = Type()) throw(IllegalArgumentException);
-
- /** Get the bounds defining this integer subrange */
- SubrangeBounds getSubrangeBounds() const;
-
-};/* class SubrangeType */
#endif /* 0 */
/**
#include "parser/antlr_tracing.h"
#include "parser/parser.h"
#include "smt/command.h"
-#include "util/subrange_bound.h"
namespace CVC4 {
class Expr;
myString() : std::string() {}
};/* class myString */
- /**
- * Just exists to give us the void* construction that
- * ANTLR requires.
- */
- class mySubrangeBound : public CVC4::SubrangeBound {
- public:
- mySubrangeBound() : CVC4::SubrangeBound() {}
- mySubrangeBound(void*) : CVC4::SubrangeBound() {}
- mySubrangeBound(const Integer& i) : CVC4::SubrangeBound(i) {}
- mySubrangeBound(const SubrangeBound& b) : CVC4::SubrangeBound(b) {}
- };/* class mySubrangeBound */
-
/**
* Just exists to give us the void* construction that
* ANTLR requires.
}
/* subrange types */
- | LBRACKET k1=bound DOTDOT k2=bound RBRACKET
- { if(k1.hasBound() && k2.hasBound() &&
- k1.getBound() > k2.getBound()) {
- std::stringstream ss;
- ss << "Subrange [" << k1.getBound() << ".." << k2.getBound()
- << "] inappropriate: range must be nonempty!";
- PARSER_STATE->parseError(ss.str());
- }
+ | LBRACKET bound DOTDOT bound RBRACKET
+ {
PARSER_STATE->unimplementedFeature("subrange typing not supported in this release");
- //t = EXPR_MANAGER->mkSubrangeType(SubrangeBounds(k1, k2));
}
/* tuple types / old-style function types */
( COMMA restrictedType[t,check] { Debug("parser-param") << "t = " << t << std::endl; params.push_back( t ); } )* RBRACKET
;
-bound returns [CVC4::parser::cvc::mySubrangeBound bound]
- : UNDERSCORE { $bound = SubrangeBound(); }
- | k=integer { $bound = SubrangeBound(k.getNumerator()); }
+bound
+ : UNDERSCORE
+ | integer
;
typeLetDecl[CVC4::parser::DeclarationCheck check]
#ifndef __CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H
#define __CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H
-#include "util/subrange_bound.h"
-
namespace CVC4 {
namespace theory {
namespace arith {
statistics.h \
statistics_registry.cpp \
statistics_registry.h \
- subrange_bound.cpp \
- subrange_bound.h \
tuple.h \
unsafe_interrupt_exception.h \
utility.h
result.i \
sexpr.i \
statistics.i \
- subrange_bound.i \
tuple.i \
unsafe_interrupt_exception.i
+++ /dev/null
-/********************* */
-/*! \file subrange_bound.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Tim King
- ** 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 subrange bounds
- **
- ** Simple class to represent a subrange bound, either infinite
- ** (no bound) or finite (an arbitrary precision integer).
- **/
-
-#include "util/subrange_bound.h"
-
-#include <limits>
-
-#include "base/cvc4_assert.h"
-#include "base/exception.h"
-#include "util/integer.h"
-
-namespace CVC4 {
-
-std::ostream& operator<<(std::ostream& out, const SubrangeBounds& bounds) {
- out << bounds.lower << ".." << bounds.upper;
-
- return out;
-}
-
-/** Get the finite SubrangeBound, failing an assertion if infinite. */
-const Integer& SubrangeBound::getBound() const {
- PrettyCheckArgument(!d_nobound, this, "SubrangeBound is infinite");
- return d_bound;
-}
-
-SubrangeBounds::SubrangeBounds(const SubrangeBound& l, const SubrangeBound& u)
- : lower(l), upper(u) {
- PrettyCheckArgument(
- !l.hasBound() || !u.hasBound() || l.getBound() <= u.getBound(), l,
- "Bad subrange bounds specified");
-}
-
-bool SubrangeBounds::joinIsBounded(const SubrangeBounds& a,
- const SubrangeBounds& b) {
- return (a.lower.hasBound() && b.lower.hasBound()) ||
- (a.upper.hasBound() && b.upper.hasBound());
-}
-
-SubrangeBounds SubrangeBounds::join(const SubrangeBounds& a,
- const SubrangeBounds& b) {
- DebugCheckArgument(joinIsBounded(a, b), a);
- SubrangeBound newLower = SubrangeBound::min(a.lower, b.lower);
- SubrangeBound newUpper = SubrangeBound::max(a.upper, b.upper);
- return SubrangeBounds(newLower, newUpper);
-}
-
-} /* namespace CVC4 */
+++ /dev/null
-/********************* */
-/*! \file subrange_bound.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Morgan Deters, Tim King
- ** 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 subrange bounds
- **
- ** Simple class to represent a subrange bound, either infinite
- ** (no bound) or finite (an arbitrary precision integer).
- **/
-
-#include "cvc4_public.h"
-
-#ifndef __CVC4__SUBRANGE_BOUND_H
-#define __CVC4__SUBRANGE_BOUND_H
-
-#include <limits>
-
-#include "base/exception.h"
-#include "util/integer.h"
-
-namespace CVC4 {
-
-/**
- * Representation of a subrange bound. A bound can either exist and be
- * a finite arbitrary-precision integer, or not exist (and thus be
- * an infinite bound). For example, the CVC language subrange [-5.._]
- * has a lower bound of -5 and an infinite upper bound.
- */
-class CVC4_PUBLIC SubrangeBound {
- public:
- /** Construct an infinite SubrangeBound. */
- SubrangeBound() : d_nobound(true), d_bound() {}
-
- /** Construct a finite SubrangeBound. */
- SubrangeBound(const Integer& i) : d_nobound(false), d_bound(i) {}
-
- ~SubrangeBound() {}
-
- /**
- * Get the finite SubrangeBound, failing an assertion if infinite.
- *
- * @throws IllegalArgumentException if the bound is infinite.
- */
- const Integer& getBound() const;
-
- /** Returns true iff this is a finite SubrangeBound. */
- bool hasBound() const { return !d_nobound; }
-
- /** Test two SubrangeBounds for equality. */
- bool operator==(const SubrangeBound& b) const {
- return hasBound() == b.hasBound() &&
- (!hasBound() || getBound() == b.getBound());
- }
-
- /** Test two SubrangeBounds for disequality. */
- bool operator!=(const SubrangeBound& b) const { return !(*this == b); }
-
- /**
- * Is this SubrangeBound "less than" another? For two
- * SubrangeBounds that "have bounds," this is defined as expected.
- * For a finite SubrangeBound b1 and a SubrangeBounds b2 without a
- * bound, b1 < b2 (but note also that b1 > b2). This strange
- * behavior is due to the fact that a SubrangeBound without a bound
- * is the representation for both +infinity and -infinity.
- */
- bool operator<(const SubrangeBound& b) const {
- return (!hasBound() && b.hasBound()) || (hasBound() && !b.hasBound()) ||
- (hasBound() && b.hasBound() && getBound() < b.getBound());
- }
-
- /**
- * Is this SubrangeBound "less than or equal to" another? For two
- * SubrangeBounds that "have bounds," this is defined as expected.
- * For a finite SubrangeBound b1 and a SubrangeBounds b2 without a
- * bound, b1 < b2 (but note also that b1 > b2). This strange
- * behavior is due to the fact that a SubrangeBound without a bound
- * is the representation for both +infinity and -infinity.
- */
- bool operator<=(const SubrangeBound& b) const {
- return !hasBound() || !b.hasBound() ||
- (hasBound() && b.hasBound() && getBound() <= b.getBound());
- }
-
- /**
- * Is this SubrangeBound "greater than" another? For two
- * SubrangeBounds that "have bounds," this is defined as expected.
- * For a finite SubrangeBound b1 and a SubrangeBounds b2 without a
- * bound, b1 > b2 (but note also that b1 < b2). This strange
- * behavior is due to the fact that a SubrangeBound without a bound
- * is the representation for both +infinity and -infinity.
- */
- bool operator>(const SubrangeBound& b) const {
- return (!hasBound() && b.hasBound()) || (hasBound() && !b.hasBound()) ||
- (hasBound() && b.hasBound() && getBound() < b.getBound());
- }
-
- /**
- * Is this SubrangeBound "greater than or equal to" another? For
- * two SubrangeBounds that "have bounds," this is defined as
- * expected. For a finite SubrangeBound b1 and a SubrangeBounds b2
- * without a bound, b1 > b2 (but note also that b1 < b2). This
- * strange behavior is due to the fact that a SubrangeBound without
- * a bound is the representation for both +infinity and -infinity.
- */
- bool operator>=(const SubrangeBound& b) const {
- return !hasBound() || !b.hasBound() ||
- (hasBound() && b.hasBound() && getBound() <= b.getBound());
- }
-
- static SubrangeBound min(const SubrangeBound& a, const SubrangeBound& b) {
- if (a.hasBound() && b.hasBound()) {
- return SubrangeBound(Integer::min(a.getBound(), b.getBound()));
- } else {
- return SubrangeBound();
- }
- }
-
- static SubrangeBound max(const SubrangeBound& a, const SubrangeBound& b) {
- if (a.hasBound() && b.hasBound()) {
- return SubrangeBound(Integer::max(a.getBound(), b.getBound()));
- } else {
- return SubrangeBound();
- }
- }
-
- private:
- bool d_nobound;
- Integer d_bound;
-}; /* class SubrangeBound */
-
-class CVC4_PUBLIC SubrangeBounds {
- public:
- SubrangeBound lower;
- SubrangeBound upper;
-
- SubrangeBounds(const SubrangeBound& l, const SubrangeBound& u);
-
- bool operator==(const SubrangeBounds& bounds) const {
- return lower == bounds.lower && upper == bounds.upper;
- }
-
- bool operator!=(const SubrangeBounds& bounds) const {
- return !(*this == bounds);
- }
-
- /**
- * Is this pair of SubrangeBounds "less than" (contained inside) the
- * given pair of SubrangeBounds? Think of this as a subtype
- * relation, e.g., [0,2] < [0,3]
- */
- bool operator<(const SubrangeBounds& bounds) const {
- return (lower > bounds.lower && upper <= bounds.upper) ||
- (lower >= bounds.lower && upper < bounds.upper);
- }
-
- /**
- * Is this pair of SubrangeBounds "less than or equal" (contained
- * inside) the given pair of SubrangeBounds? Think of this as a
- * subtype relation, e.g., [0,2] < [0,3]
- */
- bool operator<=(const SubrangeBounds& bounds) const {
- return lower >= bounds.lower && upper <= bounds.upper;
- }
-
- /**
- * Is this pair of SubrangeBounds "greater than" (does it contain)
- * the given pair of SubrangeBounds? Think of this as a supertype
- * relation, e.g., [0,3] > [0,2]
- */
- bool operator>(const SubrangeBounds& bounds) const {
- return (lower < bounds.lower && upper >= bounds.upper) ||
- (lower <= bounds.lower && upper > bounds.upper);
- }
-
- /**
- * Is this pair of SubrangeBounds "greater than" (does it contain)
- * the given pair of SubrangeBounds? Think of this as a supertype
- * relation, e.g., [0,3] > [0,2]
- */
- bool operator>=(const SubrangeBounds& bounds) const {
- return lower <= bounds.lower && upper >= bounds.upper;
- }
-
- /**
- * Returns true if the join of two subranges is not (- infinity, + infinity).
- */
- static bool joinIsBounded(const SubrangeBounds& a, const SubrangeBounds& b);
-
- /**
- * Returns the join of two subranges, a and b.
- * precondition: joinIsBounded(a,b) is true
- */
- static SubrangeBounds join(const SubrangeBounds& a, const SubrangeBounds& b);
-
-}; /* class SubrangeBounds */
-
-struct CVC4_PUBLIC SubrangeBoundsHashFunction {
- inline size_t operator()(const SubrangeBounds& bounds) const {
- // We use Integer::hash() rather than Integer::getUnsignedLong()
- // because the latter might overflow and throw an exception
- size_t l = bounds.lower.hasBound() ? bounds.lower.getBound().hash()
- : std::numeric_limits<size_t>::max();
- size_t u = bounds.upper.hasBound() ? bounds.upper.getBound().hash()
- : std::numeric_limits<size_t>::max();
- return l + 0x9e3779b9 + (u << 6) + (u >> 2);
- }
-}; /* struct SubrangeBoundsHashFunction */
-
-inline std::ostream& operator<<(std::ostream& out,
- const SubrangeBound& bound) CVC4_PUBLIC;
-
-inline std::ostream& operator<<(std::ostream& out, const SubrangeBound& bound) {
- if (bound.hasBound()) {
- out << bound.getBound();
- } else {
- out << '_';
- }
-
- return out;
-}
-
-std::ostream& operator<<(std::ostream& out,
- const SubrangeBounds& bounds) CVC4_PUBLIC;
-
-} /* CVC4 namespace */
-
-#endif /* __CVC4__SUBRANGE_BOUND_H */
+++ /dev/null
-%{
-#include "util/subrange_bound.h"
-%}
-
-%rename(equals) CVC4::SubrangeBound::operator==(const SubrangeBound&) const;
-%ignore CVC4::SubrangeBound::operator!=(const SubrangeBound&) const;
-%rename(less) CVC4::SubrangeBound::operator<(const SubrangeBound&) const;
-%rename(lessEqual) CVC4::SubrangeBound::operator<=(const SubrangeBound&) const;
-%rename(greater) CVC4::SubrangeBound::operator>(const SubrangeBound&) const;
-%rename(greaterEqual) CVC4::SubrangeBound::operator>=(const SubrangeBound&) const;
-
-%rename(equals) CVC4::SubrangeBounds::operator==(const SubrangeBounds&) const;
-%ignore CVC4::SubrangeBounds::operator!=(const SubrangeBounds&) const;
-%rename(less) CVC4::SubrangeBounds::operator<(const SubrangeBounds&) const;
-%rename(lessEqual) CVC4::SubrangeBounds::operator<=(const SubrangeBounds&) const;
-%rename(greater) CVC4::SubrangeBounds::operator>(const SubrangeBounds&) const;
-%rename(greaterEqual) CVC4::SubrangeBounds::operator>=(const SubrangeBounds&) const;
-
-%rename(apply) CVC4::SubrangeBoundsHashFunction::operator()(const SubrangeBounds&) const;
-
-%ignore CVC4::operator<<(std::ostream&, const SubrangeBound&);
-%ignore CVC4::operator<<(std::ostream&, const SubrangeBounds&);
-
-%include "util/subrange_bound.h"
TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(1, 7)));
TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-1, 7)));
TS_ASSERT( ! te.isFinished() );
-/*
- // subrange bounded only below
- te = TypeEnumerator(d_nm->mkSubrangeType(SubrangeBounds(SubrangeBound(Integer(0)), SubrangeBound())));
- TS_ASSERT( ! te.isFinished() );
- TS_ASSERT_EQUALS(*te, d_nm->mkConst(Rational(0)));
- for(int i = 1; i <= 100; ++i) {
- TS_ASSERT( ! (++te).isFinished() );
- TS_ASSERT_EQUALS(*te, d_nm->mkConst(Rational(i)));
- }
- TS_ASSERT( ! te.isFinished() );
-
- // subrange bounded only above
- te = TypeEnumerator(d_nm->mkSubrangeType(SubrangeBounds(SubrangeBound(), SubrangeBound(Integer(-5)))));
- TS_ASSERT( ! te.isFinished() );
- TS_ASSERT_EQUALS(*te, d_nm->mkConst(Rational(-5)));
- for(int i = 1; i <= 100; ++i) {
- TS_ASSERT( ! (++te).isFinished() );
- TS_ASSERT_EQUALS(*te, d_nm->mkConst(Rational(-5 - i)));
- }
- TS_ASSERT( ! te.isFinished() );
-
- // finite subrange
- te = TypeEnumerator(d_nm->mkSubrangeType(SubrangeBounds(SubrangeBound(Integer(-10)), SubrangeBound(Integer(15)))));
- TS_ASSERT( ! te.isFinished() );
- TS_ASSERT_EQUALS(*te, d_nm->mkConst(Rational(-10)));
- for(int i = -9; i <= 15; ++i) {
- TS_ASSERT( ! (++te).isFinished() );
- TS_ASSERT_EQUALS(*te, d_nm->mkConst(Rational(i)));
- }
- TS_ASSERT( (++te).isFinished() );
- TS_ASSERT_THROWS(*te, NoMoreValuesException);
-std::cout<<"here\n";
- TS_ASSERT_THROWS(*++te, NoMoreValuesException);
- */
}
void testDatatypesFinite() {
projects / cvc5.git / commitdiff