mirror of
https://github.com/AdaCore/cvc5.git
synced 2026-02-12 12:32:16 -08:00
104 lines
4.0 KiB
C++
104 lines
4.0 KiB
C++
/******************************************************************************
|
|
* Top contributors (to current version):
|
|
* Mudathir Mohamed, Mathias Preiner, Andres Noetzli
|
|
*
|
|
* This file is part of the cvc5 project.
|
|
*
|
|
* Copyright (c) 2009-2022 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.
|
|
* ****************************************************************************
|
|
*
|
|
* An example of solving floating-point problems with cvc5's cpp API
|
|
*
|
|
* This example shows to create floating-point types, variables and expressions,
|
|
* and how to create rounding mode constants by solving toy problems. The
|
|
* example also shows making special values (such as NaN and +oo) and converting
|
|
* an IEEE 754-2008 bit-vector to a floating-point number.
|
|
*/
|
|
|
|
#include <cvc5/cvc5.h>
|
|
|
|
#include <iostream>
|
|
#include <cassert>
|
|
|
|
using namespace std;
|
|
using namespace cvc5;
|
|
|
|
int main()
|
|
{
|
|
Solver solver;
|
|
solver.setOption("produce-models", "true");
|
|
|
|
// Make single precision floating-point variables
|
|
Sort fpt32 = solver.mkFloatingPointSort(8, 24);
|
|
Term a = solver.mkConst(fpt32, "a");
|
|
Term b = solver.mkConst(fpt32, "b");
|
|
Term c = solver.mkConst(fpt32, "c");
|
|
Term d = solver.mkConst(fpt32, "d");
|
|
Term e = solver.mkConst(fpt32, "e");
|
|
|
|
// Assert that floating-point addition is not associative:
|
|
// (a + (b + c)) != ((a + b) + c)
|
|
Term rm = solver.mkRoundingMode(ROUND_NEAREST_TIES_TO_EVEN);
|
|
Term lhs = solver.mkTerm(
|
|
FLOATINGPOINT_ADD, {rm, a, solver.mkTerm(FLOATINGPOINT_ADD, {rm, b, c})});
|
|
Term rhs = solver.mkTerm(
|
|
FLOATINGPOINT_ADD, {rm, solver.mkTerm(FLOATINGPOINT_ADD, {rm, a, b}), c});
|
|
solver.assertFormula(solver.mkTerm(NOT, {solver.mkTerm(EQUAL, {a, b})}));
|
|
|
|
Result r = solver.checkSat(); // result is sat
|
|
assert (r.isSat());
|
|
|
|
cout << "a = " << solver.getValue(a) << endl;
|
|
cout << "b = " << solver.getValue(b) << endl;
|
|
cout << "c = " << solver.getValue(c) << endl;
|
|
|
|
// Now, let's restrict `a` to be either NaN or positive infinity
|
|
Term nan = solver.mkFloatingPointNaN(8, 24);
|
|
Term inf = solver.mkFloatingPointPosInf(8, 24);
|
|
solver.assertFormula(solver.mkTerm(
|
|
OR, {solver.mkTerm(EQUAL, {a, inf}), solver.mkTerm(EQUAL, {a, nan})}));
|
|
|
|
r = solver.checkSat(); // result is sat
|
|
assert (r.isSat());
|
|
|
|
cout << "a = " << solver.getValue(a) << endl;
|
|
cout << "b = " << solver.getValue(b) << endl;
|
|
cout << "c = " << solver.getValue(c) << endl;
|
|
|
|
// And now for something completely different. Let's try to find a (normal)
|
|
// floating-point number that rounds to different integer values for
|
|
// different rounding modes.
|
|
Term rtp = solver.mkRoundingMode(ROUND_TOWARD_POSITIVE);
|
|
Term rtn = solver.mkRoundingMode(ROUND_TOWARD_NEGATIVE);
|
|
Op op = solver.mkOp(FLOATINGPOINT_TO_SBV, {16}); // (_ fp.to_sbv 16)
|
|
lhs = solver.mkTerm(op, {rtp, d});
|
|
rhs = solver.mkTerm(op, {rtn, d});
|
|
solver.assertFormula(solver.mkTerm(FLOATINGPOINT_IS_NORMAL, {d}));
|
|
solver.assertFormula(solver.mkTerm(NOT, {solver.mkTerm(EQUAL, {lhs, rhs})}));
|
|
|
|
r = solver.checkSat(); // result is sat
|
|
assert (r.isSat());
|
|
|
|
// Convert the result to a rational and print it
|
|
Term val = solver.getValue(d);
|
|
Term realVal = solver.getValue(solver.mkTerm(FLOATINGPOINT_TO_REAL, {val}));
|
|
cout << "d = " << val << " = " << realVal << endl;
|
|
cout << "((_ fp.to_sbv 16) RTP d) = " << solver.getValue(lhs) << endl;
|
|
cout << "((_ fp.to_sbv 16) RTN d) = " << solver.getValue(rhs) << endl;
|
|
|
|
// For our final trick, let's try to find a floating-point number between
|
|
// positive zero and the smallest positive floating-point number
|
|
Term zero = solver.mkFloatingPointPosZero(8, 24);
|
|
Term smallest = solver.mkFloatingPoint(8, 24, solver.mkBitVector(32, 0b001));
|
|
solver.assertFormula(
|
|
solver.mkTerm(AND,
|
|
{solver.mkTerm(FLOATINGPOINT_LT, {zero, e}),
|
|
solver.mkTerm(FLOATINGPOINT_LT, {e, smallest})}));
|
|
|
|
r = solver.checkSat(); // result is unsat
|
|
assert (!r.isSat());
|
|
}
|