# > for options where we don't need to detect if set by user (default: OFF)
option(USE_POLY "Use LibPoly for polynomial arithmetic")
option(USE_COCOA "Use CoCoALib for further polynomial operations")
-option(USE_SYMFPU "Use SymFPU for floating point support")
option(USE_PYTHON2 "Force Python 2 (deprecated)")
# Custom install directories for dependencies
endif()
endif()
-if(USE_SYMFPU)
- find_package(SymFPU REQUIRED)
- add_definitions(-DCVC5_USE_SYMFPU)
- set(CVC5_USE_SYMFPU 1)
-else()
- set(CVC5_USE_SYMFPU 0)
-endif()
+find_package(SymFPU REQUIRED)
if(GPL_LIBS)
if(NOT ENABLE_GPL)
print_config("MP library " "gmp")
endif()
print_config("Editline " ${USE_EDITLINE})
-print_config("SymFPU " ${USE_SYMFPU})
message("")
print_config("Api docs " ${BUILD_DOCS})
message("")
- [GMP v6.1 (GNU Multi-Precision arithmetic library)](https://gmplib.org)
- [ANTLR 3.4](http://www.antlr3.org/)
- [Java >= 1.6](https://www.java.com)
+- [SymFPU](https://github.com/martin-cs/symfpu/tree/CVC4)
### ANTLR 3.4 parser generator
not ship static libraries, cvc5 builds GMP automatically when `--auto-download`
is given.
-## Optional Dependencies
-
### SymFPU (Support for the Theory of Floating Point Numbers)
[SymFPU](https://github.com/martin-cs/symfpu/tree/CVC4)
of bit-vector operations.
It is required for supporting the theory of floating-point numbers and
can be downloaded and built automatically.
-Configure cvc5 with `configure.sh --symfpu` to build with this dependency.
+
+## Optional Dependencies
### CaDiCaL (Optional SAT solver)
======================
New Features:
+* SymFPU is now a required dependency.
* New unsat-core production modes based on the new proof infrastructure
(`--unsat-cores-mode=sat-proof`) and on the solving-under-assumption feature
of Minisat (`--unsat-cores-mode=assumptions`). The mode based on SAT
--kissat use the Kissat SAT solver
--poly use the LibPoly library [default=yes]
--cocoa use the CoCoA library
- --symfpu use SymFPU for floating point solver [default=yes]
--editline support the editline library
Optional Path to Optional Packages:
shared=default
static_binary=default
statistics=default
-symfpu=ON
tracing=default
tsan=default
ubsan=default
--statistics) statistics=ON;;
--no-statistics) statistics=OFF;;
- --symfpu) symfpu=ON;;
- --no-symfpu) symfpu=OFF;;
-
--tracing) tracing=ON;;
--no-tracing) tracing=OFF;;
&& cmake_opts="$cmake_opts -DUSE_POLY=$poly"
[ $cocoa != default ] \
&& cmake_opts="$cmake_opts -DUSE_COCOA=$cocoa"
-[ $symfpu != default ] \
- && cmake_opts="$cmake_opts -DUSE_SYMFPU=$symfpu"
[ "$abc_dir" != default ] \
&& cmake_opts="$cmake_opts -DABC_DIR=$abc_dir"
[ "$glpk_dir" != default ] \
System.loadLibrary("cvc4jni");
// Test whether CVC4 was built with floating-point support
- if (!Configuration.isBuiltWithSymFPU()) {
- System.out.println("CVC4 was built without floating-point support.");
- System.out.println("Configure with --symfpu and rebuild CVC4 to run");
- System.out.println("this example.");
- System.exit(77);
- }
-
ExprManager em = new ExprManager();
SmtEngine smt = new SmtEngine(em);
if __name__ == "__main__":
slv = pycvc5.Solver()
- if not slv.supportsFloatingPoint():
- # cvc5 must be built with SymFPU to support the theory of
- # floating-point numbers
- print("cvc5 was not built with floating-point support.")
- exit()
-
slv.setOption("produce-models", "true")
slv.setLogic("QF_FP")
if(USE_POLY)
target_link_libraries(cvc5 PRIVATE Polyxx)
endif()
-if(USE_SYMFPU)
- target_link_libraries(cvc5 PRIVATE SymFPU)
-endif()
+
+target_link_libraries(cvc5 PRIVATE SymFPU)
# Note: When linked statically GMP needs to be linked after CLN since CLN
# depends on GMP.
<< " children (the one under construction has " << nchildren << ")";
}
-/* Solver Configuration */
-/* -------------------------------------------------------------------------- */
-
-bool Solver::supportsFloatingPoint() const
-{
- CVC5_API_TRY_CATCH_BEGIN;
- //////// all checks before this line
- return Configuration::isBuiltWithSymFPU();
- ////////
- CVC5_API_TRY_CATCH_END;
-}
-
/* Sorts Handling */
/* -------------------------------------------------------------------------- */
{
NodeManagerScope scope(getNodeManager());
CVC5_API_TRY_CATCH_BEGIN;
- CVC5_API_CHECK(Configuration::isBuiltWithSymFPU())
- << "Expected cvc5 to be compiled with SymFPU support";
//////// all checks before this line
return Sort(this, getNodeManager()->roundingModeType());
////////
{
NodeManagerScope scope(getNodeManager());
CVC5_API_TRY_CATCH_BEGIN;
- CVC5_API_CHECK(Configuration::isBuiltWithSymFPU())
- << "Expected cvc5 to be compiled with SymFPU support";
CVC5_API_ARG_CHECK_EXPECTED(exp > 0, exp) << "exponent size > 0";
CVC5_API_ARG_CHECK_EXPECTED(sig > 0, sig) << "significand size > 0";
//////// all checks before this line
{
NodeManagerScope scope(getNodeManager());
CVC5_API_TRY_CATCH_BEGIN;
- CVC5_API_CHECK(Configuration::isBuiltWithSymFPU())
- << "Expected cvc5 to be compiled with SymFPU support";
//////// all checks before this line
return mkValHelper<cvc5::FloatingPoint>(
FloatingPoint::makeInf(FloatingPointSize(exp, sig), false));
{
NodeManagerScope scope(getNodeManager());
CVC5_API_TRY_CATCH_BEGIN;
- CVC5_API_CHECK(Configuration::isBuiltWithSymFPU())
- << "Expected cvc5 to be compiled with SymFPU support";
//////// all checks before this line
return mkValHelper<cvc5::FloatingPoint>(
FloatingPoint::makeInf(FloatingPointSize(exp, sig), true));
{
NodeManagerScope scope(getNodeManager());
CVC5_API_TRY_CATCH_BEGIN;
- CVC5_API_CHECK(Configuration::isBuiltWithSymFPU())
- << "Expected cvc5 to be compiled with SymFPU support";
//////// all checks before this line
return mkValHelper<cvc5::FloatingPoint>(
FloatingPoint::makeNaN(FloatingPointSize(exp, sig)));
{
NodeManagerScope scope(getNodeManager());
CVC5_API_TRY_CATCH_BEGIN;
- CVC5_API_CHECK(Configuration::isBuiltWithSymFPU())
- << "Expected cvc5 to be compiled with SymFPU support";
//////// all checks before this line
return mkValHelper<cvc5::FloatingPoint>(
FloatingPoint::makeZero(FloatingPointSize(exp, sig), false));
{
NodeManagerScope scope(getNodeManager());
CVC5_API_TRY_CATCH_BEGIN;
- CVC5_API_CHECK(Configuration::isBuiltWithSymFPU())
- << "Expected cvc5 to be compiled with SymFPU support";
//////// all checks before this line
return mkValHelper<cvc5::FloatingPoint>(
FloatingPoint::makeZero(FloatingPointSize(exp, sig), true));
{
NodeManagerScope scope(getNodeManager());
CVC5_API_TRY_CATCH_BEGIN;
- CVC5_API_CHECK(Configuration::isBuiltWithSymFPU())
- << "Expected cvc5 to be compiled with SymFPU support";
//////// all checks before this line
return mkValHelper<cvc5::RoundingMode>(s_rmodes.at(rm));
////////
{
NodeManagerScope scope(getNodeManager());
CVC5_API_TRY_CATCH_BEGIN;
- CVC5_API_CHECK(Configuration::isBuiltWithSymFPU())
- << "Expected cvc5 to be compiled with SymFPU support";
CVC5_API_SOLVER_CHECK_TERM(val);
CVC5_API_ARG_CHECK_EXPECTED(exp > 0, exp) << "a value > 0";
CVC5_API_ARG_CHECK_EXPECTED(sig > 0, sig) << "a value > 0";
Solver(const Solver&) = delete;
Solver& operator=(const Solver&) = delete;
- /* .................................................................... */
- /* Solver Configuration */
- /* .................................................................... */
-
- bool supportsFloatingPoint() const;
-
/* .................................................................... */
/* Sorts Handling */
/* .................................................................... */
cdef cppclass Solver:
Solver(Options*) except +
- bint supportsFloatingPoint() except +
Sort getBooleanSort() except +
Sort getIntegerSort() except +
Sort getRealSort() except +
def __dealloc__(self):
del self.csolver
- def supportsFloatingPoint(self):
- return self.csolver.supportsFloatingPoint()
-
def getBooleanSort(self):
cdef Sort sort = Sort(self)
sort.csort = self.csolver.getBooleanSort()
if (Configuration::isBuiltWithAbc() || Configuration::isBuiltWithCadical()
|| Configuration::isBuiltWithCryptominisat()
|| Configuration::isBuiltWithKissat()
- || Configuration::isBuiltWithSymFPU()
|| Configuration::isBuiltWithEditline())
{
ss << "This version of cvc5 is linked against the following non-(L)GPL'ed\n"
<< " See https://fmv.jku.at/kissat for copyright "
<< "information.\n\n";
}
- if (Configuration::isBuiltWithSymFPU())
- {
- ss << " SymFPU - The Symbolic Floating Point Unit\n"
- << " See https://github.com/martin-cs/symfpu/tree/cvc5 for copyright "
- << "information.\n\n";
- }
if (Configuration::isBuiltWithEditline())
{
ss << " Editline Library\n"
}
}
+ ss << " SymFPU - The Symbolic Floating Point Unit\n"
+ << " See https://github.com/martin-cs/symfpu/tree/cvc5 for copyright "
+ << "information.\n\n";
+
if (Configuration::isBuiltWithGmp() || Configuration::isBuiltWithPoly())
{
ss << "This version of cvc5 is linked against the following third party\n"
return IS_POLY_BUILD;
}
-bool Configuration::isBuiltWithSymFPU() { return IS_SYMFPU_BUILD; }
-
unsigned Configuration::getNumDebugTags() {
#if defined(CVC5_DEBUG) && defined(CVC5_TRACING)
/* -1 because a NULL pointer is inserted as the last value */
static bool isBuiltWithPoly();
- static bool isBuiltWithSymFPU();
-
/* Return the number of debug tags */
static unsigned getNumDebugTags();
/* Return a sorted array of the debug tags name */
#define IS_EDITLINE_BUILD false
#endif /* HAVE_LIBEDITLINE */
-#ifdef CVC5_USE_SYMFPU
-#define IS_SYMFPU_BUILD true
-#else /* HAVE_SYMFPU_HEADERS */
-#define IS_SYMFPU_BUILD false
-#endif /* HAVE_SYMFPU_HEADERS */
-
#if CVC5_GPL_DEPS
# define IS_GPL_BUILD true
#else /* CVC5_GPL_DEPS */
print_config_cond("kissat", Configuration::isBuiltWithKissat());
print_config_cond("poly", Configuration::isBuiltWithPoly());
print_config_cond("editline", Configuration::isBuiltWithEditline());
- print_config_cond("symfpu", Configuration::isBuiltWithSymFPU());
exit(0);
}
#include "util/floatingpoint.h"
#include "util/floatingpoint_literal_symfpu.h"
-#ifdef CVC5_USE_SYMFPU
#include "symfpu/core/add.h"
#include "symfpu/core/classify.h"
#include "symfpu/core/compare.h"
#include "symfpu/core/sqrt.h"
#include "symfpu/utils/numberOfRoundingModes.h"
#include "symfpu/utils/properties.h"
-#endif
-#ifdef CVC5_USE_SYMFPU
namespace symfpu {
using namespace ::cvc5::theory::fp::symfpuSymbolic;
return;
}
};
-#endif
-
-#ifndef CVC5_USE_SYMFPU
-#define SYMFPU_NUMBER_OF_ROUNDING_MODES 5
-#endif
namespace cvc5 {
namespace theory {
bool symbolicRoundingMode::checkNodeType(const TNode n)
{
-#ifdef CVC5_USE_SYMFPU
return n.getType(false).isBitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES);
-#else
- return false;
-#endif
}
symbolicRoundingMode::symbolicRoundingMode(const Node n) : nodeWrapper(n)
Assert(checkNodeType(*this));
}
-#ifdef CVC5_USE_SYMFPU
symbolicRoundingMode::symbolicRoundingMode(const unsigned v)
: nodeWrapper(NodeManager::currentNM()->mkConst(
BitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES, v)))
Assert((v & (v - 1)) == 0 && v != 0); // Exactly one bit set
Assert(checkNodeType(*this));
}
-#else
-symbolicRoundingMode::symbolicRoundingMode(const unsigned v)
- : nodeWrapper(NodeManager::currentNM()->mkConst(
- BitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES, v)))
-{
- Unreachable();
-}
-#endif
symbolicRoundingMode::symbolicRoundingMode(const symbolicRoundingMode &old)
: nodeWrapper(old)
FpConverter::FpConverter(context::UserContext* user)
: d_additionalAssertions(user)
-#ifdef CVC5_USE_SYMFPU
,
d_fpMap(user),
d_rmMap(user),
d_boolMap(user),
d_ubvMap(user),
d_sbvMap(user)
-#endif
{
}
FpConverter::~FpConverter() {}
-#ifdef CVC5_USE_SYMFPU
Node FpConverter::ufToNode(const fpt &format, const uf &u) const
{
NodeManager *nm = NodeManager::currentNM();
return tmp;
}
-#endif
// Non-convertible things should only be added to the stack at the very start,
// thus...
Node FpConverter::convert(TNode node)
{
-#ifdef CVC5_USE_SYMFPU
std::vector<TNode> workStack;
TNode result = node;
}
return result;
-#else
- Unimplemented() << "Conversion is dependent on SymFPU";
-#endif
}
#undef CVC5_FPCONV_PASSTHROUGH
{
Assert(Theory::isLeafOf(var, THEORY_FP));
-#ifdef CVC5_USE_SYMFPU
TypeNode t(var.getType());
Assert(t.isRoundingMode() || t.isFloatingPoint())
Assert(i != d_fpMap.end())
<< "Asking for the value of an unregistered expression";
return ufToNode(fpt(t), (*i).second);
-#else
- Unimplemented() << "Conversion is dependent on SymFPU";
-#endif
}
} // namespace fp
#include "util/floatingpoint_size.h"
#include "util/hash.h"
-#ifdef CVC5_USE_SYMFPU
#include "symfpu/core/unpackedFloat.h"
-#endif
#ifdef CVC5_SYM_SYMBOLIC_EVAL
// This allows debugging of the cvc5 symbolic back-end.
protected:
bool checkNodeType(const TNode node);
-#ifdef CVC5_USE_SYMFPU
friend ::symfpu::ite<symbolicProposition, symbolicProposition>; // For ITE
-#endif
public:
symbolicProposition(const Node n);
protected:
bool checkNodeType(const TNode n);
-#ifdef CVC5_USE_SYMFPU
friend ::symfpu::ite<symbolicProposition, symbolicRoundingMode>; // For ITE
-#endif
public:
symbolicRoundingMode(const Node n);
bool checkNodeType(const TNode n);
friend symbolicBitVector<!isSigned>; // To allow conversion between the types
-#ifdef CVC5_USE_SYMFPU
friend ::symfpu::ite<symbolicProposition,
symbolicBitVector<isSigned> >; // For ITE
-#endif
public:
symbolicBitVector(const Node n);
context::CDList<Node> d_additionalAssertions;
protected:
-#ifdef CVC5_USE_SYMFPU
typedef symfpuSymbolic::traits traits;
typedef ::symfpu::unpackedFloat<symfpuSymbolic::traits> uf;
typedef symfpuSymbolic::traits::rm rm;
/* Creates the relevant components for a variable */
uf buildComponents(TNode current);
-#endif
};
} // namespace fp
void TheoryFp::preRegisterTerm(TNode node)
{
- if (Configuration::isBuiltWithSymFPU() && !options::fpExp())
+ if (!options::fpExp())
{
TypeNode tn = node.getType();
if (tn.isFloatingPoint())
bool result;
switch (k)
{
-#ifdef CVC5_USE_SYMFPU
case kind::FLOATINGPOINT_COMPONENT_NAN: result = arg0.isNaN(); break;
case kind::FLOATINGPOINT_COMPONENT_INF: result = arg0.isInfinite(); break;
case kind::FLOATINGPOINT_COMPONENT_ZERO: result = arg0.isZero(); break;
case kind::FLOATINGPOINT_COMPONENT_SIGN: result = arg0.getSign(); break;
-#endif
default: Unreachable() << "Unknown kind used in componentFlag"; break;
}
// \todo Add a proper interface for this sort of thing to FloatingPoint #1915
return RewriteResponse(
REWRITE_DONE,
-#ifdef CVC5_USE_SYMFPU
NodeManager::currentNM()->mkConst((BitVector)arg0.getExponent())
-#else
- node
-#endif
);
}
return RewriteResponse(
REWRITE_DONE,
-#ifdef CVC5_USE_SYMFPU
NodeManager::currentNM()->mkConst((BitVector)arg0.getSignificand())
-#else
- node
-#endif
);
}
BitVector value;
-#ifdef CVC5_USE_SYMFPU
/* \todo fix the numbering of rounding modes so this doesn't need
* to call symfpu at all and remove the dependency on fp_converter.h #1915 */
RoundingMode arg0(node[0].getConst<RoundingMode>());
Unreachable() << "Unknown rounding mode in roundingModeBitBlast";
break;
}
-#else
- value = BitVector(5U, 0U);
-#endif
return RewriteResponse(REWRITE_DONE,
NodeManager::currentNM()->mkConst(value));
}
}
}
-#ifdef CVC5_USE_SYMFPU
/* Need to create some symfpu objects as the size of bit-vector
* that is needed for this component is dependent on the encoding
* used (i.e. whether subnormals are forcibly normalised or not).
* back-end but it should't make a difference. */
FloatingPointSize fps = operandType.getConst<FloatingPointSize>();
uint32_t bw = FloatingPoint::getUnpackedExponentWidth(fps);
-#else
- uint32_t bw = 2;
-#endif
return nodeManager->mkBitVectorType(bw);
}
}
}
-#ifdef CVC5_USE_SYMFPU
/* As before we need to use some of sympfu. */
FloatingPointSize fps = operandType.getConst<FloatingPointSize>();
uint32_t bw = FloatingPoint::getUnpackedSignificandWidth(fps);
-#else
- uint32_t bw = 1;
-#endif
return nodeManager->mkBitVectorType(bw);
}
{
for (TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id)
{
- if (id == THEORY_FP && !Configuration::isBuiltWithSymFPU())
- {
- continue;
- }
enableTheory(id);
}
}
# The build system configuration.
##
-configure_file(floatingpoint_literal_symfpu.h.in floatingpoint_literal_symfpu.h)
-configure_file(floatingpoint_literal_symfpu_traits.h.in
- floatingpoint_literal_symfpu_traits.h)
configure_file(rational.h.in rational.h)
configure_file(integer.h.in integer.h)
configure_file(real_algebraic_number.h.in real_algebraic_number.h)
#include "base/check.h"
-#ifdef CVC5_USE_SYMFPU
#include "symfpu/core/add.h"
#include "symfpu/core/classify.h"
#include "symfpu/core/compare.h"
#include "symfpu/core/sqrt.h"
#include "symfpu/utils/numberOfRoundingModes.h"
#include "symfpu/utils/properties.h"
-#endif
/* -------------------------------------------------------------------------- */
-#ifdef CVC5_USE_SYMFPU
namespace symfpu {
#define CVC5_LIT_ITE_DFN(T) \
#undef CVC5_LIT_ITE_DFN
} // namespace symfpu
-#endif
/* -------------------------------------------------------------------------- */
uint32_t FloatingPointLiteral::getUnpackedExponentWidth(FloatingPointSize& size)
{
-#ifdef CVC5_USE_SYMFPU
return SymFPUUnpackedFloatLiteral::exponentWidth(size);
-#else
- unimplemented();
- return 2;
-#endif
}
uint32_t FloatingPointLiteral::getUnpackedSignificandWidth(
FloatingPointSize& size)
{
-#ifdef CVC5_USE_SYMFPU
return SymFPUUnpackedFloatLiteral::significandWidth(size);
-#else
- unimplemented();
- return 2;
-#endif
}
FloatingPointLiteral::FloatingPointLiteral(uint32_t exp_size,
uint32_t sig_size,
const BitVector& bv)
: d_fp_size(exp_size, sig_size)
-#ifdef CVC5_USE_SYMFPU
,
d_symuf(symfpu::unpack<symfpuLiteral::traits>(
symfpuLiteral::Cvc5FPSize(exp_size, sig_size), bv))
-#endif
{
}
FloatingPointLiteral::FloatingPointLiteral(
const FloatingPointSize& size, FloatingPointLiteral::SpecialConstKind kind)
: d_fp_size(size)
-#ifdef CVC5_USE_SYMFPU
,
d_symuf(SymFPUUnpackedFloatLiteral::makeNaN(size))
-#endif
{
Assert(kind == FloatingPointLiteral::SpecialConstKind::FPNAN);
}
FloatingPointLiteral::SpecialConstKind kind,
bool sign)
: d_fp_size(size)
-#ifdef CVC5_USE_SYMFPU
,
d_symuf(kind == FloatingPointLiteral::SpecialConstKind::FPINF
? SymFPUUnpackedFloatLiteral::makeInf(size, sign)
: SymFPUUnpackedFloatLiteral::makeZero(size, sign))
-#endif
{
Assert(kind == FloatingPointLiteral::SpecialConstKind::FPINF
|| kind == FloatingPointLiteral::SpecialConstKind::FPZERO);
FloatingPointLiteral::FloatingPointLiteral(const FloatingPointSize& size,
const BitVector& bv)
: d_fp_size(size)
-#ifdef CVC5_USE_SYMFPU
,
d_symuf(symfpu::unpack<symfpuLiteral::traits>(size, bv))
-#endif
{
}
const BitVector& bv,
bool signedBV)
: d_fp_size(size)
-#ifdef CVC5_USE_SYMFPU
,
d_symuf(signedBV ? symfpu::convertSBVToFloat<symfpuLiteral::traits>(
symfpuLiteral::Cvc5FPSize(size),
symfpuLiteral::Cvc5FPSize(size),
symfpuLiteral::Cvc5RM(rm),
symfpuLiteral::Cvc5UnsignedBitVector(bv)))
-#endif
{
}
BitVector FloatingPointLiteral::pack(void) const
{
-#ifdef CVC5_USE_SYMFPU
BitVector bv(symfpu::pack<symfpuLiteral::traits>(d_fp_size, d_symuf));
-#else
- unimplemented();
- BitVector bv(4u, 0u);
-#endif
return bv;
}
FloatingPointLiteral FloatingPointLiteral::absolute(void) const
{
-#ifdef CVC5_USE_SYMFPU
return FloatingPointLiteral(
d_fp_size, symfpu::absolute<symfpuLiteral::traits>(d_fp_size, d_symuf));
-#else
- unimplemented();
- return *this;
-#endif
}
FloatingPointLiteral FloatingPointLiteral::negate(void) const
{
-#ifdef CVC5_USE_SYMFPU
return FloatingPointLiteral(
d_fp_size, symfpu::negate<symfpuLiteral::traits>(d_fp_size, d_symuf));
-#else
- unimplemented();
- return *this;
-#endif
}
FloatingPointLiteral FloatingPointLiteral::add(
const RoundingMode& rm, const FloatingPointLiteral& arg) const
{
-#ifdef CVC5_USE_SYMFPU
Assert(d_fp_size == arg.d_fp_size);
return FloatingPointLiteral(d_fp_size,
symfpu::add<symfpuLiteral::traits>(
d_fp_size, rm, d_symuf, arg.d_symuf, true));
-#else
- unimplemented();
- return *this;
-#endif
}
FloatingPointLiteral FloatingPointLiteral::sub(
const RoundingMode& rm, const FloatingPointLiteral& arg) const
{
-#ifdef CVC5_USE_SYMFPU
Assert(d_fp_size == arg.d_fp_size);
return FloatingPointLiteral(d_fp_size,
symfpu::add<symfpuLiteral::traits>(
d_fp_size, rm, d_symuf, arg.d_symuf, false));
-#else
- unimplemented();
- return *this;
-#endif
}
FloatingPointLiteral FloatingPointLiteral::mult(
const RoundingMode& rm, const FloatingPointLiteral& arg) const
{
-#ifdef CVC5_USE_SYMFPU
Assert(d_fp_size == arg.d_fp_size);
return FloatingPointLiteral(d_fp_size,
symfpu::multiply<symfpuLiteral::traits>(
d_fp_size, rm, d_symuf, arg.d_symuf));
-#else
- unimplemented();
- return *this;
-#endif
}
FloatingPointLiteral FloatingPointLiteral::div(
const RoundingMode& rm, const FloatingPointLiteral& arg) const
{
-#ifdef CVC5_USE_SYMFPU
Assert(d_fp_size == arg.d_fp_size);
return FloatingPointLiteral(d_fp_size,
symfpu::divide<symfpuLiteral::traits>(
d_fp_size, rm, d_symuf, arg.d_symuf));
-#else
- unimplemented();
- return *this;
-#endif
}
FloatingPointLiteral FloatingPointLiteral::fma(
const FloatingPointLiteral& arg1,
const FloatingPointLiteral& arg2) const
{
-#ifdef CVC5_USE_SYMFPU
Assert(d_fp_size == arg1.d_fp_size);
Assert(d_fp_size == arg2.d_fp_size);
return FloatingPointLiteral(
d_fp_size,
symfpu::fma<symfpuLiteral::traits>(
d_fp_size, rm, d_symuf, arg1.d_symuf, arg2.d_symuf));
-#else
- unimplemented();
- return *this;
-#endif
}
FloatingPointLiteral FloatingPointLiteral::sqrt(const RoundingMode& rm) const
{
-#ifdef CVC5_USE_SYMFPU
return FloatingPointLiteral(
d_fp_size, symfpu::sqrt<symfpuLiteral::traits>(d_fp_size, rm, d_symuf));
-#else
- unimplemented();
- return *this;
-#endif
}
FloatingPointLiteral FloatingPointLiteral::rti(const RoundingMode& rm) const
{
-#ifdef CVC5_USE_SYMFPU
return FloatingPointLiteral(
d_fp_size,
symfpu::roundToIntegral<symfpuLiteral::traits>(d_fp_size, rm, d_symuf));
-#else
- unimplemented();
- return *this;
-#endif
}
FloatingPointLiteral FloatingPointLiteral::rem(
const FloatingPointLiteral& arg) const
{
-#ifdef CVC5_USE_SYMFPU
Assert(d_fp_size == arg.d_fp_size);
return FloatingPointLiteral(d_fp_size,
symfpu::remainder<symfpuLiteral::traits>(
d_fp_size, d_symuf, arg.d_symuf));
-#else
- unimplemented();
- return *this;
-#endif
}
FloatingPointLiteral FloatingPointLiteral::maxTotal(
const FloatingPointLiteral& arg, bool zeroCaseLeft) const
{
-#ifdef CVC5_USE_SYMFPU
Assert(d_fp_size == arg.d_fp_size);
return FloatingPointLiteral(
d_fp_size,
symfpu::max<symfpuLiteral::traits>(
d_fp_size, d_symuf, arg.d_symuf, zeroCaseLeft));
-#else
- unimplemented();
- return *this;
-#endif
}
FloatingPointLiteral FloatingPointLiteral::minTotal(
const FloatingPointLiteral& arg, bool zeroCaseLeft) const
{
-#ifdef CVC5_USE_SYMFPU
Assert(d_fp_size == arg.d_fp_size);
return FloatingPointLiteral(
d_fp_size,
symfpu::min<symfpuLiteral::traits>(
d_fp_size, d_symuf, arg.d_symuf, zeroCaseLeft));
-#else
- unimplemented();
- return *this;
-#endif
}
bool FloatingPointLiteral::operator==(const FloatingPointLiteral& fp) const
{
-#ifdef CVC5_USE_SYMFPU
return ((d_fp_size == fp.d_fp_size)
&& symfpu::smtlibEqual<symfpuLiteral::traits>(
d_fp_size, d_symuf, fp.d_symuf));
-#else
- unimplemented();
- return ((d_fp_size == fp.d_fp_size));
-#endif
}
bool FloatingPointLiteral::operator<=(const FloatingPointLiteral& arg) const
{
-#ifdef CVC5_USE_SYMFPU
Assert(d_fp_size == arg.d_fp_size);
return symfpu::lessThanOrEqual<symfpuLiteral::traits>(
d_fp_size, d_symuf, arg.d_symuf);
-#else
- unimplemented();
- return false;
-#endif
}
bool FloatingPointLiteral::operator<(const FloatingPointLiteral& arg) const
{
-#ifdef CVC5_USE_SYMFPU
Assert(d_fp_size == arg.d_fp_size);
return symfpu::lessThan<symfpuLiteral::traits>(
d_fp_size, d_symuf, arg.d_symuf);
-#else
- unimplemented();
- return false;
-#endif
}
BitVector FloatingPointLiteral::getExponent() const
{
-#ifdef CVC5_USE_SYMFPU
return d_symuf.exponent;
-#else
- unimplemented();
- Unreachable() << "no concrete implementation of FloatingPointLiteral";
- return BitVector();
-#endif
}
BitVector FloatingPointLiteral::getSignificand() const
{
-#ifdef CVC5_USE_SYMFPU
return d_symuf.significand;
-#else
- unimplemented();
- Unreachable() << "no concrete implementation of FloatingPointLiteral";
- return BitVector();
-#endif
}
bool FloatingPointLiteral::getSign() const
{
-#ifdef CVC5_USE_SYMFPU
return d_symuf.sign;
-#else
- unimplemented();
- Unreachable() << "no concrete implementation of FloatingPointLiteral";
- return false;
-#endif
}
bool FloatingPointLiteral::isNormal(void) const
{
-#ifdef CVC5_USE_SYMFPU
return symfpu::isNormal<symfpuLiteral::traits>(d_fp_size, d_symuf);
-#else
- unimplemented();
- return false;
-#endif
}
bool FloatingPointLiteral::isSubnormal(void) const
{
-#ifdef CVC5_USE_SYMFPU
return symfpu::isSubnormal<symfpuLiteral::traits>(d_fp_size, d_symuf);
-#else
- unimplemented();
- return false;
-#endif
}
bool FloatingPointLiteral::isZero(void) const
{
-#ifdef CVC5_USE_SYMFPU
return symfpu::isZero<symfpuLiteral::traits>(d_fp_size, d_symuf);
-#else
- unimplemented();
- return false;
-#endif
}
bool FloatingPointLiteral::isInfinite(void) const
{
-#ifdef CVC5_USE_SYMFPU
return symfpu::isInfinite<symfpuLiteral::traits>(d_fp_size, d_symuf);
-#else
- unimplemented();
- return false;
-#endif
}
bool FloatingPointLiteral::isNaN(void) const
{
-#ifdef CVC5_USE_SYMFPU
return symfpu::isNaN<symfpuLiteral::traits>(d_fp_size, d_symuf);
-#else
- unimplemented();
- return false;
-#endif
}
bool FloatingPointLiteral::isNegative(void) const
{
-#ifdef CVC5_USE_SYMFPU
return symfpu::isNegative<symfpuLiteral::traits>(d_fp_size, d_symuf);
-#else
- unimplemented();
- return false;
-#endif
}
bool FloatingPointLiteral::isPositive(void) const
{
-#ifdef CVC5_USE_SYMFPU
return symfpu::isPositive<symfpuLiteral::traits>(d_fp_size, d_symuf);
-#else
- unimplemented();
- return false;
-#endif
}
FloatingPointLiteral FloatingPointLiteral::convert(
const FloatingPointSize& target, const RoundingMode& rm) const
{
-#ifdef CVC5_USE_SYMFPU
return FloatingPointLiteral(
target,
symfpu::convertFloatToFloat<symfpuLiteral::traits>(
d_fp_size, target, rm, d_symuf));
-#else
- unimplemented();
- return *this;
-#endif
}
BitVector FloatingPointLiteral::convertToSBVTotal(BitVectorSize width,
const RoundingMode& rm,
BitVector undefinedCase) const
{
-#ifdef CVC5_USE_SYMFPU
return symfpu::convertFloatToSBV<symfpuLiteral::traits>(
d_fp_size, rm, d_symuf, width, undefinedCase);
-#else
- unimplemented();
- return undefinedCase;
-#endif
}
BitVector FloatingPointLiteral::convertToUBVTotal(BitVectorSize width,
const RoundingMode& rm,
BitVector undefinedCase) const
{
-#ifdef CVC5_USE_SYMFPU
return symfpu::convertFloatToUBV<symfpuLiteral::traits>(
d_fp_size, rm, d_symuf, width, undefinedCase);
-#else
- unimplemented();
- return undefinedCase;
-#endif
}
-#ifndef CVC5_USE_SYMFPU
-void FloatingPointLiteral::unimplemented(void)
-{
- Unimplemented() << "no concrete implementation of FloatingPointLiteral";
-}
-
-size_t FloatingPointLiteral::hash(void) const
-{
- unimplemented();
- return 23;
-}
-#endif
-
} // namespace cvc5
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Aina Niemetz, Andres Noetzli
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * SymFPU glue code for floating-point values.
+ *
+ * !!! This header is not to be included in any other headers !!!
+ */
+#include "cvc5_public.h"
+
+#ifndef CVC5__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_H
+#define CVC5__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_H
+
+#include "util/bitvector.h"
+#include "util/floatingpoint_literal_symfpu_traits.h"
+#include "util/floatingpoint_size.h"
+#include "util/roundingmode.h"
+
+/* -------------------------------------------------------------------------- */
+
+namespace cvc5 {
+
+using SymFPUUnpackedFloatLiteral =
+ ::symfpu::unpackedFloat<symfpuLiteral::traits>;
+
+class FloatingPointLiteral
+{
+ friend class FloatingPoint;
+
+ public:
+ /**
+ * The kind of floating-point special constants that can be created via the
+ * corresponding constructor.
+ * These are prefixed with FP because of name clashes with NAN.
+ */
+ enum SpecialConstKind
+ {
+ FPINF, // +-oo
+ FPNAN, // NaN
+ FPZERO, // +-zero
+ };
+
+ /**
+ * Get the number of exponent bits in the unpacked format corresponding to a
+ * given packed format. This is the unpacked counter-part of
+ * FloatingPointSize::exponentWidth().
+ */
+ static uint32_t getUnpackedExponentWidth(FloatingPointSize& size);
+ /**
+ * Get the number of exponent bits in the unpacked format corresponding to a
+ * given packed format. This is the unpacked counter-part of
+ * FloatingPointSize::significandWidth().
+ */
+ static uint32_t getUnpackedSignificandWidth(FloatingPointSize& size);
+
+ /** Constructors. */
+
+ /** Create a FP literal from its IEEE bit-vector representation. */
+ FloatingPointLiteral(uint32_t exp_size,
+ uint32_t sig_size,
+ const BitVector& bv);
+ FloatingPointLiteral(const FloatingPointSize& size, const BitVector& bv);
+
+ /** Create a FP literal that represents a special constants. */
+ FloatingPointLiteral(const FloatingPointSize& size, SpecialConstKind kind);
+ FloatingPointLiteral(const FloatingPointSize& size,
+ SpecialConstKind kind,
+ bool sign);
+
+ /**
+ * Create a FP literal from a signed or unsigned bit-vector value with
+ * respect to given rounding mode.
+ */
+ FloatingPointLiteral(const FloatingPointSize& size,
+ const RoundingMode& rm,
+ const BitVector& bv,
+ bool signedBV);
+
+ ~FloatingPointLiteral() {}
+
+ /** Return the size of this FP literal. */
+ const FloatingPointSize& getSize() const { return d_fp_size; };
+
+ /** Return the packed (IEEE-754) representation of this literal. */
+ BitVector pack(void) const;
+
+ /** Floating-point absolute value literal. */
+ FloatingPointLiteral absolute(void) const;
+ /** Floating-point negation literal. */
+ FloatingPointLiteral negate(void) const;
+ /** Floating-point addition literal. */
+ FloatingPointLiteral add(const RoundingMode& rm,
+ const FloatingPointLiteral& arg) const;
+ /** Floating-point subtraction literal. */
+ FloatingPointLiteral sub(const RoundingMode& rm,
+ const FloatingPointLiteral& arg) const;
+ /** Floating-point multiplication literal. */
+ FloatingPointLiteral mult(const RoundingMode& rm,
+ const FloatingPointLiteral& arg) const;
+ /** Floating-point division literal. */
+ FloatingPointLiteral div(const RoundingMode& rm,
+ const FloatingPointLiteral& arg) const;
+ /** Floating-point fused multiplication and addition literal. */
+ FloatingPointLiteral fma(const RoundingMode& rm,
+ const FloatingPointLiteral& arg1,
+ const FloatingPointLiteral& arg2) const;
+ /** Floating-point square root literal. */
+ FloatingPointLiteral sqrt(const RoundingMode& rm) const;
+ /** Floating-point round to integral literal. */
+ FloatingPointLiteral rti(const RoundingMode& rm) const;
+ /** Floating-point remainder literal. */
+ FloatingPointLiteral rem(const FloatingPointLiteral& arg) const;
+
+ /**
+ * Floating-point max literal (total version).
+ * zeroCase: true to return the left (rather than the right operand) in case
+ * of max(-0,+0) or max(+0,-0).
+ */
+ FloatingPointLiteral maxTotal(const FloatingPointLiteral& arg,
+ bool zeroCaseLeft) const;
+ /**
+ * Floating-point min literal (total version).
+ * zeroCase: true to return the left (rather than the right operand) in case
+ * of min(-0,+0) or min(+0,-0).
+ */
+ FloatingPointLiteral minTotal(const FloatingPointLiteral& arg,
+ bool zeroCaseLeft) const;
+
+ /** Equality literal (NOT: fp.eq but =) over floating-point values. */
+ bool operator==(const FloatingPointLiteral& fp) const;
+ /** Floating-point less or equal than literal. */
+ bool operator<=(const FloatingPointLiteral& arg) const;
+ /** Floating-point less than literal. */
+ bool operator<(const FloatingPointLiteral& arg) const;
+
+ /** Get the exponent of this floating-point value. */
+ BitVector getExponent() const;
+ /** Get the significand of this floating-point value. */
+ BitVector getSignificand() const;
+ /** True if this value is a negative value. */
+ bool getSign() const;
+
+ /** Return true if this literal represents a normal value. */
+ bool isNormal(void) const;
+ /** Return true if this literal represents a subnormal value. */
+ bool isSubnormal(void) const;
+ /** Return true if this literal represents a zero value. */
+ bool isZero(void) const;
+ /** Return true if this literal represents an infinite value. */
+ bool isInfinite(void) const;
+ /** Return true if this literal represents a NaN value. */
+ bool isNaN(void) const;
+ /** Return true if this literal represents a negative value. */
+ bool isNegative(void) const;
+ /** Return true if this literal represents a positive value. */
+ bool isPositive(void) const;
+
+ /**
+ * Convert this floating-point literal to a literal of given size, with
+ * respect to given rounding mode.
+ */
+ FloatingPointLiteral convert(const FloatingPointSize& target,
+ const RoundingMode& rm) const;
+
+ /**
+ * Convert this floating-point literal to a signed bit-vector of given size,
+ * with respect to given rounding mode (total version).
+ * Returns given bit-vector 'undefinedCase' in the undefined case.
+ */
+ BitVector convertToSBVTotal(BitVectorSize width,
+ const RoundingMode& rm,
+ BitVector undefinedCase) const;
+ /**
+ * Convert this floating-point literal to an unsigned bit-vector of given
+ * size, with respect to given rounding mode (total version).
+ * Returns given bit-vector 'undefinedCase' in the undefined case.
+ */
+ BitVector convertToUBVTotal(BitVectorSize width,
+ const RoundingMode& rm,
+ BitVector undefinedCase) const;
+ /** Return wrapped floating-point literal. */
+ const SymFPUUnpackedFloatLiteral& getSymUF() const { return d_symuf; }
+
+ private:
+ /**
+ * Create a FP literal from unpacked representation.
+ *
+ * This unpacked representation accounts for additional bits required for the
+ * exponent to allow subnormals to be normalized.
+ *
+ * This should NOT be used to create a literal from its IEEE bit-vector
+ * representation -- for this, the above constructor is to be used while
+ * creating a SymFPUUnpackedFloatLiteral via symfpu::unpack.
+ */
+ FloatingPointLiteral(const FloatingPointSize& size,
+ const bool sign,
+ const BitVector& exp,
+ const BitVector& sig)
+ : d_fp_size(size), d_symuf(SymFPUUnpackedFloatLiteral(sign, exp, sig))
+ {
+ }
+
+ /** Create a FP literal from a symFPU unpacked float. */
+ FloatingPointLiteral(const FloatingPointSize& size,
+ SymFPUUnpackedFloatLiteral symuf)
+ : d_fp_size(size), d_symuf(symuf){};
+
+ /** The floating-point size of this floating-point literal. */
+ FloatingPointSize d_fp_size;
+ /** The actual floating-point value, a SymFPU unpackedFloat. */
+ SymFPUUnpackedFloatLiteral d_symuf;
+};
+
+/* -------------------------------------------------------------------------- */
+
+} // namespace cvc5
+
+#endif
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Aina Niemetz, Andres Noetzli
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * SymFPU glue code for floating-point values.
- *
- * !!! This header is not to be included in any other headers !!!
- */
-#include "cvc5_public.h"
-
-#ifndef CVC5__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_H
-#define CVC5__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_H
-
-#include "util/bitvector.h"
-#include "util/floatingpoint_size.h"
-#include "util/floatingpoint_literal_symfpu_traits.h"
-#include "util/roundingmode.h"
-
-/* -------------------------------------------------------------------------- */
-
-namespace cvc5 {
-
-// clang-format off
-#if @CVC5_USE_SYMFPU@
-// clang-format on
-using SymFPUUnpackedFloatLiteral =
- ::symfpu::unpackedFloat<symfpuLiteral::traits>;
-#endif
-
-class FloatingPointLiteral
-{
- friend class FloatingPoint;
-
- public:
- /**
- * The kind of floating-point special constants that can be created via the
- * corresponding constructor.
- * These are prefixed with FP because of name clashes with NAN.
- */
- enum SpecialConstKind
- {
- FPINF, // +-oo
- FPNAN, // NaN
- FPZERO, // +-zero
- };
-
- /**
- * Get the number of exponent bits in the unpacked format corresponding to a
- * given packed format. This is the unpacked counter-part of
- * FloatingPointSize::exponentWidth().
- */
- static uint32_t getUnpackedExponentWidth(FloatingPointSize& size);
- /**
- * Get the number of exponent bits in the unpacked format corresponding to a
- * given packed format. This is the unpacked counter-part of
- * FloatingPointSize::significandWidth().
- */
- static uint32_t getUnpackedSignificandWidth(FloatingPointSize& size);
-
-// clang-format off
-#if !@CVC5_USE_SYMFPU@
- // clang-format on
- /** Catch-all for unimplemented functions. */
- static void unimplemented(void);
-#endif
-
- /** Constructors. */
-
- /** Create a FP literal from its IEEE bit-vector representation. */
- FloatingPointLiteral(uint32_t exp_size,
- uint32_t sig_size,
- const BitVector& bv);
- FloatingPointLiteral(const FloatingPointSize& size, const BitVector& bv);
-
- /** Create a FP literal that represents a special constants. */
- FloatingPointLiteral(const FloatingPointSize& size, SpecialConstKind kind);
- FloatingPointLiteral(const FloatingPointSize& size,
- SpecialConstKind kind,
- bool sign);
-
- /**
- * Create a FP literal from a signed or unsigned bit-vector value with
- * respect to given rounding mode.
- */
- FloatingPointLiteral(const FloatingPointSize& size,
- const RoundingMode& rm,
- const BitVector& bv,
- bool signedBV);
-
- ~FloatingPointLiteral() {}
-
- /** Return the size of this FP literal. */
- const FloatingPointSize& getSize() const { return d_fp_size; };
-
- /** Return the packed (IEEE-754) representation of this literal. */
- BitVector pack(void) const;
-
- /** Floating-point absolute value literal. */
- FloatingPointLiteral absolute(void) const;
- /** Floating-point negation literal. */
- FloatingPointLiteral negate(void) const;
- /** Floating-point addition literal. */
- FloatingPointLiteral add(const RoundingMode& rm,
- const FloatingPointLiteral& arg) const;
- /** Floating-point subtraction literal. */
- FloatingPointLiteral sub(const RoundingMode& rm,
- const FloatingPointLiteral& arg) const;
- /** Floating-point multiplication literal. */
- FloatingPointLiteral mult(const RoundingMode& rm,
- const FloatingPointLiteral& arg) const;
- /** Floating-point division literal. */
- FloatingPointLiteral div(const RoundingMode& rm,
- const FloatingPointLiteral& arg) const;
- /** Floating-point fused multiplication and addition literal. */
- FloatingPointLiteral fma(const RoundingMode& rm,
- const FloatingPointLiteral& arg1,
- const FloatingPointLiteral& arg2) const;
- /** Floating-point square root literal. */
- FloatingPointLiteral sqrt(const RoundingMode& rm) const;
- /** Floating-point round to integral literal. */
- FloatingPointLiteral rti(const RoundingMode& rm) const;
- /** Floating-point remainder literal. */
- FloatingPointLiteral rem(const FloatingPointLiteral& arg) const;
-
- /**
- * Floating-point max literal (total version).
- * zeroCase: true to return the left (rather than the right operand) in case
- * of max(-0,+0) or max(+0,-0).
- */
- FloatingPointLiteral maxTotal(const FloatingPointLiteral& arg,
- bool zeroCaseLeft) const;
- /**
- * Floating-point min literal (total version).
- * zeroCase: true to return the left (rather than the right operand) in case
- * of min(-0,+0) or min(+0,-0).
- */
- FloatingPointLiteral minTotal(const FloatingPointLiteral& arg,
- bool zeroCaseLeft) const;
-
- /** Equality literal (NOT: fp.eq but =) over floating-point values. */
- bool operator==(const FloatingPointLiteral& fp) const;
- /** Floating-point less or equal than literal. */
- bool operator<=(const FloatingPointLiteral& arg) const;
- /** Floating-point less than literal. */
- bool operator<(const FloatingPointLiteral& arg) const;
-
- /** Get the exponent of this floating-point value. */
- BitVector getExponent() const;
- /** Get the significand of this floating-point value. */
- BitVector getSignificand() const;
- /** True if this value is a negative value. */
- bool getSign() const;
-
- /** Return true if this literal represents a normal value. */
- bool isNormal(void) const;
- /** Return true if this literal represents a subnormal value. */
- bool isSubnormal(void) const;
- /** Return true if this literal represents a zero value. */
- bool isZero(void) const;
- /** Return true if this literal represents an infinite value. */
- bool isInfinite(void) const;
- /** Return true if this literal represents a NaN value. */
- bool isNaN(void) const;
- /** Return true if this literal represents a negative value. */
- bool isNegative(void) const;
- /** Return true if this literal represents a positive value. */
- bool isPositive(void) const;
-
- /**
- * Convert this floating-point literal to a literal of given size, with
- * respect to given rounding mode.
- */
- FloatingPointLiteral convert(const FloatingPointSize& target,
- const RoundingMode& rm) const;
-
- /**
- * Convert this floating-point literal to a signed bit-vector of given size,
- * with respect to given rounding mode (total version).
- * Returns given bit-vector 'undefinedCase' in the undefined case.
- */
- BitVector convertToSBVTotal(BitVectorSize width,
- const RoundingMode& rm,
- BitVector undefinedCase) const;
- /**
- * Convert this floating-point literal to an unsigned bit-vector of given
- * size, with respect to given rounding mode (total version).
- * Returns given bit-vector 'undefinedCase' in the undefined case.
- */
- BitVector convertToUBVTotal(BitVectorSize width,
- const RoundingMode& rm,
- BitVector undefinedCase) const;
-// clang-format off
-#if @CVC5_USE_SYMFPU@
- // clang-format on
- /** Return wrapped floating-point literal. */
- const SymFPUUnpackedFloatLiteral& getSymUF() const { return d_symuf; }
-#else
- /** Dummy hash function. */
- size_t hash(void) const;
-#endif
-
- private:
-
- /**
- * Create a FP literal from unpacked representation.
- *
- * This unpacked representation accounts for additional bits required for the
- * exponent to allow subnormals to be normalized.
- *
- * This should NOT be used to create a literal from its IEEE bit-vector
- * representation -- for this, the above constructor is to be used while
- * creating a SymFPUUnpackedFloatLiteral via symfpu::unpack.
- */
- FloatingPointLiteral(const FloatingPointSize& size,
- const bool sign,
- const BitVector& exp,
- const BitVector& sig)
- : d_fp_size(size)
-// clang-format off
-#if @CVC5_USE_SYMFPU@
- // clang-format on
- ,
- d_symuf(SymFPUUnpackedFloatLiteral(sign, exp, sig))
-#endif
- {
- }
-
-// clang-format off
-#if @CVC5_USE_SYMFPU@
- // clang-format on
-
- /** Create a FP literal from a symFPU unpacked float. */
- FloatingPointLiteral(const FloatingPointSize& size,
- SymFPUUnpackedFloatLiteral symuf)
- : d_fp_size(size), d_symuf(symuf){};
-#endif
-
- /** The floating-point size of this floating-point literal. */
- FloatingPointSize d_fp_size;
-// clang-format off
-#if @CVC5_USE_SYMFPU@
- // clang-format on
- /** The actual floating-point value, a SymFPU unpackedFloat. */
- SymFPUUnpackedFloatLiteral d_symuf;
-#endif
-};
-
-/* -------------------------------------------------------------------------- */
-
-} // namespace cvc5
-
-#endif
* SymFPU glue code for floating-point values.
*/
-#if CVC5_USE_SYMFPU
-
#include "util/floatingpoint_literal_symfpu_traits.h"
#include "base/check.h"
}
} // namespace symfpuLiteral
} // namespace cvc5
-#endif
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Aina Niemetz, Martin Brain, Andres Noetzli
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * SymFPU glue code for floating-point values.
+ *
+ * !!! This header is only to be included in floating-point literal headers !!!
+ *
+ * This is a symfpu literal "back-end". It allows the library to be used as
+ * an arbitrary precision floating-point implementation. This is effectively
+ * the glue between symfpu's notion of "signed bit-vector" and cvc5's
+ * BitVector.
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_TRAITS_H
+#define CVC5__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_TRAITS_H
+
+#include <symfpu/core/unpackedFloat.h>
+
+#include "util/bitvector.h"
+#include "util/floatingpoint_size.h"
+#include "util/roundingmode.h"
+
+/* -------------------------------------------------------------------------- */
+
+namespace cvc5 {
+namespace symfpuLiteral {
+
+/**
+ * Forward declaration of wrapper so that traits can be defined early and so
+ * used in the implementation of wrappedBitVector.
+ */
+template <bool T>
+class wrappedBitVector;
+
+using Cvc5BitWidth = uint32_t;
+using Cvc5Prop = bool;
+using Cvc5RM = ::cvc5::RoundingMode;
+using Cvc5FPSize = ::cvc5::FloatingPointSize;
+using Cvc5UnsignedBitVector = wrappedBitVector<false>;
+using Cvc5SignedBitVector = wrappedBitVector<true>;
+
+/**
+ * This is the template parameter for symfpu's templates.
+ */
+class traits
+{
+ public:
+ /** The six key types that symfpu uses. */
+ using bwt = Cvc5BitWidth; // bit-width type
+ using prop = Cvc5Prop; // boolean type
+ using rm = Cvc5RM; // rounding-mode type
+ using fpt = Cvc5FPSize; // floating-point format type
+ using ubv = Cvc5UnsignedBitVector; // unsigned bit-vector type
+ using sbv = Cvc5SignedBitVector; // signed bit-vector type
+
+ /** Give concrete instances of each rounding mode, mainly for comparisons. */
+ static rm RNE(void);
+ static rm RNA(void);
+ static rm RTP(void);
+ static rm RTN(void);
+ static rm RTZ(void);
+
+ /** The sympfu properties. */
+ static void precondition(const prop& p);
+ static void postcondition(const prop& p);
+ static void invariant(const prop& p);
+};
+
+/**
+ * Type function for mapping between types.
+ */
+template <bool T>
+struct signedToLiteralType;
+
+template <>
+struct signedToLiteralType<true>
+{
+ using literalType = int32_t;
+};
+template <>
+struct signedToLiteralType<false>
+{
+ using literalType = uint32_t;
+};
+
+/**
+ * This extends the interface for cvc5::BitVector for compatibility with symFPU.
+ * The template parameter distinguishes signed and unsigned bit-vectors, a
+ * distinction symfpu uses.
+ */
+template <bool isSigned>
+class wrappedBitVector : public BitVector
+{
+ protected:
+ using literalType = typename signedToLiteralType<isSigned>::literalType;
+ friend wrappedBitVector<!isSigned>; // To allow conversion between types
+
+ friend ::symfpu::ite<Cvc5Prop, wrappedBitVector<isSigned> >; // For ITE
+
+ public:
+ /** Constructors. */
+ wrappedBitVector(const Cvc5BitWidth w, const uint32_t v) : BitVector(w, v) {}
+ wrappedBitVector(const Cvc5Prop& p) : BitVector(1, p ? 1U : 0U) {}
+ wrappedBitVector(const wrappedBitVector<isSigned>& old) : BitVector(old) {}
+ wrappedBitVector(const BitVector& old) : BitVector(old) {}
+
+ /** Get the bit-width of this wrapped bit-vector. */
+ Cvc5BitWidth getWidth(void) const { return getSize(); }
+
+ /** Create a zero value of given bit-width 'w'. */
+ static wrappedBitVector<isSigned> one(const Cvc5BitWidth& w);
+ /** Create a one value of given bit-width 'w'. */
+ static wrappedBitVector<isSigned> zero(const Cvc5BitWidth& w);
+ /** Create a ones value (all bits 1) of given bit-width 'w'. */
+ static wrappedBitVector<isSigned> allOnes(const Cvc5BitWidth& w);
+ /** Create a maximum signed/unsigned value of given bit-width 'w'. */
+ static wrappedBitVector<isSigned> maxValue(const Cvc5BitWidth& w);
+ /** Create a minimum signed/unsigned value of given bit-width 'w'. */
+ static wrappedBitVector<isSigned> minValue(const Cvc5BitWidth& w);
+
+ /** Return true if this a bit-vector representing a ones value. */
+ Cvc5Prop isAllOnes() const;
+ /** Return true if this a bit-vector representing a zero value. */
+ Cvc5Prop isAllZeros() const;
+
+ /** Left shift. */
+ wrappedBitVector<isSigned> operator<<(
+ const wrappedBitVector<isSigned>& op) const;
+ /** Logical (unsigned) and arithmetic (signed) right shift. */
+ wrappedBitVector<isSigned> operator>>(
+ const wrappedBitVector<isSigned>& op) const;
+
+ /**
+ * Inherited but ...
+ * *sigh* if we use the inherited version then it will return a
+ * cvc5::BitVector which can be converted back to a
+ * wrappedBitVector<isSigned> but isn't done automatically when working
+ * out types for templates instantiation. ITE is a particular
+ * problem as expressions and constants no longer derive the
+ * same type. There aren't any good solutions in C++, we could
+ * use CRTP but Liana wouldn't appreciate that, so the following
+ * pointless wrapping functions are needed.
+ */
+
+ /** Bit-wise or. */
+ wrappedBitVector<isSigned> operator|(
+ const wrappedBitVector<isSigned>& op) const;
+ /** Bit-wise and. */
+ wrappedBitVector<isSigned> operator&(
+ const wrappedBitVector<isSigned>& op) const;
+ /** Bit-vector addition. */
+ wrappedBitVector<isSigned> operator+(
+ const wrappedBitVector<isSigned>& op) const;
+ /** Bit-vector subtraction. */
+ wrappedBitVector<isSigned> operator-(
+ const wrappedBitVector<isSigned>& op) const;
+ /** Bit-vector multiplication. */
+ wrappedBitVector<isSigned> operator*(
+ const wrappedBitVector<isSigned>& op) const;
+ /** Bit-vector signed/unsigned division. */
+ wrappedBitVector<isSigned> operator/(
+ const wrappedBitVector<isSigned>& op) const;
+ /** Bit-vector signed/unsigned remainder. */
+ wrappedBitVector<isSigned> operator%(
+ const wrappedBitVector<isSigned>& op) const;
+ /** Bit-vector negation. */
+ wrappedBitVector<isSigned> operator-(void) const;
+ /** Bit-wise not. */
+ wrappedBitVector<isSigned> operator~(void) const;
+
+ /** Bit-vector increment. */
+ wrappedBitVector<isSigned> increment() const;
+ /** Bit-vector decrement. */
+ wrappedBitVector<isSigned> decrement() const;
+ /**
+ * Bit-vector logical/arithmetic right shift where 'op' extended to the
+ * bit-width of this wrapped bit-vector.
+ */
+ wrappedBitVector<isSigned> signExtendRightShift(
+ const wrappedBitVector<isSigned>& op) const;
+
+ /**
+ * Modular operations.
+ * Note: No overflow checking so these are the same as other operations.
+ */
+ wrappedBitVector<isSigned> modularLeftShift(
+ const wrappedBitVector<isSigned>& op) const;
+ wrappedBitVector<isSigned> modularRightShift(
+ const wrappedBitVector<isSigned>& op) const;
+ wrappedBitVector<isSigned> modularIncrement() const;
+ wrappedBitVector<isSigned> modularDecrement() const;
+ wrappedBitVector<isSigned> modularAdd(
+ const wrappedBitVector<isSigned>& op) const;
+ wrappedBitVector<isSigned> modularNegate() const;
+
+ /** Bit-vector equality. */
+ Cvc5Prop operator==(const wrappedBitVector<isSigned>& op) const;
+ /** Bit-vector signed/unsigned less or equal than. */
+ Cvc5Prop operator<=(const wrappedBitVector<isSigned>& op) const;
+ /** Bit-vector sign/unsigned greater or equal than. */
+ Cvc5Prop operator>=(const wrappedBitVector<isSigned>& op) const;
+ /** Bit-vector signed/unsigned less than. */
+ Cvc5Prop operator<(const wrappedBitVector<isSigned>& op) const;
+ /** Bit-vector sign/unsigned greater or equal than. */
+ Cvc5Prop operator>(const wrappedBitVector<isSigned>& op) const;
+
+ /** Convert this bit-vector to a signed bit-vector. */
+ wrappedBitVector<true> toSigned(void) const;
+ /** Convert this bit-vector to an unsigned bit-vector. */
+ wrappedBitVector<false> toUnsigned(void) const;
+
+ /** Bit-vector signed/unsigned (zero) extension. */
+ wrappedBitVector<isSigned> extend(Cvc5BitWidth extension) const;
+
+ /**
+ * Create a "contracted" bit-vector by cutting off the 'reduction' number of
+ * most significant bits, i.e., by extracting the (bit-width - reduction)
+ * least significant bits.
+ */
+ wrappedBitVector<isSigned> contract(Cvc5BitWidth reduction) const;
+
+ /**
+ * Create a "resized" bit-vector of given size bei either extending (if new
+ * size is larger) or contracting (if it is smaller) this wrapped bit-vector.
+ */
+ wrappedBitVector<isSigned> resize(Cvc5BitWidth newSize) const;
+
+ /**
+ * Create an extension of this bit-vector that matches the bit-width of the
+ * given bit-vector.
+ *
+ * Note: The size of the given bit-vector may not be larger than the size of
+ * this bit-vector.
+ */
+ wrappedBitVector<isSigned> matchWidth(
+ const wrappedBitVector<isSigned>& op) const;
+
+ /** Bit-vector concatenation. */
+ wrappedBitVector<isSigned> append(const wrappedBitVector<isSigned>& op) const;
+
+ /** Inclusive of end points, thus if the same, extracts just one bit. */
+ wrappedBitVector<isSigned> extract(Cvc5BitWidth upper,
+ Cvc5BitWidth lower) const;
+};
+} // namespace symfpuLiteral
+} // namespace cvc5
+
+#endif
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Aina Niemetz, Martin Brain, Andres Noetzli
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * SymFPU glue code for floating-point values.
- *
- * !!! This header is only to be included in floating-point literal headers !!!
- *
- * This is a symfpu literal "back-end". It allows the library to be used as
- * an arbitrary precision floating-point implementation. This is effectively
- * the glue between symfpu's notion of "signed bit-vector" and cvc5's
- * BitVector.
- */
-
-#include "cvc5_private.h"
-
-#ifndef CVC5__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_TRAITS_H
-#define CVC5__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_TRAITS_H
-
-// clang-format off
-#if @CVC5_USE_SYMFPU@
-// clang-format on
-
-#include "util/bitvector.h"
-#include "util/floatingpoint_size.h"
-#include "util/roundingmode.h"
-
-#include <symfpu/core/unpackedFloat.h>
-
-/* -------------------------------------------------------------------------- */
-
-namespace cvc5 {
-namespace symfpuLiteral {
-
-/**
- * Forward declaration of wrapper so that traits can be defined early and so
- * used in the implementation of wrappedBitVector.
- */
-template <bool T>
-class wrappedBitVector;
-
-using Cvc5BitWidth = uint32_t;
-using Cvc5Prop = bool;
-using Cvc5RM = ::cvc5::RoundingMode;
-using Cvc5FPSize = ::cvc5::FloatingPointSize;
-using Cvc5UnsignedBitVector = wrappedBitVector<false>;
-using Cvc5SignedBitVector = wrappedBitVector<true>;
-
-/**
- * This is the template parameter for symfpu's templates.
- */
-class traits
-{
- public:
- /** The six key types that symfpu uses. */
- using bwt = Cvc5BitWidth; // bit-width type
- using prop = Cvc5Prop; // boolean type
- using rm = Cvc5RM; // rounding-mode type
- using fpt = Cvc5FPSize; // floating-point format type
- using ubv = Cvc5UnsignedBitVector; // unsigned bit-vector type
- using sbv = Cvc5SignedBitVector; // signed bit-vector type
-
- /** Give concrete instances of each rounding mode, mainly for comparisons. */
- static rm RNE(void);
- static rm RNA(void);
- static rm RTP(void);
- static rm RTN(void);
- static rm RTZ(void);
-
- /** The sympfu properties. */
- static void precondition(const prop& p);
- static void postcondition(const prop& p);
- static void invariant(const prop& p);
-};
-
-/**
- * Type function for mapping between types.
- */
-template <bool T>
-struct signedToLiteralType;
-
-template <>
-struct signedToLiteralType<true>
-{
- using literalType = int32_t;
-};
-template <>
-struct signedToLiteralType<false>
-{
- using literalType = uint32_t;
-};
-
-/**
- * This extends the interface for cvc5::BitVector for compatibility with symFPU.
- * The template parameter distinguishes signed and unsigned bit-vectors, a
- * distinction symfpu uses.
- */
-template <bool isSigned>
-class wrappedBitVector : public BitVector
-{
- protected:
- using literalType = typename signedToLiteralType<isSigned>::literalType;
- friend wrappedBitVector<!isSigned>; // To allow conversion between types
-
- friend ::symfpu::ite<Cvc5Prop, wrappedBitVector<isSigned> >; // For ITE
-
- public:
- /** Constructors. */
- wrappedBitVector(const Cvc5BitWidth w, const uint32_t v) : BitVector(w, v) {}
- wrappedBitVector(const Cvc5Prop& p) : BitVector(1, p ? 1U : 0U) {}
- wrappedBitVector(const wrappedBitVector<isSigned>& old) : BitVector(old) {}
- wrappedBitVector(const BitVector& old) : BitVector(old) {}
-
- /** Get the bit-width of this wrapped bit-vector. */
- Cvc5BitWidth getWidth(void) const { return getSize(); }
-
- /** Create a zero value of given bit-width 'w'. */
- static wrappedBitVector<isSigned> one(const Cvc5BitWidth& w);
- /** Create a one value of given bit-width 'w'. */
- static wrappedBitVector<isSigned> zero(const Cvc5BitWidth& w);
- /** Create a ones value (all bits 1) of given bit-width 'w'. */
- static wrappedBitVector<isSigned> allOnes(const Cvc5BitWidth& w);
- /** Create a maximum signed/unsigned value of given bit-width 'w'. */
- static wrappedBitVector<isSigned> maxValue(const Cvc5BitWidth& w);
- /** Create a minimum signed/unsigned value of given bit-width 'w'. */
- static wrappedBitVector<isSigned> minValue(const Cvc5BitWidth& w);
-
- /** Return true if this a bit-vector representing a ones value. */
- Cvc5Prop isAllOnes() const;
- /** Return true if this a bit-vector representing a zero value. */
- Cvc5Prop isAllZeros() const;
-
- /** Left shift. */
- wrappedBitVector<isSigned> operator<<(
- const wrappedBitVector<isSigned>& op) const;
- /** Logical (unsigned) and arithmetic (signed) right shift. */
- wrappedBitVector<isSigned> operator>>(
- const wrappedBitVector<isSigned>& op) const;
-
- /**
- * Inherited but ...
- * *sigh* if we use the inherited version then it will return a
- * cvc5::BitVector which can be converted back to a
- * wrappedBitVector<isSigned> but isn't done automatically when working
- * out types for templates instantiation. ITE is a particular
- * problem as expressions and constants no longer derive the
- * same type. There aren't any good solutions in C++, we could
- * use CRTP but Liana wouldn't appreciate that, so the following
- * pointless wrapping functions are needed.
- */
-
- /** Bit-wise or. */
- wrappedBitVector<isSigned> operator|(
- const wrappedBitVector<isSigned>& op) const;
- /** Bit-wise and. */
- wrappedBitVector<isSigned> operator&(
- const wrappedBitVector<isSigned>& op) const;
- /** Bit-vector addition. */
- wrappedBitVector<isSigned> operator+(
- const wrappedBitVector<isSigned>& op) const;
- /** Bit-vector subtraction. */
- wrappedBitVector<isSigned> operator-(
- const wrappedBitVector<isSigned>& op) const;
- /** Bit-vector multiplication. */
- wrappedBitVector<isSigned> operator*(
- const wrappedBitVector<isSigned>& op) const;
- /** Bit-vector signed/unsigned division. */
- wrappedBitVector<isSigned> operator/(
- const wrappedBitVector<isSigned>& op) const;
- /** Bit-vector signed/unsigned remainder. */
- wrappedBitVector<isSigned> operator%(
- const wrappedBitVector<isSigned>& op) const;
- /** Bit-vector negation. */
- wrappedBitVector<isSigned> operator-(void) const;
- /** Bit-wise not. */
- wrappedBitVector<isSigned> operator~(void) const;
-
- /** Bit-vector increment. */
- wrappedBitVector<isSigned> increment() const;
- /** Bit-vector decrement. */
- wrappedBitVector<isSigned> decrement() const;
- /**
- * Bit-vector logical/arithmetic right shift where 'op' extended to the
- * bit-width of this wrapped bit-vector.
- */
- wrappedBitVector<isSigned> signExtendRightShift(
- const wrappedBitVector<isSigned>& op) const;
-
- /**
- * Modular operations.
- * Note: No overflow checking so these are the same as other operations.
- */
- wrappedBitVector<isSigned> modularLeftShift(
- const wrappedBitVector<isSigned>& op) const;
- wrappedBitVector<isSigned> modularRightShift(
- const wrappedBitVector<isSigned>& op) const;
- wrappedBitVector<isSigned> modularIncrement() const;
- wrappedBitVector<isSigned> modularDecrement() const;
- wrappedBitVector<isSigned> modularAdd(
- const wrappedBitVector<isSigned>& op) const;
- wrappedBitVector<isSigned> modularNegate() const;
-
- /** Bit-vector equality. */
- Cvc5Prop operator==(const wrappedBitVector<isSigned>& op) const;
- /** Bit-vector signed/unsigned less or equal than. */
- Cvc5Prop operator<=(const wrappedBitVector<isSigned>& op) const;
- /** Bit-vector sign/unsigned greater or equal than. */
- Cvc5Prop operator>=(const wrappedBitVector<isSigned>& op) const;
- /** Bit-vector signed/unsigned less than. */
- Cvc5Prop operator<(const wrappedBitVector<isSigned>& op) const;
- /** Bit-vector sign/unsigned greater or equal than. */
- Cvc5Prop operator>(const wrappedBitVector<isSigned>& op) const;
-
- /** Convert this bit-vector to a signed bit-vector. */
- wrappedBitVector<true> toSigned(void) const;
- /** Convert this bit-vector to an unsigned bit-vector. */
- wrappedBitVector<false> toUnsigned(void) const;
-
- /** Bit-vector signed/unsigned (zero) extension. */
- wrappedBitVector<isSigned> extend(Cvc5BitWidth extension) const;
-
- /**
- * Create a "contracted" bit-vector by cutting off the 'reduction' number of
- * most significant bits, i.e., by extracting the (bit-width - reduction)
- * least significant bits.
- */
- wrappedBitVector<isSigned> contract(Cvc5BitWidth reduction) const;
-
- /**
- * Create a "resized" bit-vector of given size bei either extending (if new
- * size is larger) or contracting (if it is smaller) this wrapped bit-vector.
- */
- wrappedBitVector<isSigned> resize(Cvc5BitWidth newSize) const;
-
- /**
- * Create an extension of this bit-vector that matches the bit-width of the
- * given bit-vector.
- *
- * Note: The size of the given bit-vector may not be larger than the size of
- * this bit-vector.
- */
- wrappedBitVector<isSigned> matchWidth(
- const wrappedBitVector<isSigned>& op) const;
-
- /** Bit-vector concatenation. */
- wrappedBitVector<isSigned> append(const wrappedBitVector<isSigned>& op) const;
-
- /** Inclusive of end points, thus if the same, extracts just one bit. */
- wrappedBitVector<isSigned> extract(Cvc5BitWidth upper,
- Cvc5BitWidth lower) const;
-};
-} // namespace symfpuLiteral
-}
-
-#endif
-#endif
int main()
{
-#ifdef CVC5_USE_SYMFPU
Solver slv;
Sort sort_int = slv.getIntegerSort();
Sort sort_array = slv.mkArraySort(sort_int, sort_int);
Term rem = slv.mkTerm(FLOATINGPOINT_REM, ite, const1);
Term isnan = slv.mkTerm(FLOATINGPOINT_ISNAN, rem);
slv.checkSatAssuming(isnan);
-#endif
return 0;
}
def test_supports_floating_point(solver):
- if solver.supportsFloatingPoint():
- solver.mkRoundingMode(pycvc5.RoundNearestTiesToEven)
- else:
- with pytest.raises(RuntimeError):
- solver.mkRoundingMode(pycvc5.RoundNearestTiesToEven)
+ solver.mkRoundingMode(pycvc5.RoundNearestTiesToEven)
def test_get_boolean_sort(solver):
def test_get_rounding_mode_sort(solver):
- if solver.supportsFloatingPoint():
- solver.getRoundingModeSort()
- else:
- with pytest.raises(RuntimeError):
- solver.getRoundingModeSort()
+ solver.getRoundingModeSort()
def test_mk_array_sort(solver):
solver.mkArraySort(boolSort, intSort)
solver.mkArraySort(realSort, bvSort)
- if (solver.supportsFloatingPoint()):
- fpSort = solver.mkFloatingPointSort(3, 5)
- solver.mkArraySort(fpSort, fpSort)
- solver.mkArraySort(bvSort, fpSort)
+ fpSort = solver.mkFloatingPointSort(3, 5)
+ solver.mkArraySort(fpSort, fpSort)
+ solver.mkArraySort(bvSort, fpSort)
slv = pycvc5.Solver()
with pytest.raises(RuntimeError):
def test_mk_floating_point_sort(solver):
- if solver.supportsFloatingPoint():
- solver.mkFloatingPointSort(4, 8)
- with pytest.raises(RuntimeError):
- solver.mkFloatingPointSort(0, 8)
- with pytest.raises(RuntimeError):
- solver.mkFloatingPointSort(4, 0)
- else:
- with pytest.raises(RuntimeError):
- solver.mkFloatingPointSort(4, 8)
+ solver.mkFloatingPointSort(4, 8)
+ with pytest.raises(RuntimeError):
+ solver.mkFloatingPointSort(0, 8)
+ with pytest.raises(RuntimeError):
+ solver.mkFloatingPointSort(4, 0)
def test_mk_datatype_sort(solver):
def test_mk_rounding_mode(solver):
- if solver.supportsFloatingPoint():
- solver.mkRoundingMode(pycvc5.RoundTowardZero)
- else:
- with pytest.raises(RuntimeError):
- solver.mkRoundingMode(pycvc5.RoundTowardZero)
+ solver.mkRoundingMode(pycvc5.RoundTowardZero)
def test_mk_uninterpreted_const(solver):
t1 = solver.mkBitVector(8)
t2 = solver.mkBitVector(4)
t3 = solver.mkInteger(2)
- if (solver.supportsFloatingPoint()):
- solver.mkFloatingPoint(3, 5, t1)
- else:
- with pytest.raises(RuntimeError):
- solver.mkFloatingPoint(3, 5, t1)
+ solver.mkFloatingPoint(3, 5, t1)
with pytest.raises(RuntimeError):
solver.mkFloatingPoint(0, 5, pycvc5.Term(solver))
with pytest.raises(RuntimeError):
solver.mkFloatingPoint(3, 5, t2)
- if (solver.supportsFloatingPoint()):
- slv = pycvc5.Solver()
- with pytest.raises(RuntimeError):
- slv.mkFloatingPoint(3, 5, t1)
+ slv = pycvc5.Solver()
+ with pytest.raises(RuntimeError):
+ slv.mkFloatingPoint(3, 5, t1)
def test_mk_empty_set(solver):
def test_mk_nan(solver):
- if (solver.supportsFloatingPoint()):
- solver.mkNaN(3, 5)
- else:
- with pytest.raises(RuntimeError):
- solver.mkNaN(3, 5)
+ solver.mkNaN(3, 5)
def test_mk_neg_zero(solver):
- if (solver.supportsFloatingPoint()):
- solver.mkNegZero(3, 5)
- else:
- with pytest.raises(RuntimeError):
- solver.mkNegZero(3, 5)
+ solver.mkNegZero(3, 5)
def test_mk_neg_inf(solver):
- if (solver.supportsFloatingPoint()):
- solver.mkNegInf(3, 5)
- else:
- with pytest.raises(RuntimeError):
- solver.mkNegInf(3, 5)
+ solver.mkNegInf(3, 5)
def test_mk_pos_inf(solver):
- if (solver.supportsFloatingPoint()):
- solver.mkPosInf(3, 5)
- else:
- with pytest.raises(RuntimeError):
- solver.mkPosInf(3, 5)
+ solver.mkPosInf(3, 5)
def test_mk_pos_zero(solver):
- if (solver.supportsFloatingPoint()):
- solver.mkPosZero(3, 5)
- else:
- with pytest.raises(RuntimeError):
- solver.mkPosZero(3, 5)
+ solver.mkPosZero(3, 5)
def test_mk_pi(solver):
def test_is_rounding_mode(solver):
- if solver.supportsFloatingPoint():
- assert solver.getRoundingModeSort().isRoundingMode()
- Sort(solver).isRoundingMode()
+ assert solver.getRoundingModeSort().isRoundingMode()
+ Sort(solver).isRoundingMode()
def test_is_bit_vector(solver):
def test_is_floating_point(solver):
- if solver.supportsFloatingPoint():
- assert solver.mkFloatingPointSort(8, 24).isFloatingPoint()
- Sort(solver).isFloatingPoint()
+ assert solver.mkFloatingPointSort(8, 24).isFloatingPoint()
+ Sort(solver).isFloatingPoint()
def test_is_datatype(solver):
def test_get_fp_exponent_size(solver):
- if solver.supportsFloatingPoint():
- fpSort = solver.mkFloatingPointSort(4, 8)
- fpSort.getFPExponentSize()
- setSort = solver.mkSetSort(solver.getIntegerSort())
- with pytest.raises(RuntimeError):
- setSort.getFPExponentSize()
+ fpSort = solver.mkFloatingPointSort(4, 8)
+ fpSort.getFPExponentSize()
+ setSort = solver.mkSetSort(solver.getIntegerSort())
+ with pytest.raises(RuntimeError):
+ setSort.getFPExponentSize()
def test_get_fp_significand_size(solver):
- if solver.supportsFloatingPoint():
- fpSort = solver.mkFloatingPointSort(4, 8)
- fpSort.getFPSignificandSize()
- setSort = solver.mkSetSort(solver.getIntegerSort())
- with pytest.raises(RuntimeError):
- setSort.getFPSignificandSize()
+ fpSort = solver.mkFloatingPointSort(4, 8)
+ fpSort.getFPSignificandSize()
+ setSort = solver.mkSetSort(solver.getIntegerSort())
+ with pytest.raises(RuntimeError):
+ setSort.getFPSignificandSize()
def test_get_datatype_paramsorts(solver):
a given benchmark when a feature is supported. For example:
```
-; REQUIRES: symfpu
+; REQUIRES: cryptominisat
```
-This benchmark is only run when symfpu has been configured. Multiple
+This benchmark is only run when CryptoMiniSat has been configured. Multiple
`REQUIRES` directives are supported. For a list of features that can be listed
as a requirement, refer to cvc5's `--show-config` output. Features can also be
-excluded by adding the `no-` prefix, e.g. `no-symfpu` means that the test is
-not valid for builds that include symfpu support.
+excluded by adding the `no-` prefix, e.g. `no-cryptominisat` means that the
+test is not valid for builds that include CryptoMiniSat support.
-; REQUIRES: symfpu
; COMMAND-LINE: --fp-exp
; EXPECT: sat
(set-logic QF_FP)
-; REQUIRES: symfpu
; COMMAND-LINE: --fp-exp
; EXPECT: unsat
(set-logic QF_FP)
-; REQUIRES: symfpu
; COMMAND-LINE: --fp-exp
; EXPECT: unsat
-; REQUIRES: symfpu
; COMMAND-LINE: --ext-rew-prep --ext-rew-prep-agg
; EXPECT: unsat
(set-info :smt-lib-version 2.6)
-; REQUIRES: symfpu
; COMMAND-LINE: --fp-exp
; EXPECT: unsat
(set-logic QF_BVFP)
-; REQUIRES: symfpu
; EXPECT: unsat
(set-logic QF_FP)
(declare-const r RoundingMode)
-; REQUIRES: symfpu
; EXPECT: unsat
(set-logic QF_FP)
(declare-fun fpv5 () Float32)
-; REQUIRES: symfpu
; COMMAND-LINE: -q
; EXPECT: sat
(set-logic QF_FP)
-; REQUIRES: symfpu
; EXPECT: unsat
(set-logic QF_FP)
(declare-fun bv () (_ BitVec 1))
-; REQUIRES: symfpu
; COMMAND-LINE: -q
; EXPECT: sat
(set-logic QF_FPLRA)
; COMMAND-LINE: -q
; EXPECT: sat
-; REQUIRES: symfpu
(set-logic HO_ALL)
(set-option :assign-function-values false)
(set-info :status sat)
-; REQUIRES: symfpu
; EXPECT: sat
(set-logic QF_FP)
(declare-fun a () (_ FloatingPoint 53 11))
-; REQUIRES: symfpu
; EXPECT: sat
(set-logic QF_FP)
(declare-fun a () RoundingMode)
-; REQUIRES: symfpu
; EXPECT: sat
; EXPECT: ((((_ to_fp 5 11) roundNearestTiesToAway (/ 1 10)) (fp #b0 #b01011 #b1001100110)))
(set-logic ALL)
-; REQUIRES: symfpu\r
; COMMAND-LINE: --fp-exp\r
; EXPECT: unsat\r
\r
-; REQUIRES: symfpu
; EXPECT: unsat
(set-logic QF_FP)
(declare-const x Float32)
-; REQUIRES: symfpu
; COMMAND-LINE: --fp-exp
; EXPECT: sat
; COMMAND-LINE: --bv-to-bool
-; REQUIRES: symfpu
(set-logic ALL)
(set-info :status sat)
(declare-fun c () (Array (_ BitVec 2) (_ BitVec 1)))
-; REQUIRES: symfpu
; COMMAND-LINE: --strict-parsing -q
; EXPECT: sat
(set-logic QF_FP)
-; REQUIRES: symfpu
; COMMAND-LINE: --fp-exp
; EXPECT: unsat
-; REQUIRES: symfpu
(set-info :smt-lib-version 2.6)
(set-logic FP)
(set-info :status unsat)
; COMMAND-LINE: --no-jh-rlv-order
-; REQUIRES: symfpu
; EXPECT: unsat
(set-logic AUFBVFPDTNIRA)
(set-info :status unsat)
-; REQUIRES: symfpu
; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break --fp-exp
; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.")
; SCRUBBER: grep -v -E '(\(define-fun|\(rewrite)'
-; REQUIRES: symfpu
; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break --fp-exp
; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.")
; SCRUBBER: grep -v -E '(\(define-fun|\(rewrite)'
-; REQUIRES: symfpu
; EXPECT: unsat
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic ALL)
-; REQUIRES: symfpu
; COMMAND-LINE: --decision=internal -q
; COMMAND-LINE: --decision=justification -q
; EXPECT: sat
-; REQUIRES: symfpu
; EXPECT: unsat
; COMMAND-LINE: --lang=sygus2 --sygus-out=status --fp-exp
(set-logic ALL)
TEST_F(TestApiBlackSolver, supportsFloatingPoint)
{
- if (d_solver.supportsFloatingPoint())
- {
- ASSERT_NO_THROW(d_solver.mkRoundingMode(ROUND_NEAREST_TIES_TO_EVEN));
- }
- else
- {
- ASSERT_THROW(d_solver.mkRoundingMode(ROUND_NEAREST_TIES_TO_EVEN),
- CVC5ApiException);
- }
+ ASSERT_NO_THROW(d_solver.mkRoundingMode(ROUND_NEAREST_TIES_TO_EVEN));
}
TEST_F(TestApiBlackSolver, getBooleanSort)
TEST_F(TestApiBlackSolver, getRoundingModeSort)
{
- if (d_solver.supportsFloatingPoint())
- {
- ASSERT_NO_THROW(d_solver.getRoundingModeSort());
- }
- else
- {
- ASSERT_THROW(d_solver.getRoundingModeSort(), CVC5ApiException);
- }
+ ASSERT_NO_THROW(d_solver.getRoundingModeSort());
}
TEST_F(TestApiBlackSolver, mkArraySort)
ASSERT_NO_THROW(d_solver.mkArraySort(boolSort, intSort));
ASSERT_NO_THROW(d_solver.mkArraySort(realSort, bvSort));
- if (d_solver.supportsFloatingPoint())
- {
- Sort fpSort = d_solver.mkFloatingPointSort(3, 5);
- ASSERT_NO_THROW(d_solver.mkArraySort(fpSort, fpSort));
- ASSERT_NO_THROW(d_solver.mkArraySort(bvSort, fpSort));
- }
+ Sort fpSort = d_solver.mkFloatingPointSort(3, 5);
+ ASSERT_NO_THROW(d_solver.mkArraySort(fpSort, fpSort));
+ ASSERT_NO_THROW(d_solver.mkArraySort(bvSort, fpSort));
Solver slv;
ASSERT_THROW(slv.mkArraySort(boolSort, boolSort), CVC5ApiException);
TEST_F(TestApiBlackSolver, mkFloatingPointSort)
{
- if (d_solver.supportsFloatingPoint())
- {
- ASSERT_NO_THROW(d_solver.mkFloatingPointSort(4, 8));
- ASSERT_THROW(d_solver.mkFloatingPointSort(0, 8), CVC5ApiException);
- ASSERT_THROW(d_solver.mkFloatingPointSort(4, 0), CVC5ApiException);
- }
- else
- {
- ASSERT_THROW(d_solver.mkFloatingPointSort(4, 8), CVC5ApiException);
- }
+ ASSERT_NO_THROW(d_solver.mkFloatingPointSort(4, 8));
+ ASSERT_THROW(d_solver.mkFloatingPointSort(0, 8), CVC5ApiException);
+ ASSERT_THROW(d_solver.mkFloatingPointSort(4, 0), CVC5ApiException);
}
TEST_F(TestApiBlackSolver, mkDatatypeSort)
TEST_F(TestApiBlackSolver, mkRoundingMode)
{
- if (d_solver.supportsFloatingPoint())
- {
- ASSERT_NO_THROW(d_solver.mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO));
- }
- else
- {
- ASSERT_THROW(d_solver.mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO),
- CVC5ApiException);
- }
+ ASSERT_NO_THROW(d_solver.mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO));
}
TEST_F(TestApiBlackSolver, mkUninterpretedConst)
Term t1 = d_solver.mkBitVector(8);
Term t2 = d_solver.mkBitVector(4);
Term t3 = d_solver.mkInteger(2);
- if (d_solver.supportsFloatingPoint())
- {
- ASSERT_NO_THROW(d_solver.mkFloatingPoint(3, 5, t1));
- }
- else
- {
- ASSERT_THROW(d_solver.mkFloatingPoint(3, 5, t1), CVC5ApiException);
- }
+ ASSERT_NO_THROW(d_solver.mkFloatingPoint(3, 5, t1));
ASSERT_THROW(d_solver.mkFloatingPoint(0, 5, Term()), CVC5ApiException);
ASSERT_THROW(d_solver.mkFloatingPoint(0, 5, t1), CVC5ApiException);
ASSERT_THROW(d_solver.mkFloatingPoint(3, 0, t1), CVC5ApiException);
ASSERT_THROW(d_solver.mkFloatingPoint(3, 5, t2), CVC5ApiException);
ASSERT_THROW(d_solver.mkFloatingPoint(3, 5, t2), CVC5ApiException);
- if (d_solver.supportsFloatingPoint())
- {
- Solver slv;
- ASSERT_THROW(slv.mkFloatingPoint(3, 5, t1), CVC5ApiException);
- }
+ Solver slv;
+ ASSERT_THROW(slv.mkFloatingPoint(3, 5, t1), CVC5ApiException);
}
TEST_F(TestApiBlackSolver, mkEmptySet)
ASSERT_NO_THROW(d_solver.mkFalse());
}
-TEST_F(TestApiBlackSolver, mkNaN)
-{
- if (d_solver.supportsFloatingPoint())
- {
- ASSERT_NO_THROW(d_solver.mkNaN(3, 5));
- }
- else
- {
- ASSERT_THROW(d_solver.mkNaN(3, 5), CVC5ApiException);
- }
-}
+TEST_F(TestApiBlackSolver, mkNaN) { ASSERT_NO_THROW(d_solver.mkNaN(3, 5)); }
TEST_F(TestApiBlackSolver, mkNegZero)
{
- if (d_solver.supportsFloatingPoint())
- {
- ASSERT_NO_THROW(d_solver.mkNegZero(3, 5));
- }
- else
- {
- ASSERT_THROW(d_solver.mkNegZero(3, 5), CVC5ApiException);
- }
+ ASSERT_NO_THROW(d_solver.mkNegZero(3, 5));
}
TEST_F(TestApiBlackSolver, mkNegInf)
{
- if (d_solver.supportsFloatingPoint())
- {
- ASSERT_NO_THROW(d_solver.mkNegInf(3, 5));
- }
- else
- {
- ASSERT_THROW(d_solver.mkNegInf(3, 5), CVC5ApiException);
- }
+ ASSERT_NO_THROW(d_solver.mkNegInf(3, 5));
}
TEST_F(TestApiBlackSolver, mkPosInf)
{
- if (d_solver.supportsFloatingPoint())
- {
- ASSERT_NO_THROW(d_solver.mkPosInf(3, 5));
- }
- else
- {
- ASSERT_THROW(d_solver.mkPosInf(3, 5), CVC5ApiException);
- }
+ ASSERT_NO_THROW(d_solver.mkPosInf(3, 5));
}
TEST_F(TestApiBlackSolver, mkPosZero)
{
- if (d_solver.supportsFloatingPoint())
- {
- ASSERT_NO_THROW(d_solver.mkPosZero(3, 5));
- }
- else
- {
- ASSERT_THROW(d_solver.mkPosZero(3, 5), CVC5ApiException);
- }
+ ASSERT_NO_THROW(d_solver.mkPosZero(3, 5));
}
TEST_F(TestApiBlackSolver, mkOp)
TEST_F(TestApiBlackSort, isRoundingMode)
{
- if (d_solver.supportsFloatingPoint())
- {
- ASSERT_TRUE(d_solver.getRoundingModeSort().isRoundingMode());
- ASSERT_NO_THROW(Sort().isRoundingMode());
- }
+ ASSERT_TRUE(d_solver.getRoundingModeSort().isRoundingMode());
+ ASSERT_NO_THROW(Sort().isRoundingMode());
}
TEST_F(TestApiBlackSort, isBitVector)
TEST_F(TestApiBlackSort, isFloatingPoint)
{
- if (d_solver.supportsFloatingPoint())
- {
- ASSERT_TRUE(d_solver.mkFloatingPointSort(8, 24).isFloatingPoint());
- ASSERT_NO_THROW(Sort().isFloatingPoint());
- }
+ ASSERT_TRUE(d_solver.mkFloatingPointSort(8, 24).isFloatingPoint());
+ ASSERT_NO_THROW(Sort().isFloatingPoint());
}
TEST_F(TestApiBlackSort, isDatatype)
TEST_F(TestApiBlackSort, getFPExponentSize)
{
- if (d_solver.supportsFloatingPoint())
- {
- Sort fpSort = d_solver.mkFloatingPointSort(4, 8);
- ASSERT_NO_THROW(fpSort.getFPExponentSize());
- Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
- ASSERT_THROW(setSort.getFPExponentSize(), CVC5ApiException);
- }
+ Sort fpSort = d_solver.mkFloatingPointSort(4, 8);
+ ASSERT_NO_THROW(fpSort.getFPExponentSize());
+ Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
+ ASSERT_THROW(setSort.getFPExponentSize(), CVC5ApiException);
}
TEST_F(TestApiBlackSort, getFPSignificandSize)
{
- if (d_solver.supportsFloatingPoint())
- {
- Sort fpSort = d_solver.mkFloatingPointSort(4, 8);
- ASSERT_NO_THROW(fpSort.getFPSignificandSize());
- Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
- ASSERT_THROW(setSort.getFPSignificandSize(), CVC5ApiException);
- }
+ Sort fpSort = d_solver.mkFloatingPointSort(4, 8);
+ ASSERT_NO_THROW(fpSort.getFPSignificandSize());
+ Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
+ ASSERT_THROW(setSort.getFPSignificandSize(), CVC5ApiException);
}
TEST_F(TestApiBlackSort, getDatatypeParamSorts)
info.arithOnlyLinear();
info.disableIntegers();
info.lock();
- if (cvc5::Configuration::isBuiltWithSymFPU())
- {
- ASSERT_EQ(info.getLogicString(), "SEP_AUFBVFPDTLRA");
- }
- else
- {
- ASSERT_EQ(info.getLogicString(), "SEP_AUFBVDTLRA");
- }
+ ASSERT_EQ(info.getLogicString(), "SEP_AUFBVFPDTLRA");
info = info.getUnlockedCopy();
ASSERT_FALSE(info.isLocked());
info.disableQuantifiers();
info.disableTheory(THEORY_BAGS);
info.lock();
- if (cvc5::Configuration::isBuiltWithSymFPU())
- {
- ASSERT_EQ(info.getLogicString(), "QF_SEP_AUFBVFPDTLRA");
- }
- else
- {
- ASSERT_EQ(info.getLogicString(), "QF_SEP_AUFBVDTLRA");
- }
+ ASSERT_EQ(info.getLogicString(), "QF_SEP_AUFBVFPDTLRA");
info = info.getUnlockedCopy();
ASSERT_FALSE(info.isLocked());
info.enableIntegers();
info.disableReals();
info.lock();
- if (cvc5::Configuration::isBuiltWithSymFPU())
- {
- ASSERT_EQ(info.getLogicString(), "QF_SEP_AUFFPLIA");
- }
- else
- {
- ASSERT_EQ(info.getLogicString(), "QF_SEP_AUFLIA");
- }
+ ASSERT_EQ(info.getLogicString(), "QF_SEP_AUFFPLIA");
info = info.getUnlockedCopy();
ASSERT_FALSE(info.isLocked());
cvc5_add_unit_test_black(configuration_black util)
cvc5_add_unit_test_black(datatype_black util)
cvc5_add_unit_test_black(exception_black util)
-if(CVC5_USE_SYMFPU)
cvc5_add_unit_test_black(floatingpoint_black util)
-endif()
cvc5_add_unit_test_black(integer_black util)
cvc5_add_unit_test_white(integer_white util)
cvc5_add_unit_test_black(output_black util)
projects / cvc5.git / commitdiff