diff options
Diffstat (limited to 'src/util')
62 files changed, 831 insertions, 750 deletions
diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index eba5fb8c9..028288dbc 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -17,6 +17,7 @@ libcvc4_add_sources( floatingpoint.cpp gmp_util.h hash.h + iand.h index.cpp index.h maybe.h diff --git a/src/util/abstract_value.cpp b/src/util/abstract_value.cpp index 49247ee38..e004a22a7 100644 --- a/src/util/abstract_value.cpp +++ b/src/util/abstract_value.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/util/abstract_value.h b/src/util/abstract_value.h index 8091a7ee5..f1fe9f575 100644 --- a/src/util/abstract_value.h +++ b/src/util/abstract_value.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/util/bin_heap.h b/src/util/bin_heap.h index 7ada9a655..d7d3a8e18 100644 --- a/src/util/bin_heap.h +++ b/src/util/bin_heap.h @@ -2,9 +2,9 @@ /*! \file bin_heap.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Andres Noetzli + ** Tim King, Morgan Deters, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/util/bitvector.cpp b/src/util/bitvector.cpp index a561fe088..3f3327c93 100644 --- a/src/util/bitvector.cpp +++ b/src/util/bitvector.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Aina Niemetz, Liana Hadarean, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/util/bitvector.h b/src/util/bitvector.h index a75339112..8e11d2465 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -2,9 +2,9 @@ /*! \file bitvector.h ** \verbatim ** Top contributors (to current version): - ** Aina Niemetz, Dejan Jovanovic, Morgan Deters + ** Aina Niemetz, Andres Noetzli, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/util/bool.h b/src/util/bool.h index 32f3741f8..5779f073b 100644 --- a/src/util/bool.h +++ b/src/util/bool.h @@ -2,9 +2,9 @@ /*! \file bool.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters + ** Morgan Deters, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/util/cardinality.cpp b/src/util/cardinality.cpp index 6615f8378..e7c0ac01c 100644 --- a/src/util/cardinality.cpp +++ b/src/util/cardinality.cpp @@ -2,9 +2,9 @@ /*! \file cardinality.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Tim King + ** Morgan Deters, Tim King, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/util/cardinality.h b/src/util/cardinality.h index b06d72286..d1b003300 100644 --- a/src/util/cardinality.h +++ b/src/util/cardinality.h @@ -2,9 +2,9 @@ /*! \file cardinality.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Tim King, Andrew Reynolds + ** Morgan Deters, Tim King, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/util/dense_map.h b/src/util/dense_map.h index 08da8faaa..8e5f5f9cf 100644 --- a/src/util/dense_map.h +++ b/src/util/dense_map.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Dejan Jovanovic, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/util/divisible.cpp b/src/util/divisible.cpp index c89886fa8..a218642d7 100644 --- a/src/util/divisible.cpp +++ b/src/util/divisible.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/util/divisible.h b/src/util/divisible.h index a0c730436..bb2370f0b 100644 --- a/src/util/divisible.h +++ b/src/util/divisible.h @@ -2,9 +2,9 @@ /*! \file divisible.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters + ** Morgan Deters, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp index f5545f73c..7403c340b 100644 --- a/src/util/floatingpoint.cpp +++ b/src/util/floatingpoint.cpp @@ -2,10 +2,10 @@ /*! \file floatingpoint.cpp ** \verbatim ** Top contributors (to current version): - ** Martin Brain, Martin Brain, Tim King + ** Martin Brain, Haniel Barbosa, Mathias Preiner ** Copyright (c) 2013 University of Oxford ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 @@ -959,6 +959,41 @@ static FloatingPointLiteral constructorHelperBitVector( return bv; } - +std::string FloatingPoint::toString(bool printAsIndexed) const +{ + std::string str; + // retrive BV value + BitVector bv(pack()); + unsigned largestSignificandBit = + t.significand() - 2; // -1 for -inclusive, -1 for hidden + unsigned largestExponentBit = + (t.exponent() - 1) + (largestSignificandBit + 1); + BitVector v[3]; + v[0] = bv.extract(largestExponentBit + 1, largestExponentBit + 1); + v[1] = bv.extract(largestExponentBit, largestSignificandBit + 1); + v[2] = bv.extract(largestSignificandBit, 0); + str.append("(fp "); + for (unsigned i = 0; i < 3; ++i) + { + if (printAsIndexed) + { + str.append("(_ bv"); + str.append(v[i].getValue().toString()); + str.append(" "); + str.append(std::to_string(v[i].getSize())); + str.append(")"); + } + else + { + str.append("#b"); + str.append(v[i].toString()); + } + if (i < 2) + { + str.append(" "); + } + } + return str; +} }/* CVC4 namespace */ diff --git a/src/util/floatingpoint.h.in b/src/util/floatingpoint.h.in index bac0fbd59..d38cae5fa 100644 --- a/src/util/floatingpoint.h.in +++ b/src/util/floatingpoint.h.in @@ -2,10 +2,10 @@ /*! \file floatingpoint.h.in ** \verbatim ** Top contributors (to current version): - ** Martin Brain, Martin Brain, Tim King + ** Martin Brain, Haniel Barbosa, Tim King ** Copyright (c) 2013 University of Oxford ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 @@ -333,6 +333,13 @@ namespace CVC4 { return this->fpl; } + /* Return string representation. + * + * If printAsIndexed is true then it prints + * the bit-vector components of the FP value as indexed symbols, otherwise + * in binary notation. */ + std::string toString(bool printAsIndexed = false) const; + // Gives the corresponding IEEE-754 transfer format BitVector pack (void) const; @@ -526,17 +533,10 @@ namespace CVC4 { */ inline std::ostream& operator <<(std::ostream& os, const FloatingPoint& fp) CVC4_PUBLIC; - inline std::ostream& operator <<(std::ostream& os, const FloatingPoint& fp) { - BitVector bv(fp.pack()); - - unsigned largestSignificandBit = fp.t.significand() - 2; // -1 for -inclusive, -1 for hidden - unsigned largestExponentBit = (fp.t.exponent() - 1) + (largestSignificandBit + 1); - - return os - << "(fp #b" << bv.extract(largestExponentBit + 1, largestExponentBit + 1) - << " #b" << bv.extract(largestExponentBit, largestSignificandBit + 1) - << " #b" << bv.extract(largestSignificandBit, 0) - << ")"; + inline std::ostream& operator<<(std::ostream& os, const FloatingPoint& fp) + { + // print in binary notation + return os << fp.toString(); } inline std::ostream& operator <<(std::ostream& os, const FloatingPointSize& fps) CVC4_PUBLIC; diff --git a/src/util/gmp_util.h b/src/util/gmp_util.h index 3ba388564..bde7b50a8 100644 --- a/src/util/gmp_util.h +++ b/src/util/gmp_util.h @@ -2,9 +2,9 @@ /*! \file gmp_util.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Andres Noetzli, Morgan Deters + ** Tim King, Andres Noetzli, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/util/hash.h b/src/util/hash.h index 14167bc82..548fb3afc 100644 --- a/src/util/hash.h +++ b/src/util/hash.h @@ -2,9 +2,9 @@ /*! \file hash.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Andres Noetzli + ** Morgan Deters, Andres Noetzli, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/util/iand.h b/src/util/iand.h new file mode 100644 index 000000000..b5bc92960 --- /dev/null +++ b/src/util/iand.h @@ -0,0 +1,47 @@ +/********************* */ +/*! \file iand.h + ** \verbatim + ** Top contributors (to current version): + ** Anrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 The integer AND operator. + **/ + +#include "cvc4_public.h" + +#ifndef CVC4__IAND_H +#define CVC4__IAND_H + +#include <cstdint> +#include <iosfwd> + +#include "base/exception.h" +#include "util/integer.h" + +namespace CVC4 { + +struct CVC4_PUBLIC IntAnd +{ + unsigned d_size; + IntAnd(unsigned size) : d_size(size) {} + operator unsigned() const { return d_size; } +}; /* struct IntAnd */ + +/* ----------------------------------------------------------------------- + ** Output stream + * ----------------------------------------------------------------------- */ + +inline std::ostream& operator<<(std::ostream& os, const IntAnd& ia) CVC4_PUBLIC; +inline std::ostream& operator<<(std::ostream& os, const IntAnd& ia) +{ + return os << "[" << ia.d_size << "]"; +} + +} // namespace CVC4 + +#endif /* CVC4__IAND_H */ diff --git a/src/util/iand.i b/src/util/iand.i new file mode 100644 index 000000000..92c5a1223 --- /dev/null +++ b/src/util/iand.i @@ -0,0 +1,9 @@ +%{ +#include "util/iand.h" +%} + +%rename(toUnsigned) CVC4::IntAnd::operator unsigned() const; + +%ignore CVC4::operator<<(std::ostream&, const IntAnd&); + +%include "util/iand.h" diff --git a/src/util/index.cpp b/src/util/index.cpp index 6f036d537..3d9877135 100644 --- a/src/util/index.cpp +++ b/src/util/index.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/util/index.h b/src/util/index.h index 2ee6ff19e..05227f0d3 100644 --- a/src/util/index.h +++ b/src/util/index.h @@ -2,9 +2,9 @@ /*! \file index.h ** \verbatim ** Top contributors (to current version): - ** Tim King + ** Mathias Preiner, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/util/integer.h.in b/src/util/integer.h.in index 87a5e35d3..f13f68a82 100644 --- a/src/util/integer.h.in +++ b/src/util/integer.h.in @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/util/integer_cln_imp.cpp b/src/util/integer_cln_imp.cpp index 5cca2fcba..ca59822a7 100644 --- a/src/util/integer_cln_imp.cpp +++ b/src/util/integer_cln_imp.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Aina Niemetz, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h index aba5b6a3a..ff4bcdf69 100644 --- a/src/util/integer_cln_imp.h +++ b/src/util/integer_cln_imp.h @@ -2,9 +2,9 @@ /*! \file integer_cln_imp.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Liana Hadarean + ** Tim King, Gereon Kremer, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 @@ -24,6 +24,7 @@ #include <cln/integer.h> #include <cln/integer_io.h> #include <cln/modinteger.h> + #include <iostream> #include <limits> #include <sstream> @@ -35,53 +36,22 @@ namespace CVC4 { class Rational; -class CVC4_PUBLIC Integer { -private: - /** - * Stores the value of the rational is stored in a C++ CLN integer class. - */ - cln::cl_I d_value; - - /** - * Gets a reference to the cln data that backs up the integer. - * Only accessible to friend classes. - */ - const cln::cl_I& get_cl_I() const { return d_value; } +class CVC4_PUBLIC Integer +{ + friend class CVC4::Rational; + public: /** * Constructs an Integer by copying a CLN C++ primitive. */ Integer(const cln::cl_I& val) : d_value(val) {} - // Throws a std::invalid_argument on invalid input `s` for the given base. - void readInt(const cln::cl_read_flags& flags, - const std::string& s, - unsigned base); - - // Throws a std::invalid_argument on invalid inputs. - void parseInt(const std::string& s, unsigned base); - - // These constants are to help with CLN conversion in 32 bit. - // See http://www.ginac.de/CLN/cln.html#Conversions - static signed int s_fastSignedIntMax; /* 2^29 - 1 */ - static signed int s_fastSignedIntMin; /* -2^29 */ - static unsigned int s_fastUnsignedIntMax; /* 2^29 - 1 */ - - static signed long s_slowSignedIntMax; /* std::numeric_limits<signed int>::max() */ - static signed long s_slowSignedIntMin; /* std::numeric_limits<signed int>::min() */ - static unsigned long s_slowUnsignedIntMax; /* std::numeric_limits<unsigned int>::max() */ - static unsigned long s_signedLongMin; - static unsigned long s_signedLongMax; - static unsigned long s_unsignedLongMax; -public: /** Constructs a rational with the value 0. */ - Integer() : d_value(0){} + Integer() : d_value(0) {} /** * Constructs a Integer from a C string. - * Throws std::invalid_argument if the string is not a valid rational. - * For more information about what is a valid rational string, - * see GMP's documentation for mpq_set_str(). + * Throws std::invalid_argument if the string is not a valid integer. */ explicit Integer(const char* sp, unsigned base = 10) { @@ -95,13 +65,13 @@ public: Integer(const Integer& q) : d_value(q.d_value) {} - Integer( signed int z) : d_value((signed long int)z) {} + Integer(signed int z) : d_value((signed long int)z) {} Integer(unsigned int z) : d_value((unsigned long int)z) {} - Integer( signed long int z) : d_value(z) {} + Integer(signed long int z) : d_value(z) {} Integer(unsigned long int z) : d_value(z) {} #ifdef CVC4_NEED_INT64_T_OVERLOADS - Integer( int64_t z) : d_value(static_cast<long>(z)) {} + Integer(int64_t z) : d_value(static_cast<long>(z)) {} Integer(uint64_t z) : d_value(static_cast<unsigned long>(z)) {} #endif /* CVC4_NEED_INT64_T_OVERLOADS */ @@ -110,103 +80,90 @@ public: /** * Returns a copy of d_value to enable public access of CLN data. */ - cln::cl_I getValue() const - { - return d_value; - } + const cln::cl_I& getValue() const { return d_value; } - Integer& operator=(const Integer& x){ - if(this == &x) return *this; + Integer& operator=(const Integer& x) + { + if (this == &x) return *this; d_value = x.d_value; return *this; } - bool operator==(const Integer& y) const { - return d_value == y.d_value; - } - - Integer operator-() const{ - return Integer(-(d_value)); - } + bool operator==(const Integer& y) const { return d_value == y.d_value; } + Integer operator-() const { return Integer(-(d_value)); } - bool operator!=(const Integer& y) const { - return d_value != y.d_value; - } + bool operator!=(const Integer& y) const { return d_value != y.d_value; } - bool operator< (const Integer& y) const { - return d_value < y.d_value; - } + bool operator<(const Integer& y) const { return d_value < y.d_value; } - bool operator<=(const Integer& y) const { - return d_value <= y.d_value; - } + bool operator<=(const Integer& y) const { return d_value <= y.d_value; } - bool operator> (const Integer& y) const { - return d_value > y.d_value; - } + bool operator>(const Integer& y) const { return d_value > y.d_value; } - bool operator>=(const Integer& y) const { - return d_value >= y.d_value; - } + bool operator>=(const Integer& y) const { return d_value >= y.d_value; } - - Integer operator+(const Integer& y) const { - return Integer( d_value + y.d_value ); + Integer operator+(const Integer& y) const + { + return Integer(d_value + y.d_value); } - Integer& operator+=(const Integer& y) { + 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) const + { + return Integer(d_value - y.d_value); } - Integer& operator-=(const Integer& y) { + 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) const + { + return Integer(d_value * y.d_value); } - Integer& operator*=(const Integer& y) { + Integer& operator*=(const Integer& y) + { d_value *= y.d_value; return *this; } - - Integer bitwiseOr(const Integer& y) const { + Integer bitwiseOr(const Integer& y) const + { return Integer(cln::logior(d_value, y.d_value)); } - Integer bitwiseAnd(const Integer& y) const { + Integer bitwiseAnd(const Integer& y) const + { return Integer(cln::logand(d_value, y.d_value)); } - Integer bitwiseXor(const Integer& y) const { + Integer bitwiseXor(const Integer& y) const + { return Integer(cln::logxor(d_value, y.d_value)); } - Integer bitwiseNot() const { - return Integer(cln::lognot(d_value)); - } - + Integer bitwiseNot() const { return Integer(cln::lognot(d_value)); } /** * Return this*(2^pow). */ - Integer multiplyByPow2(uint32_t pow) const { + Integer multiplyByPow2(uint32_t pow) const + { cln::cl_I ipow(pow); - return Integer( d_value << ipow); + return Integer(d_value << ipow); } - bool isBitSet(uint32_t i) const { - return !extractBitRange(1, i).isZero(); - } + bool isBitSet(uint32_t i) const { return !extractBitRange(1, i).isZero(); } - Integer setBit(uint32_t i) const { + Integer setBit(uint32_t i) const + { cln::cl_I mask(1); mask = mask << i; return Integer(cln::logior(d_value, mask)); @@ -214,13 +171,11 @@ public: Integer oneExtend(uint32_t size, uint32_t amount) const; - uint32_t toUnsignedInt() const { - return cln::cl_I_to_uint(d_value); - } - + uint32_t toUnsignedInt() const { return cln::cl_I_to_uint(d_value); } /** See CLN Documentation. */ - Integer extractBitRange(uint32_t bitCount, uint32_t low) const { + Integer extractBitRange(uint32_t bitCount, uint32_t low) const + { cln::cl_byte range(bitCount, low); return Integer(cln::ldb(d_value, range)); } @@ -228,20 +183,26 @@ public: /** * Returns the floor(this / y) */ - Integer floorDivideQuotient(const Integer& y) const { - return Integer( cln::floor1(d_value, y.d_value) ); + Integer floorDivideQuotient(const Integer& y) const + { + return Integer(cln::floor1(d_value, y.d_value)); } /** * Returns r == this - floor(this/y)*y */ - Integer floorDivideRemainder(const Integer& y) const { - return Integer( cln::floor2(d_value, y.d_value).remainder ); + Integer floorDivideRemainder(const Integer& y) const + { + return Integer(cln::floor2(d_value, y.d_value).remainder); } - /** + /** * Computes a floor quoient and remainder for x divided by y. */ - static void floorQR(Integer& q, Integer& r, const Integer& x, const Integer& y) { + static void floorQR(Integer& q, + Integer& r, + const Integer& x, + const Integer& y) + { cln::cl_I_div_t res = cln::floor2(x.d_value, y.d_value); q.d_value = res.quotient; r.d_value = res.remainder; @@ -250,43 +211,53 @@ public: /** * Returns the ceil(this / y) */ - Integer ceilingDivideQuotient(const Integer& y) const { - return Integer( cln::ceiling1(d_value, y.d_value) ); + Integer ceilingDivideQuotient(const Integer& y) const + { + return Integer(cln::ceiling1(d_value, y.d_value)); } /** * Returns the ceil(this / y) */ - Integer ceilingDivideRemainder(const Integer& y) const { - return Integer( cln::ceiling2(d_value, y.d_value).remainder ); + Integer ceilingDivideRemainder(const Integer& y) const + { + return Integer(cln::ceiling2(d_value, y.d_value).remainder); } /** - * Computes a quoitent and remainder according to Boute's Euclidean definition. - * euclidianDivideQuotient, euclidianDivideRemainder. + * Computes a quoitent and remainder according to Boute's Euclidean + * definition. euclidianDivideQuotient, euclidianDivideRemainder. * * Boute, Raymond T. (April 1992). * The Euclidean definition of the functions div and mod. * ACM Transactions on Programming Languages and Systems (TOPLAS) * ACM Press. 14 (2): 127 - 144. doi:10.1145/128861.128862. */ - static void euclidianQR(Integer& q, Integer& r, const Integer& x, const Integer& y) { + static void euclidianQR(Integer& q, + Integer& r, + const Integer& x, + const Integer& y) + { // compute the floor and then fix the value up if needed. - floorQR(q,r,x,y); + floorQR(q, r, x, y); - if(r.strictlyNegative()){ + if (r.strictlyNegative()) + { // if r < 0 // abs(r) < abs(y) // - abs(y) < r < 0, then 0 < r + abs(y) < abs(y) // n = y * q + r // n = y * q - abs(y) + r + abs(y) - if(r.sgn() >= 0){ + if (r.sgn() >= 0) + { // y = abs(y) // n = y * q - y + r + y // n = y * (q-1) + (r+y) q -= 1; r += y; - }else{ + } + else + { // y = -abs(y) // n = y * q + y + r - y // n = y * (q+1) + (r-y) @@ -300,9 +271,10 @@ public: * Returns the quoitent according to Boute's Euclidean definition. * See the documentation for euclidianQR. */ - Integer euclidianDivideQuotient(const Integer& y) const { - Integer q,r; - euclidianQR(q,r, *this, y); + Integer euclidianDivideQuotient(const Integer& y) const + { + Integer q, r; + euclidianQR(q, r, *this, y); return q; } @@ -310,9 +282,10 @@ public: * Returns the remainfing according to Boute's Euclidean definition. * See the documentation for euclidianQR. */ - Integer euclidianDivideRemainder(const Integer& y) const { - Integer q,r; - euclidianQR(q,r, *this, y); + Integer euclidianDivideRemainder(const Integer& y) const + { + Integer q, r; + euclidianQR(q, r, *this, y); return r; } @@ -321,14 +294,13 @@ public: */ Integer exactQuotient(const Integer& y) const; - Integer modByPow2(uint32_t exp) const { + Integer modByPow2(uint32_t exp) const + { cln::cl_byte range(exp, 0); return Integer(cln::ldb(d_value, range)); } - Integer divByPow2(uint32_t exp) const { - return d_value >> exp; - } + Integer divByPow2(uint32_t exp) const { return d_value >> exp; } /** * Raise this Integer to the power <code>exp</code>. @@ -340,7 +312,8 @@ public: /** * Return the greatest common divisor of this integer with another. */ - Integer gcd(const Integer& y) const { + Integer gcd(const Integer& y) const + { cln::cl_I result = cln::gcd(d_value, y.d_value); return Integer(result); } @@ -348,7 +321,8 @@ public: /** * Return the least common multiple of this integer with another. */ - Integer lcm(const Integer& y) const { + Integer lcm(const Integer& y) const + { cln::cl_I result = cln::lcm(d_value, y.d_value); return Integer(result); } @@ -380,7 +354,8 @@ public: /** * Return true if *this exactly divides y. */ - bool divides(const Integer& y) const { + bool divides(const Integer& y) const + { cln::cl_I result = cln::rem(y.d_value, d_value); return cln::zerop(result); } @@ -388,31 +363,24 @@ public: /** * Return the absolute value of this integer. */ - Integer abs() const { - return d_value >= 0 ? *this : -*this; - } + Integer abs() const { return d_value >= 0 ? *this : -*this; } - std::string toString(int base = 10) const{ + std::string toString(int base = 10) const + { std::stringstream ss; - switch(base){ - case 2: - fprintbinary(ss,d_value); - break; - case 8: - fprintoctal(ss,d_value); - break; - case 10: - fprintdecimal(ss,d_value); - break; - case 16: - fprinthexadecimal(ss,d_value); - break; - default: - throw Exception("Unhandled base in Integer::toString()"); + switch (base) + { + case 2: fprintbinary(ss, d_value); break; + case 8: fprintoctal(ss, d_value); break; + case 10: fprintdecimal(ss, d_value); break; + case 16: fprinthexadecimal(ss, d_value); break; + default: throw Exception("Unhandled base in Integer::toString()"); } std::string output = ss.str(); - for( unsigned i = 0; i <= output.length(); ++i){ - if(isalpha(output[i])){ + for (unsigned i = 0; i <= output.length(); ++i) + { + if (isalpha(output[i])) + { output.replace(i, 1, 1, tolower(output[i])); } } @@ -420,31 +388,21 @@ public: return output; } - int sgn() const { + int sgn() const + { cln::cl_I sgn = cln::signum(d_value); return cln::cl_I_to_int(sgn); } + inline bool strictlyPositive() const { return sgn() > 0; } - inline bool strictlyPositive() const { - return sgn() > 0; - } - - inline bool strictlyNegative() const { - return sgn() < 0; - } + inline bool strictlyNegative() const { return sgn() < 0; } - inline bool isZero() const { - return sgn() == 0; - } + inline bool isZero() const { return sgn() == 0; } - inline bool isOne() const { - return d_value == 1; - } + inline bool isOne() const { return d_value == 1; } - inline bool isNegativeOne() const { - return d_value == -1; - } + inline bool isNegativeOne() const { return d_value == -1; } /** fits the C "signed int" primitive */ bool fitsSignedInt() const; @@ -460,20 +418,26 @@ public: bool fitsUnsignedLong() const; - long getLong() const { + long getLong() const + { // ensure there isn't overflow - CheckArgument(d_value <= std::numeric_limits<long>::max(), this, + CheckArgument(d_value <= std::numeric_limits<long>::max(), + this, "Overflow detected in Integer::getLong()"); - CheckArgument(d_value >= std::numeric_limits<long>::min(), this, + CheckArgument(d_value >= std::numeric_limits<long>::min(), + this, "Overflow detected in Integer::getLong()"); return cln::cl_I_to_long(d_value); } - unsigned long getUnsignedLong() const { + unsigned long getUnsignedLong() const + { // ensure there isn't overflow - CheckArgument(d_value <= std::numeric_limits<unsigned long>::max(), this, + CheckArgument(d_value <= std::numeric_limits<unsigned long>::max(), + this, "Overflow detected in Integer::getUnsignedLong()"); - CheckArgument(d_value >= std::numeric_limits<unsigned long>::min(), this, + CheckArgument(d_value >= std::numeric_limits<unsigned long>::min(), + this, "Overflow detected in Integer::getUnsignedLong()"); return cln::cl_I_to_ulong(d_value); } @@ -482,9 +446,7 @@ public: * Computes the hash of the node from the first word of the * numerator, the denominator. */ - size_t hash() const { - return equal_hashcode(d_value); - } + size_t hash() const { return equal_hashcode(d_value); } /** * Returns true iff bit n is set. @@ -492,15 +454,14 @@ public: * @param n the bit to test (0 == least significant bit) * @return true if bit n is set in this integer; false otherwise */ - bool testBit(unsigned n) const { - return cln::logbitp(n, d_value); - } + bool testBit(unsigned n) const { return cln::logbitp(n, d_value); } /** * Returns k if the integer is equal to 2^(k-1) * @return k if the integer is equal to 2^(k-1) and 0 otherwise */ - unsigned isPow2() const { + unsigned isPow2() const + { if (d_value <= 0) return 0; // power2p returns n such that d_value = 2^(n-1) return cln::power2p(d_value); @@ -510,53 +471,101 @@ public: * If x != 0, returns the unique n s.t. 2^{n-1} <= abs(x) < 2^{n}. * If x == 0, returns 1. */ - size_t length() const { + size_t length() const + { int s = sgn(); - if(s == 0){ + if (s == 0) + { return 1; - }else if(s < 0){ + } + else if (s < 0) + { size_t len = cln::integer_length(d_value); - /*If this is -2^n, return len+1 not len to stay consistent with the definition above! - * From CLN's documentation of integer_length: - * This is the smallest n >= 0 such that -2^n <= x < 2^n. - * If x > 0, this is the unique n > 0 such that 2^(n-1) <= x < 2^n. + /*If this is -2^n, return len+1 not len to stay consistent with the + * definition above! From CLN's documentation of integer_length: This is + * the smallest n >= 0 such that -2^n <= x < 2^n. If x > 0, this is the + * unique n > 0 such that 2^(n-1) <= x < 2^n. */ size_t ord2 = cln::ord2(d_value); return (len == ord2) ? (len + 1) : len; - }else{ + } + else + { return cln::integer_length(d_value); } } -/* cl_I xgcd (const cl_I& a, const cl_I& b, cl_I* u, cl_I* v) */ -/* This function ("extended gcd") returns the greatest common divisor g of a and b and at the same time the representation of g as an integral linear combination of a and b: u and v with u*a+v*b = g, g >= 0. u and v will be normalized to be of smallest possible absolute value, in the following sense: If a and b are non-zero, and abs(a) != abs(b), u and v will satisfy the inequalities abs(u) <= abs(b)/(2*g), abs(v) <= abs(a)/(2*g). */ - static void extendedGcd(Integer& g, Integer& s, Integer& t, const Integer& a, const Integer& b){ + /* cl_I xgcd (const cl_I& a, const cl_I& b, cl_I* u, cl_I* v) */ + /* This function ("extended gcd") returns the greatest common divisor g of a + * and b and at the same time the representation of g as an integral linear + * combination of a and b: u and v with u*a+v*b = g, g >= 0. u and v will be + * normalized to be of smallest possible absolute value, in the following + * sense: If a and b are non-zero, and abs(a) != abs(b), u and v will satisfy + * the inequalities abs(u) <= abs(b)/(2*g), abs(v) <= abs(a)/(2*g). */ + static void extendedGcd( + Integer& g, Integer& s, Integer& t, const Integer& a, const Integer& b) + { g.d_value = cln::xgcd(a.d_value, b.d_value, &s.d_value, &t.d_value); } /** Returns a reference to the minimum of two integers. */ - static const Integer& min(const Integer& a, const Integer& b){ - return (a <=b ) ? a : b; + static const Integer& min(const Integer& a, const Integer& b) + { + return (a <= b) ? a : b; } /** Returns a reference to the maximum of two integers. */ - static const Integer& max(const Integer& a, const Integer& b){ - return (a >= b ) ? a : b; + static const Integer& max(const Integer& a, const Integer& b) + { + return (a >= b) ? a : b; } - friend class CVC4::Rational; -};/* class Integer */ + private: + /** + * Gets a reference to the cln data that backs up the integer. + * Only accessible to friend classes. + */ + const cln::cl_I& get_cl_I() const { return d_value; } + // Throws a std::invalid_argument on invalid input `s` for the given base. + void readInt(const cln::cl_read_flags& flags, + const std::string& s, + unsigned base); -struct IntegerHashFunction { - inline size_t operator()(const CVC4::Integer& i) const { - return i.hash(); - } -};/* struct IntegerHashFunction */ + // Throws a std::invalid_argument on invalid inputs. + void parseInt(const std::string& s, unsigned base); + + // These constants are to help with CLN conversion in 32 bit. + // See http://www.ginac.de/CLN/cln.html#Conversions + static signed int s_fastSignedIntMax; /* 2^29 - 1 */ + static signed int s_fastSignedIntMin; /* -2^29 */ + static unsigned int s_fastUnsignedIntMax; /* 2^29 - 1 */ + + static signed long + s_slowSignedIntMax; /* std::numeric_limits<signed int>::max() */ + static signed long + s_slowSignedIntMin; /* std::numeric_limits<signed int>::min() */ + static unsigned long + s_slowUnsignedIntMax; /* std::numeric_limits<unsigned int>::max() */ + static unsigned long s_signedLongMin; + static unsigned long s_signedLongMax; + static unsigned long s_unsignedLongMax; + + /** + * Stores the value of the rational is stored in a C++ CLN integer class. + */ + cln::cl_I d_value; +}; /* class Integer */ + +struct IntegerHashFunction +{ + inline size_t operator()(const CVC4::Integer& i) const { return i.hash(); } +}; /* struct IntegerHashFunction */ -inline std::ostream& operator<<(std::ostream& os, const Integer& n) { +inline std::ostream& operator<<(std::ostream& os, const Integer& n) +{ return os << n.toString(); } -}/* CVC4 namespace */ +} // namespace CVC4 #endif /* CVC4__INTEGER_H */ diff --git a/src/util/integer_gmp_imp.cpp b/src/util/integer_gmp_imp.cpp index 2bc11f0a7..8c59d74b8 100644 --- a/src/util/integer_gmp_imp.cpp +++ b/src/util/integer_gmp_imp.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Aina Niemetz, Liana Hadarean ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h index 144e88536..5277923f4 100644 --- a/src/util/integer_gmp_imp.h +++ b/src/util/integer_gmp_imp.h @@ -2,9 +2,9 @@ /*! \file integer_gmp_imp.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Liana Hadarean, Morgan Deters + ** Tim King, Gereon Kremer, Liana Hadarean ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 @@ -20,9 +20,9 @@ #ifndef CVC4__INTEGER_H #define CVC4__INTEGER_H -#include <string> #include <iosfwd> #include <limits> +#include <string> #include "base/exception.h" #include "util/gmp_util.h" @@ -31,29 +31,18 @@ namespace CVC4 { class Rational; -class CVC4_PUBLIC Integer { -private: - /** - * Stores the value of the rational is stored in a C++ GMP integer class. - * Using this instead of mpz_t allows for easier destruction. - */ - mpz_class d_value; - - /** - * Gets a reference to the gmp data that backs up the integer. - * Only accessible to friend classes. - */ - const mpz_class& get_mpz() const { return d_value; } +class CVC4_PUBLIC Integer +{ + friend class CVC4::Rational; + public: /** * Constructs an Integer by copying a GMP C++ primitive. */ Integer(const mpz_class& val) : d_value(val) {} -public: - /** Constructs a rational with the value 0. */ - Integer() : d_value(0){} + Integer() : d_value(0) {} /** * Constructs a Integer from a C string. @@ -66,13 +55,13 @@ public: Integer(const Integer& q) : d_value(q.d_value) {} - Integer( signed int z) : d_value(z) {} + Integer(signed int z) : d_value(z) {} Integer(unsigned int z) : d_value(z) {} - Integer( signed long int z) : d_value(z) {} + Integer(signed long int z) : d_value(z) {} Integer(unsigned long int z) : d_value(z) {} #ifdef CVC4_NEED_INT64_T_OVERLOADS - Integer( int64_t z) : d_value(static_cast<long>(z)) {} + Integer(int64_t z) : d_value(static_cast<long>(z)) {} Integer(uint64_t z) : d_value(static_cast<unsigned long>(z)) {} #endif /* CVC4_NEED_INT64_T_OVERLOADS */ @@ -81,91 +70,82 @@ public: /** * Returns a copy of d_value to enable public access of GMP data. */ - mpz_class getValue() const - { - return d_value; - } + const mpz_class& getValue() const { return d_value; } - Integer& operator=(const Integer& x){ - if(this == &x) return *this; + Integer& operator=(const Integer& x) + { + if (this == &x) return *this; d_value = x.d_value; return *this; } - bool operator==(const Integer& y) const { - return d_value == y.d_value; - } - - Integer operator-() const { - return Integer(-(d_value)); - } + bool operator==(const Integer& y) const { return d_value == y.d_value; } + Integer operator-() const { return Integer(-(d_value)); } - bool operator!=(const Integer& y) const { - return d_value != y.d_value; - } - - bool operator< (const Integer& y) const { - return d_value < y.d_value; - } + bool operator!=(const Integer& y) const { return d_value != y.d_value; } - bool operator<=(const Integer& y) const { - return d_value <= y.d_value; - } + bool operator<(const Integer& y) const { return d_value < y.d_value; } - bool operator> (const Integer& y) const { - return d_value > y.d_value; - } + bool operator<=(const Integer& y) const { return d_value <= y.d_value; } - bool operator>=(const Integer& y) const { - return d_value >= y.d_value; - } + bool operator>(const Integer& y) const { return d_value > y.d_value; } + bool operator>=(const Integer& y) const { return d_value >= y.d_value; } - Integer operator+(const Integer& y) const { - return Integer( d_value + y.d_value ); + Integer operator+(const Integer& y) const + { + return Integer(d_value + y.d_value); } - Integer& operator+=(const Integer& y) { + 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) const + { + return Integer(d_value - y.d_value); } - Integer& operator-=(const Integer& y) { + 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) const + { + return Integer(d_value * y.d_value); } - Integer& operator*=(const Integer& y) { + Integer& operator*=(const Integer& y) + { d_value *= y.d_value; return *this; } - - Integer bitwiseOr(const Integer& y) const { + Integer bitwiseOr(const Integer& y) const + { mpz_class result; mpz_ior(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t()); return Integer(result); } - Integer bitwiseAnd(const Integer& y) const { + Integer bitwiseAnd(const Integer& y) const + { mpz_class result; mpz_and(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t()); return Integer(result); } - Integer bitwiseXor(const Integer& y) const { + Integer bitwiseXor(const Integer& y) const + { mpz_class result; mpz_xor(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t()); return Integer(result); } - Integer bitwiseNot() const { + Integer bitwiseNot() const + { mpz_class result; mpz_com(result.get_mpz_t(), d_value.get_mpz_t()); return Integer(result); @@ -174,25 +154,25 @@ public: /** * Return this*(2^pow). */ - Integer multiplyByPow2(uint32_t pow) const{ + Integer multiplyByPow2(uint32_t pow) const + { mpz_class result; mpz_mul_2exp(result.get_mpz_t(), d_value.get_mpz_t(), pow); - return Integer( result ); + return Integer(result); } /** * Returns the Integer obtained by setting the ith bit of the * current Integer to 1. */ - Integer setBit(uint32_t i) const { + Integer setBit(uint32_t i) const + { mpz_class res = d_value; mpz_setbit(res.get_mpz_t(), i); return Integer(res); } - bool isBitSet(uint32_t i) const { - return !extractBitRange(1, i).isZero(); - } + bool isBitSet(uint32_t i) const { return !extractBitRange(1, i).isZero(); } /** * Returns the integer with the binary representation of size bits @@ -200,17 +180,16 @@ public: */ Integer oneExtend(uint32_t size, uint32_t amount) const; - uint32_t toUnsignedInt() const { - return mpz_get_ui(d_value.get_mpz_t()); - } + uint32_t toUnsignedInt() const { return mpz_get_ui(d_value.get_mpz_t()); } /** See GMP Documentation. */ - Integer extractBitRange(uint32_t bitCount, uint32_t low) const { + Integer extractBitRange(uint32_t bitCount, uint32_t low) const + { // bitCount = high-low+1 - uint32_t high = low + bitCount-1; + uint32_t high = low + bitCount - 1; //— Function: void mpz_fdiv_r_2exp (mpz_t r, mpz_t n, mp_bitcnt_t b) mpz_class rem, div; - mpz_fdiv_r_2exp(rem.get_mpz_t(), d_value.get_mpz_t(), high+1); + mpz_fdiv_r_2exp(rem.get_mpz_t(), d_value.get_mpz_t(), high + 1); mpz_fdiv_q_2exp(div.get_mpz_t(), rem.get_mpz_t(), low); return Integer(div); @@ -219,72 +198,91 @@ public: /** * Returns the floor(this / y) */ - Integer floorDivideQuotient(const Integer& y) const { + Integer floorDivideQuotient(const Integer& y) const + { mpz_class q; mpz_fdiv_q(q.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t()); - return Integer( q ); + return Integer(q); } /** * Returns r == this - floor(this/y)*y */ - Integer floorDivideRemainder(const Integer& y) const { + Integer floorDivideRemainder(const Integer& y) const + { mpz_class r; mpz_fdiv_r(r.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t()); - return Integer( r ); + return Integer(r); } /** * Computes a floor quotient and remainder for x divided by y. */ - static void floorQR(Integer& q, Integer& r, const Integer& x, const Integer& y) { - mpz_fdiv_qr(q.d_value.get_mpz_t(), r.d_value.get_mpz_t(), x.d_value.get_mpz_t(), y.d_value.get_mpz_t()); + static void floorQR(Integer& q, + Integer& r, + const Integer& x, + const Integer& y) + { + mpz_fdiv_qr(q.d_value.get_mpz_t(), + r.d_value.get_mpz_t(), + x.d_value.get_mpz_t(), + y.d_value.get_mpz_t()); } /** * Returns the ceil(this / y) */ - Integer ceilingDivideQuotient(const Integer& y) const { + Integer ceilingDivideQuotient(const Integer& y) const + { mpz_class q; mpz_cdiv_q(q.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t()); - return Integer( q ); + return Integer(q); } /** * Returns the ceil(this / y) */ - Integer ceilingDivideRemainder(const Integer& y) const { + Integer ceilingDivideRemainder(const Integer& y) const + { mpz_class r; mpz_cdiv_r(r.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t()); - return Integer( r ); + return Integer(r); } /** - * Computes a quotient and remainder according to Boute's Euclidean definition. - * euclidianDivideQuotient, euclidianDivideRemainder. + * Computes a quotient and remainder according to Boute's Euclidean + * definition. euclidianDivideQuotient, euclidianDivideRemainder. * * Boute, Raymond T. (April 1992). * The Euclidean definition of the functions div and mod. * ACM Transactions on Programming Languages and Systems (TOPLAS) * ACM Press. 14 (2): 127 - 144. doi:10.1145/128861.128862. */ - static void euclidianQR(Integer& q, Integer& r, const Integer& x, const Integer& y) { + static void euclidianQR(Integer& q, + Integer& r, + const Integer& x, + const Integer& y) + { // compute the floor and then fix the value up if needed. - floorQR(q,r,x,y); + floorQR(q, r, x, y); - if(r.strictlyNegative()){ + if (r.strictlyNegative()) + { // if r < 0 // abs(r) < abs(y) // - abs(y) < r < 0, then 0 < r + abs(y) < abs(y) // n = y * q + r // n = y * q - abs(y) + r + abs(y) - if(r.sgn() >= 0){ + if (r.sgn() >= 0) + { // y = abs(y) // n = y * q - y + r + y // n = y * (q-1) + (r+y) q -= 1; r += y; - }else{ + } + else + { // y = -abs(y) // n = y * q + y + r - y // n = y * (q+1) + (r-y) @@ -298,9 +296,10 @@ public: * Returns the quotient according to Boute's Euclidean definition. * See the documentation for euclidianQR. */ - Integer euclidianDivideQuotient(const Integer& y) const { - Integer q,r; - euclidianQR(q,r, *this, y); + Integer euclidianDivideQuotient(const Integer& y) const + { + Integer q, r; + euclidianQR(q, r, *this, y); return q; } @@ -308,13 +307,13 @@ public: * Returns the remainder according to Boute's Euclidean definition. * See the documentation for euclidianQR. */ - Integer euclidianDivideRemainder(const Integer& y) const { - Integer q,r; - euclidianQR(q,r, *this, y); + Integer euclidianDivideRemainder(const Integer& y) const + { + Integer q, r; + euclidianQR(q, r, *this, y); return r; } - /** * If y divides *this, then exactQuotient returns (this/y) */ @@ -323,7 +322,8 @@ public: /** * Returns y mod 2^exp */ - Integer modByPow2(uint32_t exp) const { + Integer modByPow2(uint32_t exp) const + { mpz_class res; mpz_fdiv_r_2exp(res.get_mpz_t(), d_value.get_mpz_t(), exp); return Integer(res); @@ -332,34 +332,25 @@ public: /** * Returns y / 2^exp */ - Integer divByPow2(uint32_t exp) const { + Integer divByPow2(uint32_t exp) const + { mpz_class res; mpz_fdiv_q_2exp(res.get_mpz_t(), d_value.get_mpz_t(), exp); return Integer(res); } + int sgn() const { return mpz_sgn(d_value.get_mpz_t()); } - int sgn() const { - return mpz_sgn(d_value.get_mpz_t()); - } + inline bool strictlyPositive() const { return sgn() > 0; } - inline bool strictlyPositive() const { - return sgn() > 0; - } + inline bool strictlyNegative() const { return sgn() < 0; } - inline bool strictlyNegative() const { - return sgn() < 0; - } - - inline bool isZero() const { - return sgn() == 0; - } + inline bool isZero() const { return sgn() == 0; } - bool isOne() const { - return mpz_cmp_si(d_value.get_mpz_t(), 1) == 0; - } + bool isOne() const { return mpz_cmp_si(d_value.get_mpz_t(), 1) == 0; } - bool isNegativeOne() const { + bool isNegativeOne() const + { return mpz_cmp_si(d_value.get_mpz_t(), -1) == 0; } @@ -368,7 +359,8 @@ public: * * @param exp the exponent */ - Integer pow(unsigned long int exp) const { + Integer pow(unsigned long int exp) const + { mpz_class result; mpz_pow_ui(result.get_mpz_t(), d_value.get_mpz_t(), exp); return Integer(result); @@ -377,7 +369,8 @@ public: /** * Return the greatest common divisor of this integer with another. */ - Integer gcd(const Integer& y) const { + Integer gcd(const Integer& y) const + { mpz_class result; mpz_gcd(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t()); return Integer(result); @@ -386,7 +379,8 @@ public: /** * Return the least common multiple of this integer with another. */ - Integer lcm(const Integer& y) const { + Integer lcm(const Integer& y) const + { mpz_class result; mpz_lcm(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t()); return Integer(result); @@ -420,7 +414,8 @@ public: * All non-zero integers z, z.divide(0) * ! zero.divides(zero) */ - bool divides(const Integer& y) const { + bool divides(const Integer& y) const + { int res = mpz_divisible_p(y.d_value.get_mpz_t(), d_value.get_mpz_t()); return res != 0; } @@ -428,13 +423,9 @@ public: /** * Return the absolute value of this integer. */ - Integer abs() const { - return d_value >= 0 ? *this : -*this; - } + Integer abs() const { return d_value >= 0 ? *this : -*this; } - std::string toString(int base = 10) const{ - return d_value.get_str(base); - } + std::string toString(int base = 10) const { return d_value.get_str(base); } bool fitsSignedInt() const; @@ -448,18 +439,22 @@ public: bool fitsUnsignedLong() const; - long getLong() const { + long getLong() const + { long si = d_value.get_si(); // ensure there wasn't overflow - CheckArgument(mpz_cmp_si(d_value.get_mpz_t(), si) == 0, this, - "Overflow detected in Integer::getLong()."); + CheckArgument(mpz_cmp_si(d_value.get_mpz_t(), si) == 0, + this, + "Overflow detected in Integer::getLong()."); return si; } - unsigned long getUnsignedLong() const { + unsigned long getUnsignedLong() const + { unsigned long ui = d_value.get_ui(); // ensure there wasn't overflow - CheckArgument(mpz_cmp_ui(d_value.get_mpz_t(), ui) == 0, this, + CheckArgument(mpz_cmp_ui(d_value.get_mpz_t(), ui) == 0, + this, "Overflow detected in Integer::getUnsignedLong()."); return ui; } @@ -468,9 +463,7 @@ public: * Computes the hash of the node from the first word of the * numerator, the denominator. */ - size_t hash() const { - return gmpz_hash(d_value.get_mpz_t()); - } + size_t hash() const { return gmpz_hash(d_value.get_mpz_t()); } /** * Returns true iff bit n is set. @@ -478,66 +471,88 @@ public: * @param n the bit to test (0 == least significant bit) * @return true if bit n is set in this integer; false otherwise */ - bool testBit(unsigned n) const { - return mpz_tstbit(d_value.get_mpz_t(), n); - } + bool testBit(unsigned n) const { return mpz_tstbit(d_value.get_mpz_t(), n); } /** * Returns k if the integer is equal to 2^(k-1) * @return k if the integer is equal to 2^(k-1) and 0 otherwise */ - unsigned isPow2() const { + unsigned isPow2() const + { if (d_value <= 0) return 0; // check that the number of ones in the binary representation is 1 - if (mpz_popcount(d_value.get_mpz_t()) == 1) { + if (mpz_popcount(d_value.get_mpz_t()) == 1) + { // return the index of the first one plus 1 return mpz_scan1(d_value.get_mpz_t(), 0) + 1; } - return 0; + return 0; } - /** * If x != 0, returns the smallest n s.t. 2^{n-1} <= abs(x) < 2^{n}. * If x == 0, returns 1. */ - size_t length() const { - if(sgn() == 0){ + size_t length() const + { + if (sgn() == 0) + { return 1; - }else{ - return mpz_sizeinbase(d_value.get_mpz_t(),2); + } + else + { + return mpz_sizeinbase(d_value.get_mpz_t(), 2); } } - static void extendedGcd(Integer& g, Integer& s, Integer& t, const Integer& a, const Integer& b){ - //see the documentation for: - //mpz_gcdext (mpz_t g, mpz_t s, mpz_t t, mpz_t a, mpz_t b); - mpz_gcdext (g.d_value.get_mpz_t(), s.d_value.get_mpz_t(), t.d_value.get_mpz_t(), a.d_value.get_mpz_t(), b.d_value.get_mpz_t()); + static void extendedGcd( + Integer& g, Integer& s, Integer& t, const Integer& a, const Integer& b) + { + // see the documentation for: + // mpz_gcdext (mpz_t g, mpz_t s, mpz_t t, mpz_t a, mpz_t b); + mpz_gcdext(g.d_value.get_mpz_t(), + s.d_value.get_mpz_t(), + t.d_value.get_mpz_t(), + a.d_value.get_mpz_t(), + b.d_value.get_mpz_t()); } /** Returns a reference to the minimum of two integers. */ - static const Integer& min(const Integer& a, const Integer& b){ - return (a <=b ) ? a : b; + static const Integer& min(const Integer& a, const Integer& b) + { + return (a <= b) ? a : b; } /** Returns a reference to the maximum of two integers. */ - static const Integer& max(const Integer& a, const Integer& b){ - return (a >= b ) ? a : b; + static const Integer& max(const Integer& a, const Integer& b) + { + return (a >= b) ? a : b; } - friend class CVC4::Rational; -};/* class Integer */ + private: + /** + * Gets a reference to the gmp data that backs up the integer. + * Only accessible to friend classes. + */ + const mpz_class& get_mpz() const { return d_value; } -struct IntegerHashFunction { - inline size_t operator()(const CVC4::Integer& i) const { - return i.hash(); - } -};/* struct IntegerHashFunction */ + /** + * Stores the value of the rational is stored in a C++ GMP integer class. + * Using this instead of mpz_t allows for easier destruction. + */ + mpz_class d_value; +}; /* class Integer */ + +struct IntegerHashFunction +{ + inline size_t operator()(const CVC4::Integer& i) const { return i.hash(); } +}; /* struct IntegerHashFunction */ -inline std::ostream& operator<<(std::ostream& os, const Integer& n) { +inline std::ostream& operator<<(std::ostream& os, const Integer& n) +{ return os << n.toString(); } -}/* CVC4 namespace */ +} // namespace CVC4 #endif /* CVC4__INTEGER_H */ diff --git a/src/util/maybe.h b/src/util/maybe.h index 33c6c6511..ed8c999a5 100644 --- a/src/util/maybe.h +++ b/src/util/maybe.h @@ -2,9 +2,9 @@ /*! \file maybe.h ** \verbatim ** Top contributors (to current version): - ** Tim King + ** Tim King, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/util/ostream_util.cpp b/src/util/ostream_util.cpp index 3ada604ca..c8d81d363 100644 --- a/src/util/ostream_util.cpp +++ b/src/util/ostream_util.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/util/ostream_util.h b/src/util/ostream_util.h index 45d30a01c..e58ff8443 100644 --- a/src/util/ostream_util.h +++ b/src/util/ostream_util.h @@ -2,9 +2,9 @@ /*! \file ostream_util.h ** \verbatim ** Top contributors (to current version): - ** Tim King + ** Tim King, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/util/proof.h b/src/util/proof.h index ac129e3aa..c89a3b0a6 100644 --- a/src/util/proof.h +++ b/src/util/proof.h @@ -2,9 +2,9 @@ /*! \file proof.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Tim King, Guy Katz + ** Tim King, Morgan Deters, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/util/proof.i b/src/util/proof.i index 22dff1043..59a524a0f 100644 --- a/src/util/proof.i +++ b/src/util/proof.i @@ -2,4 +2,6 @@ #include "util/proof.h" %} +%ignore CVC4::Proof::toStream(std::ostream& out, const ProofLetMap& map) const; + %include "util/proof.h" diff --git a/src/util/random.cpp b/src/util/random.cpp index 325fac325..89b8c0513 100644 --- a/src/util/random.cpp +++ b/src/util/random.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/util/random.h b/src/util/random.h index 0b46a1f04..04bea1b69 100644 --- a/src/util/random.h +++ b/src/util/random.h @@ -2,9 +2,9 @@ /*! \file random.h ** \verbatim ** Top contributors (to current version): - ** Aina Niemetz, Andres Noetzli + ** Aina Niemetz, Andres Noetzli, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/util/rational.h.in b/src/util/rational.h.in index 5da7a501e..b5934cc10 100644 --- a/src/util/rational.h.in +++ b/src/util/rational.h.in @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/util/rational_cln_imp.cpp b/src/util/rational_cln_imp.cpp index d19f99d31..2624698bc 100644 --- a/src/util/rational_cln_imp.cpp +++ b/src/util/rational_cln_imp.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Christopher L. Conway, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h index 660c4b075..724698363 100644 --- a/src/util/rational_cln_imp.h +++ b/src/util/rational_cln_imp.h @@ -2,9 +2,9 @@ /*! \file rational_cln_imp.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Christopher L. Conway + ** Tim King, Gereon Kremer, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 @@ -20,19 +20,19 @@ #ifndef CVC4__RATIONAL_H #define CVC4__RATIONAL_H -#include <gmp.h> -#include <string> -#include <sstream> -#include <cassert> -#include <cln/rational.h> +#include <cln/dfloat.h> #include <cln/input.h> #include <cln/io.h> +#include <cln/number_io.h> #include <cln/output.h> +#include <cln/rational.h> #include <cln/rational_io.h> -#include <cln/number_io.h> -#include <cln/dfloat.h> #include <cln/real.h> +#include <cassert> +#include <sstream> +#include <string> + #include "base/exception.h" #include "util/integer.h" #include "util/maybe.h" @@ -54,24 +54,14 @@ namespace CVC4 { ** in danger of invoking the char* constructor, from whence you will segfault. **/ -class CVC4_PUBLIC Rational { -private: +class CVC4_PUBLIC Rational +{ + public: /** - * Stores the value of the rational is stored in a C++ GMP rational class. - * Using this instead of mpq_t allows for easier destruction. - */ - cln::cl_RA d_value; - - /** - * Constructs a Rational from a mpq_class object. + * Constructs a Rational from a cln::cl_RA object. * Does a deep copy. - * Assumes that the value is in canonical form, and thus does not - * have to call canonicalize() on the value. */ - //Rational(const mpq_class& val) : d_value(val) { } - Rational(const cln::cl_RA& val) : d_value(val) { } - -public: + Rational(const cln::cl_RA& val) : d_value(val) {} /** * Creates a rational from a decimal string (e.g., <code>"1.5"</code>). @@ -82,14 +72,13 @@ public: static Rational fromDecimal(const std::string& dec); /** Constructs a rational with the value 0/1. */ - Rational() : d_value(0){ - } + Rational() : d_value(0) {} /** * Constructs a Rational from a C string in a given base (defaults to 10). * * Throws std::invalid_argument if the string is not a valid rational. * For more information about what is a valid rational string, - * see GMP's documentation for mpq_set_str(). + * see CLN's documentation for read_rational. */ explicit Rational(const char* s, unsigned base = 10) { @@ -98,11 +87,14 @@ public: flags.syntax = cln::syntax_rational; flags.lsyntax = cln::lsyntax_standard; flags.rational_base = base; - try{ + try + { d_value = read_rational(flags, s, NULL, NULL); - }catch(...){ + } + catch (...) + { std::stringstream ss; - ss << "Rational() failed to parse value \"" <<s << "\" in base=" <<base; + ss << "Rational() failed to parse value \"" << s << "\" in base=" << base; throw std::invalid_argument(ss.str()); } } @@ -113,11 +105,14 @@ public: flags.syntax = cln::syntax_rational; flags.lsyntax = cln::lsyntax_standard; flags.rational_base = base; - try{ + try + { d_value = read_rational(flags, s.c_str(), NULL, NULL); - }catch(...){ + } + catch (...) + { std::stringstream ss; - ss << "Rational() failed to parse value \"" <<s << "\" in base=" <<base; + ss << "Rational() failed to parse value \"" << s << "\" in base=" << base; throw std::invalid_argument(ss.str()); } } @@ -125,78 +120,76 @@ public: /** * Creates a Rational from another Rational, q, by performing a deep copy. */ - Rational(const Rational& q) : d_value(q.d_value) { } + Rational(const Rational& q) : d_value(q.d_value) {} /** * Constructs a canonical Rational from a numerator. */ - Rational(signed int n) : d_value((signed long int)n) { } - Rational(unsigned int n) : d_value((unsigned long int)n) { } - Rational(signed long int n) : d_value(n) { } - Rational(unsigned long int n) : d_value(n) { } + Rational(signed int n) : d_value((signed long int)n) {} + Rational(unsigned int n) : d_value((unsigned long int)n) {} + Rational(signed long int n) : d_value(n) {} + Rational(unsigned long int n) : d_value(n) {} #ifdef CVC4_NEED_INT64_T_OVERLOADS - Rational(int64_t n) : d_value(static_cast<long>(n)) { } - Rational(uint64_t n) : d_value(static_cast<unsigned long>(n)) { } + Rational(int64_t n) : d_value(static_cast<long>(n)) {} + Rational(uint64_t n) : d_value(static_cast<unsigned long>(n)) {} #endif /* CVC4_NEED_INT64_T_OVERLOADS */ /** * Constructs a canonical Rational from a numerator and denominator. */ - Rational(signed int n, signed int d) : d_value((signed long int)n) { + Rational(signed int n, signed int d) : d_value((signed long int)n) + { d_value /= cln::cl_I(d); } - Rational(unsigned int n, unsigned int d) : d_value((unsigned long int)n) { + Rational(unsigned int n, unsigned int d) : d_value((unsigned long int)n) + { d_value /= cln::cl_I(d); } - Rational(signed long int n, signed long int d) : d_value(n) { + Rational(signed long int n, signed long int d) : d_value(n) + { d_value /= cln::cl_I(d); } - Rational(unsigned long int n, unsigned long int d) : d_value(n) { + Rational(unsigned long int n, unsigned long int d) : d_value(n) + { d_value /= cln::cl_I(d); } #ifdef CVC4_NEED_INT64_T_OVERLOADS - Rational(int64_t n, int64_t d) : d_value(static_cast<long>(n)) { + Rational(int64_t n, int64_t d) : d_value(static_cast<long>(n)) + { d_value /= cln::cl_I(d); } - Rational(uint64_t n, uint64_t d) : d_value(static_cast<unsigned long>(n)) { + Rational(uint64_t n, uint64_t d) : d_value(static_cast<unsigned long>(n)) + { d_value /= cln::cl_I(d); } #endif /* CVC4_NEED_INT64_T_OVERLOADS */ - Rational(const Integer& n, const Integer& d) : - d_value(n.get_cl_I()) + Rational(const Integer& n, const Integer& d) : d_value(n.get_cl_I()) { d_value /= d.get_cl_I(); } - Rational(const Integer& n) : d_value(n.get_cl_I()){ } + Rational(const Integer& n) : d_value(n.get_cl_I()) {} ~Rational() {} /** * Returns a copy of d_value to enable public access of CLN data. */ - cln::cl_RA getValue() const - { - return d_value; - } + const cln::cl_RA& getValue() const { return d_value; } /** * Returns the value of numerator of the Rational. * Note that this makes a deep copy of the numerator. */ - Integer getNumerator() const { - return Integer(cln::numerator(d_value)); - } + Integer getNumerator() const { return Integer(cln::numerator(d_value)); } /** * Returns the value of denominator of the Rational. * Note that this makes a deep copy of the denominator. */ - Integer getDenominator() const { - return Integer(cln::denominator(d_value)); - } + Integer getDenominator() const { return Integer(cln::denominator(d_value)); } /** Return an exact rational for a double d. */ static Maybe<Rational> fromDouble(double d); @@ -206,138 +199,126 @@ public: * approximate: truncation may occur, overflow may result in * infinity, and underflow may result in zero. */ - double getDouble() const { - return cln::double_approx(d_value); - } + double getDouble() const { return cln::double_approx(d_value); } - Rational inverse() const { - return Rational(cln::recip(d_value)); - } + Rational inverse() const { return Rational(cln::recip(d_value)); } - int cmp(const Rational& x) const { - //Don't use mpq_class's cmp() function. - //The name ends up conflicting with this function. + int cmp(const Rational& x) const + { + // Don't use mpq_class's cmp() function. + // The name ends up conflicting with this function. return cln::compare(d_value, x.d_value); } - - int sgn() const { - if(cln::zerop(d_value)){ - return 0; - }else if(cln::minusp(d_value)){ - return -1; - }else{ + int sgn() const + { + if (cln::zerop(d_value)) + { + return 0; + } + else if (cln::minusp(d_value)) + { + return -1; + } + else + { assert(cln::plusp(d_value)); return 1; } } - bool isZero() const { - return cln::zerop(d_value); - } + bool isZero() const { return cln::zerop(d_value); } - bool isOne() const { - return d_value == 1; - } + bool isOne() const { return d_value == 1; } - bool isNegativeOne() const { - return d_value == -1; - } + bool isNegativeOne() const { return d_value == -1; } - Rational abs() const { - if(sgn() < 0){ + Rational abs() const + { + if (sgn() < 0) + { return -(*this); - }else{ + } + else + { return *this; } } - bool isIntegral() const{ - return getDenominator() == 1; - } + bool isIntegral() const { return getDenominator() == 1; } - Integer floor() const { - return Integer(cln::floor1(d_value)); - } + Integer floor() const { return Integer(cln::floor1(d_value)); } - Integer ceiling() const { - return Integer(cln::ceiling1(d_value)); - } + Integer ceiling() const { return Integer(cln::ceiling1(d_value)); } - Rational floor_frac() const { - return (*this) - Rational(floor()); - } + Rational floor_frac() const { return (*this) - Rational(floor()); } - Rational& operator=(const Rational& x){ - if(this == &x) return *this; + Rational& operator=(const Rational& x) + { + if (this == &x) return *this; d_value = x.d_value; return *this; } - Rational operator-() const{ - return Rational(-(d_value)); - } + Rational operator-() const { return Rational(-(d_value)); } - bool operator==(const Rational& y) const { - return d_value == y.d_value; - } + bool operator==(const Rational& y) const { return d_value == y.d_value; } - bool operator!=(const Rational& y) const { - return d_value != y.d_value; - } + bool operator!=(const Rational& y) const { return d_value != y.d_value; } - bool operator< (const Rational& y) const { - return d_value < y.d_value; - } + bool operator<(const Rational& y) const { return d_value < y.d_value; } - bool operator<=(const Rational& y) const { - return d_value <= y.d_value; - } + bool operator<=(const Rational& y) const { return d_value <= y.d_value; } - bool operator> (const Rational& y) const { - return d_value > y.d_value; - } + bool operator>(const Rational& y) const { return d_value > y.d_value; } - bool operator>=(const Rational& y) const { - return d_value >= y.d_value; - } + bool operator>=(const Rational& y) const { return d_value >= y.d_value; } - Rational operator+(const Rational& y) const{ - return Rational( d_value + y.d_value ); + Rational operator+(const Rational& y) const + { + return Rational(d_value + y.d_value); } - Rational operator-(const Rational& y) const { - return Rational( d_value - y.d_value ); + Rational operator-(const Rational& y) const + { + return Rational(d_value - y.d_value); } - Rational operator*(const Rational& y) const { - return Rational( d_value * y.d_value ); + Rational operator*(const Rational& y) const + { + return Rational(d_value * y.d_value); } - Rational operator/(const Rational& y) const { - return Rational( d_value / y.d_value ); + Rational operator/(const Rational& y) const + { + return Rational(d_value / y.d_value); } - Rational& operator+=(const Rational& y){ + Rational& operator+=(const Rational& y) + { d_value += y.d_value; return (*this); } - Rational& operator-=(const Rational& y){ + Rational& operator-=(const Rational& y) + { d_value -= y.d_value; return (*this); } - Rational& operator*=(const Rational& y){ + Rational& operator*=(const Rational& y) + { d_value *= y.d_value; return (*this); } - Rational& operator/=(const Rational& y){ + Rational& operator/=(const Rational& y) + { d_value /= y.d_value; return (*this); } /** Returns a string representing the rational in the given base. */ - std::string toString(int base = 10) const { + std::string toString(int base = 10) const + { cln::cl_print_flags flags; flags.rational_base = base; flags.rational_readably = false; @@ -350,27 +331,31 @@ public: * Computes the hash of the rational from hashes of the numerator and the * denominator. */ - size_t hash() const { - return equal_hashcode(d_value); - } + size_t hash() const { return equal_hashcode(d_value); } - uint32_t complexity() const { + uint32_t complexity() const + { return getNumerator().length() + getDenominator().length(); } /** Equivalent to calling (this->abs()).cmp(b.abs()) */ int absCmp(const Rational& q) const; -};/* class Rational */ + private: + /** + * Stores the value of the rational in a C++ CLN rational class. + */ + cln::cl_RA d_value; + +}; /* class Rational */ -struct RationalHashFunction { - inline size_t operator()(const CVC4::Rational& r) const { - return r.hash(); - } -};/* struct RationalHashFunction */ +struct RationalHashFunction +{ + inline size_t operator()(const CVC4::Rational& r) const { return r.hash(); } +}; /* struct RationalHashFunction */ CVC4_PUBLIC std::ostream& operator<<(std::ostream& os, const Rational& n); -}/* CVC4 namespace */ +} // namespace CVC4 #endif /* CVC4__RATIONAL_H */ diff --git a/src/util/rational_gmp_imp.cpp b/src/util/rational_gmp_imp.cpp index 0127381b6..a6442ac1f 100644 --- a/src/util/rational_gmp_imp.cpp +++ b/src/util/rational_gmp_imp.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Christopher L. Conway, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h index ff8a0f776..6054cd793 100644 --- a/src/util/rational_gmp_imp.h +++ b/src/util/rational_gmp_imp.h @@ -2,9 +2,9 @@ /*! \file rational_gmp_imp.h ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Christopher L. Conway + ** Tim King, Gereon Kremer, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 @@ -25,9 +25,9 @@ * cause errors: https://gcc.gnu.org/gcc-4.9/porting_to.html * Including <cstddef> is a workaround for this issue. */ -#include <cstddef> - #include <gmp.h> + +#include <cstddef> #include <string> #include "base/exception.h" @@ -51,23 +51,16 @@ namespace CVC4 { ** in danger of invoking the char* constructor, from whence you will segfault. **/ -class CVC4_PUBLIC Rational { -private: - /** - * Stores the value of the rational is stored in a C++ GMP rational class. - * Using this instead of mpq_t allows for easier destruction. - */ - mpq_class d_value; - +class CVC4_PUBLIC Rational +{ + public: /** * Constructs a Rational from a mpq_class object. * Does a deep copy. * Assumes that the value is in canonical form, and thus does not * have to call canonicalize() on the value. */ - Rational(const mpq_class& val) : d_value(val) { } - -public: + Rational(const mpq_class& val) : d_value(val) {} /** * Creates a rational from a decimal string (e.g., <code>"1.5"</code>). @@ -78,9 +71,7 @@ public: static Rational fromDecimal(const std::string& dec); /** Constructs a rational with the value 0/1. */ - Rational() : d_value(0){ - d_value.canonicalize(); - } + Rational() : d_value(0) { d_value.canonicalize(); } /** * Constructs a Rational from a C string in a given base (defaults to 10). @@ -89,41 +80,35 @@ public: * For more information about what is a valid rational string, * see GMP's documentation for mpq_set_str(). */ - explicit Rational(const char* s, unsigned base = 10): d_value(s, base) { + explicit Rational(const char* s, unsigned base = 10) : d_value(s, base) + { d_value.canonicalize(); } - Rational(const std::string& s, unsigned base = 10) : d_value(s, base) { + Rational(const std::string& s, unsigned base = 10) : d_value(s, base) + { d_value.canonicalize(); } /** * Creates a Rational from another Rational, q, by performing a deep copy. */ - Rational(const Rational& q) : d_value(q.d_value) { - d_value.canonicalize(); - } + Rational(const Rational& q) : d_value(q.d_value) { d_value.canonicalize(); } /** * Constructs a canonical Rational from a numerator. */ - Rational(signed int n) : d_value(n,1) { - d_value.canonicalize(); - } - Rational(unsigned int n) : d_value(n,1) { - d_value.canonicalize(); - } - Rational(signed long int n) : d_value(n,1) { - d_value.canonicalize(); - } - Rational(unsigned long int n) : d_value(n,1) { - d_value.canonicalize(); - } + Rational(signed int n) : d_value(n, 1) { d_value.canonicalize(); } + Rational(unsigned int n) : d_value(n, 1) { d_value.canonicalize(); } + Rational(signed long int n) : d_value(n, 1) { d_value.canonicalize(); } + Rational(unsigned long int n) : d_value(n, 1) { d_value.canonicalize(); } #ifdef CVC4_NEED_INT64_T_OVERLOADS - Rational(int64_t n) : d_value(static_cast<long>(n), 1) { + Rational(int64_t n) : d_value(static_cast<long>(n), 1) + { d_value.canonicalize(); } - Rational(uint64_t n) : d_value(static_cast<unsigned long>(n), 1) { + Rational(uint64_t n) : d_value(static_cast<unsigned long>(n), 1) + { d_value.canonicalize(); } #endif /* CVC4_NEED_INT64_T_OVERLOADS */ @@ -131,63 +116,60 @@ public: /** * Constructs a canonical Rational from a numerator and denominator. */ - Rational(signed int n, signed int d) : d_value(n,d) { + Rational(signed int n, signed int d) : d_value(n, d) + { d_value.canonicalize(); } - Rational(unsigned int n, unsigned int d) : d_value(n,d) { + Rational(unsigned int n, unsigned int d) : d_value(n, d) + { d_value.canonicalize(); } - Rational(signed long int n, signed long int d) : d_value(n,d) { + Rational(signed long int n, signed long int d) : d_value(n, d) + { d_value.canonicalize(); } - Rational(unsigned long int n, unsigned long int d) : d_value(n,d) { + Rational(unsigned long int n, unsigned long int d) : d_value(n, d) + { d_value.canonicalize(); } #ifdef CVC4_NEED_INT64_T_OVERLOADS - Rational(int64_t n, int64_t d) : d_value(static_cast<long>(n), static_cast<long>(d)) { + Rational(int64_t n, int64_t d) + : d_value(static_cast<long>(n), static_cast<long>(d)) + { d_value.canonicalize(); } - Rational(uint64_t n, uint64_t d) : d_value(static_cast<unsigned long>(n), static_cast<unsigned long>(d)) { + Rational(uint64_t n, uint64_t d) + : d_value(static_cast<unsigned long>(n), static_cast<unsigned long>(d)) + { d_value.canonicalize(); } #endif /* CVC4_NEED_INT64_T_OVERLOADS */ - Rational(const Integer& n, const Integer& d) : - d_value(n.get_mpz(), d.get_mpz()) - { - d_value.canonicalize(); - } - Rational(const Integer& n) : - d_value(n.get_mpz()) + Rational(const Integer& n, const Integer& d) + : d_value(n.get_mpz(), d.get_mpz()) { d_value.canonicalize(); } + Rational(const Integer& n) : d_value(n.get_mpz()) { d_value.canonicalize(); } ~Rational() {} /** * Returns a copy of d_value to enable public access of GMP data. */ - mpq_class getValue() const - { - return d_value; - } + const mpq_class& getValue() const { return d_value; } /** * Returns the value of numerator of the Rational. * Note that this makes a deep copy of the numerator. */ - Integer getNumerator() const { - return Integer(d_value.get_num()); - } + Integer getNumerator() const { return Integer(d_value.get_num()); } /** * Returns the value of denominator of the Rational. * Note that this makes a deep copy of the denominator. */ - Integer getDenominator() const { - return Integer(d_value.get_den()); - } + Integer getDenominator() const { return Integer(d_value.get_den()); } static Maybe<Rational> fromDouble(double d); @@ -196,166 +178,164 @@ public: * approximate: truncation may occur, overflow may result in * infinity, and underflow may result in zero. */ - double getDouble() const { - return d_value.get_d(); - } + double getDouble() const { return d_value.get_d(); } - Rational inverse() const { + Rational inverse() const + { return Rational(getDenominator(), getNumerator()); } - int cmp(const Rational& x) const { - //Don't use mpq_class's cmp() function. - //The name ends up conflicting with this function. + int cmp(const Rational& x) const + { + // Don't use mpq_class's cmp() function. + // The name ends up conflicting with this function. return mpq_cmp(d_value.get_mpq_t(), x.d_value.get_mpq_t()); } - int sgn() const { - return mpq_sgn(d_value.get_mpq_t()); - } + int sgn() const { return mpq_sgn(d_value.get_mpq_t()); } - bool isZero() const { - return sgn() == 0; - } + bool isZero() const { return sgn() == 0; } - bool isOne() const { - return mpq_cmp_si(d_value.get_mpq_t(), 1, 1) == 0; - } + bool isOne() const { return mpq_cmp_si(d_value.get_mpq_t(), 1, 1) == 0; } - bool isNegativeOne() const { + bool isNegativeOne() const + { return mpq_cmp_si(d_value.get_mpq_t(), -1, 1) == 0; } - Rational abs() const { - if(sgn() < 0){ + Rational abs() const + { + if (sgn() < 0) + { return -(*this); - }else{ + } + else + { return *this; } } - Integer floor() const { + Integer floor() const + { mpz_class q; mpz_fdiv_q(q.get_mpz_t(), d_value.get_num_mpz_t(), d_value.get_den_mpz_t()); return Integer(q); } - Integer ceiling() const { + Integer ceiling() const + { mpz_class q; mpz_cdiv_q(q.get_mpz_t(), d_value.get_num_mpz_t(), d_value.get_den_mpz_t()); return Integer(q); } - Rational floor_frac() const { - return (*this) - Rational(floor()); - } + Rational floor_frac() const { return (*this) - Rational(floor()); } - Rational& operator=(const Rational& x){ - if(this == &x) return *this; + Rational& operator=(const Rational& x) + { + if (this == &x) return *this; d_value = x.d_value; return *this; } - Rational operator-() const{ - return Rational(-(d_value)); - } + Rational operator-() const { return Rational(-(d_value)); } - bool operator==(const Rational& y) const { - return d_value == y.d_value; - } + bool operator==(const Rational& y) const { return d_value == y.d_value; } - bool operator!=(const Rational& y) const { - return d_value != y.d_value; - } + bool operator!=(const Rational& y) const { return d_value != y.d_value; } - bool operator< (const Rational& y) const { - return d_value < y.d_value; - } + bool operator<(const Rational& y) const { return d_value < y.d_value; } - bool operator<=(const Rational& y) const { - return d_value <= y.d_value; - } + bool operator<=(const Rational& y) const { return d_value <= y.d_value; } - bool operator> (const Rational& y) const { - return d_value > y.d_value; - } + bool operator>(const Rational& y) const { return d_value > y.d_value; } - bool operator>=(const Rational& y) const { - return d_value >= y.d_value; - } + bool operator>=(const Rational& y) const { return d_value >= y.d_value; } - Rational operator+(const Rational& y) const{ - return Rational( d_value + y.d_value ); + Rational operator+(const Rational& y) const + { + return Rational(d_value + y.d_value); } - Rational operator-(const Rational& y) const { - return Rational( d_value - y.d_value ); + Rational operator-(const Rational& y) const + { + return Rational(d_value - y.d_value); } - Rational operator*(const Rational& y) const { - return Rational( d_value * y.d_value ); + Rational operator*(const Rational& y) const + { + return Rational(d_value * y.d_value); } - Rational operator/(const Rational& y) const { - return Rational( d_value / y.d_value ); + Rational operator/(const Rational& y) const + { + return Rational(d_value / y.d_value); } - Rational& operator+=(const Rational& y){ + Rational& operator+=(const Rational& y) + { d_value += y.d_value; return (*this); } - Rational& operator-=(const Rational& y){ + Rational& operator-=(const Rational& y) + { d_value -= y.d_value; return (*this); } - Rational& operator*=(const Rational& y){ + Rational& operator*=(const Rational& y) + { d_value *= y.d_value; return (*this); } - Rational& operator/=(const Rational& y){ + Rational& operator/=(const Rational& y) + { d_value /= y.d_value; return (*this); } - bool isIntegral() const{ - return getDenominator() == 1; - } + bool isIntegral() const { return getDenominator() == 1; } /** Returns a string representing the rational in the given base. */ - std::string toString(int base = 10) const { - return d_value.get_str(base); - } + std::string toString(int base = 10) const { return d_value.get_str(base); } /** * Computes the hash of the rational from hashes of the numerator and the * denominator. */ - size_t hash() const { + size_t hash() const + { size_t numeratorHash = gmpz_hash(d_value.get_num_mpz_t()); size_t denominatorHash = gmpz_hash(d_value.get_den_mpz_t()); return numeratorHash xor denominatorHash; } - uint32_t complexity() const { + uint32_t complexity() const + { uint32_t numLen = getNumerator().length(); uint32_t denLen = getDenominator().length(); - return numLen + denLen; + return numLen + denLen; } /** Equivalent to calling (this->abs()).cmp(b.abs()) */ int absCmp(const Rational& q) const; -};/* class Rational */ + private: + /** + * Stores the value of the rational is stored in a C++ GMP rational class. + * Using this instead of mpq_t allows for easier destruction. + */ + mpq_class d_value; -struct RationalHashFunction { - inline size_t operator()(const CVC4::Rational& r) const { - return r.hash(); - } -};/* struct RationalHashFunction */ +}; /* class Rational */ + +struct RationalHashFunction +{ + inline size_t operator()(const CVC4::Rational& r) const { return r.hash(); } +}; /* struct RationalHashFunction */ CVC4_PUBLIC std::ostream& operator<<(std::ostream& os, const Rational& n); -}/* CVC4 namespace */ +} // namespace CVC4 #endif /* CVC4__RATIONAL_H */ diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp index 7051b251f..be1459865 100644 --- a/src/util/regexp.cpp +++ b/src/util/regexp.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/util/regexp.h b/src/util/regexp.h index aaba9e4db..180bb0c32 100644 --- a/src/util/regexp.h +++ b/src/util/regexp.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp index 2667d8513..eddf9e5c9 100644 --- a/src/util/resource_manager.cpp +++ b/src/util/resource_manager.cpp @@ -2,9 +2,9 @@ /*! \file resource_manager.cpp ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Tim King, Morgan Deters + ** Liana Hadarean, Mathias Preiner, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h index 659d455f2..39fceb7ec 100644 --- a/src/util/resource_manager.h +++ b/src/util/resource_manager.h @@ -2,9 +2,9 @@ /*! \file resource_manager.h ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Tim King, Morgan Deters + ** Tim King, Liana Hadarean, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/util/result.cpp b/src/util/result.cpp index 01d5b052e..0ed063ebc 100644 --- a/src/util/result.cpp +++ b/src/util/result.cpp @@ -2,9 +2,9 @@ /*! \file result.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Andrew Reynolds + ** Tim King, Aina Niemetz, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 @@ -374,7 +374,6 @@ void Result::toStreamTptp(std::ostream& out) const { void Result::toStream(std::ostream& out, OutputLanguage language) const { switch (language) { - case language::output::LANG_SYGUS_V1: case language::output::LANG_SYGUS_V2: toStreamSmt2(out); break; case language::output::LANG_TPTP: toStreamTptp(out); diff --git a/src/util/result.h b/src/util/result.h index 10df05388..d9d024b5a 100644 --- a/src/util/result.h +++ b/src/util/result.h @@ -2,9 +2,9 @@ /*! \file result.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Tim King + ** Morgan Deters, Tim King, Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/util/safe_print.cpp b/src/util/safe_print.cpp index beb1a1673..7bc7fed9b 100644 --- a/src/util/safe_print.cpp +++ b/src/util/safe_print.cpp @@ -2,9 +2,9 @@ /*! \file safe_print.cpp ** \verbatim ** Top contributors (to current version): - ** Andres Noetzli, Andres Noetzli + ** Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/util/safe_print.h b/src/util/safe_print.h index fa9430f2c..4afd08c1a 100644 --- a/src/util/safe_print.h +++ b/src/util/safe_print.h @@ -2,9 +2,9 @@ /*! \file safe_print.h ** \verbatim ** Top contributors (to current version): - ** Andres Noetzli + ** Andres Noetzli, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/util/sampler.cpp b/src/util/sampler.cpp index 60d38bb34..47cc32fb0 100644 --- a/src/util/sampler.cpp +++ b/src/util/sampler.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/util/sampler.h b/src/util/sampler.h index aa473ba0c..688c83f1b 100644 --- a/src/util/sampler.h +++ b/src/util/sampler.h @@ -2,9 +2,9 @@ /*! \file sampler.h ** \verbatim ** Top contributors (to current version): - ** Andres Noetzli + ** Andres Noetzli, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/util/sexpr.cpp b/src/util/sexpr.cpp index 24ec700bc..6f2da480e 100644 --- a/src/util/sexpr.cpp +++ b/src/util/sexpr.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Morgan Deters, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 @@ -272,7 +272,6 @@ void SExpr::toStreamRec(std::ostream& out, const SExpr& sexpr, bool SExpr::languageQuotesKeywords(OutputLanguage language) { switch (language) { - case language::output::LANG_SYGUS_V1: case language::output::LANG_TPTP: return true; case language::output::LANG_AST: diff --git a/src/util/sexpr.h b/src/util/sexpr.h index bdc85df41..73e25026a 100644 --- a/src/util/sexpr.h +++ b/src/util/sexpr.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Tim King, Morgan Deters, Christopher L. Conway ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/util/smt2_quote_string.cpp b/src/util/smt2_quote_string.cpp index 8d1d4b987..3dc41407a 100644 --- a/src/util/smt2_quote_string.cpp +++ b/src/util/smt2_quote_string.cpp @@ -2,9 +2,9 @@ /*! \file smt2_quote_string.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Morgan Deters, Kshitij Bansal + ** Tim King, Andres Noetzli, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/util/smt2_quote_string.h b/src/util/smt2_quote_string.h index f91874a2e..fb8332063 100644 --- a/src/util/smt2_quote_string.h +++ b/src/util/smt2_quote_string.h @@ -2,9 +2,9 @@ /*! \file smt2_quote_string.h ** \verbatim ** Top contributors (to current version): - ** Tim King + ** Tim King, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/util/statistics.cpp b/src/util/statistics.cpp index c61520df9..0344bb5b1 100644 --- a/src/util/statistics.cpp +++ b/src/util/statistics.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Andres Noetzli, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/util/statistics.h b/src/util/statistics.h index 68d8d6fda..e77b48090 100644 --- a/src/util/statistics.h +++ b/src/util/statistics.h @@ -2,9 +2,9 @@ /*! \file statistics.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Andres Noetzli, Tim King + ** Morgan Deters, Andres Noetzli, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/util/statistics.i b/src/util/statistics.i index 8d1086dcc..7dfc7ec39 100644 --- a/src/util/statistics.i +++ b/src/util/statistics.i @@ -64,12 +64,12 @@ %include <std_pair.i> %include <std_string.i> -%include <std_vector.i> -%include "bindings/java_iterator_adapter.h" %include "util/sexpr.h" %template(Statistic) std::pair<std::string, CVC4::SExpr>; + +%feature("valuewrapper") CVC4::JavaIteratorAdapter<CVC4::StatisticsBase, std::pair<std::string, CVC4::SExpr> >; %template(JavaIteratorAdapter_StatisticsBase) CVC4::JavaIteratorAdapter<CVC4::StatisticsBase, std::pair<std::string, CVC4::SExpr> >; #endif /* SWIGJAVA */ diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp index ee7d1bb87..81eaa3559 100644 --- a/src/util/statistics_registry.cpp +++ b/src/util/statistics_registry.cpp @@ -2,9 +2,9 @@ /*! \file statistics_registry.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Tim King, Kshitij Bansal + ** Morgan Deters, Tim King, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h index 4d4cc76df..69f6105cd 100644 --- a/src/util/statistics_registry.h +++ b/src/util/statistics_registry.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Tim King, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/util/string.cpp b/src/util/string.cpp index ff522ba7b..abe3b01e7 100644 --- a/src/util/string.cpp +++ b/src/util/string.cpp @@ -2,9 +2,9 @@ /*! \file string.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Tianyi Liang, Andrew Reynolds + ** Andrew Reynolds, Tim King, Tianyi Liang ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/util/string.h b/src/util/string.h index 637ffe365..700291aeb 100644 --- a/src/util/string.h +++ b/src/util/string.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Tim King, Tianyi Liang ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/util/tuple.h b/src/util/tuple.h index 13b605794..ff5dd18b3 100644 --- a/src/util/tuple.h +++ b/src/util/tuple.h @@ -2,9 +2,9 @@ /*! \file tuple.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Tim King + ** Morgan Deters, Tim King, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/util/unsafe_interrupt_exception.h b/src/util/unsafe_interrupt_exception.h index 5c8360cdf..0cd390cdd 100644 --- a/src/util/unsafe_interrupt_exception.h +++ b/src/util/unsafe_interrupt_exception.h @@ -2,9 +2,9 @@ /*! \file unsafe_interrupt_exception.h ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean + ** Liana Hadarean, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/util/utility.cpp b/src/util/utility.cpp index acabd8739..b1b86a38b 100644 --- a/src/util/utility.cpp +++ b/src/util/utility.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 diff --git a/src/util/utility.h b/src/util/utility.h index 4477fc7b2..86dd64df9 100644 --- a/src/util/utility.h +++ b/src/util/utility.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Andres Noetzli, Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 |