3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-16 15:46:20 +00:00

removing file to deal with build issue

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-01-13 09:15:14 -08:00
parent eca8e19231
commit 38d67b3c59

View file

@ -1,119 +0,0 @@
/**
\brief Example demonstrating the RCF (Real Closed Field) API in C++.
This example shows how to use RCF numerals to work with:
- Transcendental numbers (pi, e)
- Algebraic numbers (roots of polynomials)
- Infinitesimals
- Exact real arithmetic
*/
#include <iostream>
#include "z3++.h"
using namespace z3;
void rcf_basic_example() {
std::cout << "RCF Basic Example\n";
std::cout << "=================\n";
context c;
// Create pi and e
rcf_num pi = rcf_pi(c);
rcf_num e = rcf_e(c);
std::cout << "pi = " << pi << "\n";
std::cout << "e = " << e << "\n";
// Arithmetic operations
rcf_num sum = pi + e;
rcf_num prod = pi * e;
std::cout << "pi + e = " << sum << "\n";
std::cout << "pi * e = " << prod << "\n";
// Decimal approximations
std::cout << "pi (10 decimals) = " << pi.to_decimal(10) << "\n";
std::cout << "e (10 decimals) = " << e.to_decimal(10) << "\n";
// Comparisons
std::cout << "pi < e? " << (pi < e ? "yes" : "no") << "\n";
std::cout << "pi > e? " << (pi > e ? "yes" : "no") << "\n";
}
void rcf_rational_example() {
std::cout << "\nRCF Rational Example\n";
std::cout << "====================\n";
context c;
// Create rational numbers
rcf_num half(c, "1/2");
rcf_num third(c, "1/3");
std::cout << "1/2 = " << half << "\n";
std::cout << "1/3 = " << third << "\n";
// Arithmetic
rcf_num sum = half + third;
std::cout << "1/2 + 1/3 = " << sum << "\n";
// Type queries
std::cout << "Is 1/2 rational? " << (half.is_rational() ? "yes" : "no") << "\n";
std::cout << "Is 1/2 algebraic? " << (half.is_algebraic() ? "yes" : "no") << "\n";
}
void rcf_roots_example() {
std::cout << "\nRCF Roots Example\n";
std::cout << "=================\n";
context c;
// Find roots of x^2 - 2 = 0
// Polynomial: -2 + 0*x + 1*x^2
std::vector<rcf_num> coeffs;
coeffs.push_back(rcf_num(c, -2)); // constant term
coeffs.push_back(rcf_num(c, 0)); // x coefficient
coeffs.push_back(rcf_num(c, 1)); // x^2 coefficient
std::vector<rcf_num> roots = rcf_roots(c, coeffs);
std::cout << "Roots of x^2 - 2 = 0:\n";
for (size_t i = 0; i < roots.size(); i++) {
std::cout << " root[" << i << "] = " << roots[i] << "\n";
std::cout << " decimal = " << roots[i].to_decimal(15) << "\n";
std::cout << " is_algebraic = " << (roots[i].is_algebraic() ? "yes" : "no") << "\n";
}
}
void rcf_infinitesimal_example() {
std::cout << "\nRCF Infinitesimal Example\n";
std::cout << "=========================\n";
context c;
// Create an infinitesimal
rcf_num eps = rcf_infinitesimal(c);
std::cout << "eps = " << eps << "\n";
std::cout << "Is eps infinitesimal? " << (eps.is_infinitesimal() ? "yes" : "no") << "\n";
// Infinitesimals are smaller than any positive real number
rcf_num tiny(c, "1/1000000000");
std::cout << "eps < 1/1000000000? " << (eps < tiny ? "yes" : "no") << "\n";
}
int main() {
try {
rcf_basic_example();
rcf_rational_example();
rcf_roots_example();
rcf_infinitesimal_example();
std::cout << "\nAll RCF examples completed successfully!\n";
return 0;
}
catch (exception& e) {
std::cerr << "Z3 exception: " << e << "\n";
return 1;
}
}