mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-24 02:54:00 +00:00
Code Activity

remove RCF example

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-01-14 17:07:25 -08:00
parent 1d8c50ebd6
commit a2605e7b66
1 changed files with 0 additions and 133 deletions
Download patch file Download diff file Expand all files Collapse all files

133
examples/dotnet/RCFExample.cs
View file

@ -1,133 +0,0 @@
/**
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
*/
using Microsoft.Z3;
using System;
class RCFExample
{
static void RcfBasicExample()
{
Console.WriteLine("RCF Basic Example");
Console.WriteLine("=================");
using (Context ctx = new Context())
{
// Create pi and e
RCFNum pi = RCFNum.MkPi(ctx);
RCFNum e = RCFNum.MkE(ctx);
Console.WriteLine("pi = " + pi);
Console.WriteLine("e = " + e);
// Arithmetic operations
RCFNum sum = pi + e;
RCFNum prod = pi * e;
Console.WriteLine("pi + e = " + sum);
Console.WriteLine("pi * e = " + prod);
// Decimal approximations
Console.WriteLine("pi (10 decimals) = " + pi.ToDecimal(10));
Console.WriteLine("e (10 decimals) = " + e.ToDecimal(10));
// Comparisons
Console.WriteLine("pi < e? " + (pi < e ? "yes" : "no"));
Console.WriteLine("pi > e? " + (pi > e ? "yes" : "no"));
}
}
static void RcfRationalExample()
{
Console.WriteLine("\nRCF Rational Example");
Console.WriteLine("====================");
using (Context ctx = new Context())
{
// Create rational numbers
RCFNum half = new RCFNum(ctx, "1/2");
RCFNum third = new RCFNum(ctx, "1/3");
Console.WriteLine("1/2 = " + half);
Console.WriteLine("1/3 = " + third);
// Arithmetic
RCFNum sum = half + third;
Console.WriteLine("1/2 + 1/3 = " + sum);
// Type queries
Console.WriteLine("Is 1/2 rational? " + (half.IsRational() ? "yes" : "no"));
Console.WriteLine("Is 1/2 algebraic? " + (half.IsAlgebraic() ? "yes" : "no"));
}
}
static void RcfRootsExample()
{
Console.WriteLine("\nRCF Roots Example");
Console.WriteLine("=================");
using (Context ctx = new Context())
{
// Find roots of x^2 - 2 = 0
// Polynomial: -2 + 0*x + 1*x^2
RCFNum[] coeffs = new RCFNum[] {
new RCFNum(ctx, -2), // constant term
new RCFNum(ctx, 0), // x coefficient
new RCFNum(ctx, 1) // x^2 coefficient
};
RCFNum[] roots = RCFNum.MkRoots(ctx, coeffs);
Console.WriteLine("Roots of x^2 - 2 = 0:");
for (int i = 0; i < roots.Length; i++)
{
Console.WriteLine(" root[" + i + "] = " + roots[i]);
Console.WriteLine(" decimal = " + roots[i].ToDecimal(15));
Console.WriteLine(" is_algebraic = " + (roots[i].IsAlgebraic() ? "yes" : "no"));
}
}
}
static void RcfInfinitesimalExample()
{
Console.WriteLine("\nRCF Infinitesimal Example");
Console.WriteLine("=========================");
using (Context ctx = new Context())
{
// Create an infinitesimal
RCFNum eps = RCFNum.MkInfinitesimal(ctx);
Console.WriteLine("eps = " + eps);
Console.WriteLine("Is eps infinitesimal? " + (eps.IsInfinitesimal() ? "yes" : "no"));
// Infinitesimals are smaller than any positive real number
RCFNum tiny = new RCFNum(ctx, "1/1000000000");
Console.WriteLine("eps < 1/1000000000? " + (eps < tiny ? "yes" : "no"));
}
}
static void Main(string[] args)
{
try
{
RcfBasicExample();
RcfRationalExample();
RcfRootsExample();
RcfInfinitesimalExample();
Console.WriteLine("\nAll RCF examples completed successfully!");
}
catch (Exception ex)
{
Console.Error.WriteLine("Error: " + ex.Message);
Console.Error.WriteLine(ex.StackTrace);
}
}
}