Source

z3 / src / test / mpbq.cpp

/*++
Copyright (c) 2012 Microsoft Corporation

Module Name:

    mpbq.cpp

Abstract:

    mpbq tests...

Author:

    Leonardo de Moura (leonardo) 2012-09-20

Revision History:

--*/
#include "mpbq.h"

static void tst1() {
    unsynch_mpz_manager zm;
    mpbq_manager m(zm);
    scoped_mpbq  a(m), b(m);
    m.set(a, INT_MAX);
    a = a + 1;
    a = a * a;
    a = a*3 - 1;
    a = a * a - 5;
    a = a * a - 7;
    m.div2k(a, 67);
    std::cout << a << "\n";
    b = a;
    m.approx(b, 32, true);
    std::cout << b << "\n";
    b = a;
    m.approx(b, 32, false);
    std::cout << b << "\n";
    b = a; m.neg(b);
    m.approx(b, 32, true);
    std::cout << b << "\n";
    b = a; m.neg(b);
    m.approx(b, 32, false);
    std::cout << b << "\n";
}

static void tst2() {
   unsynch_mpz_manager zm;
   mpbq_manager m(zm);
   scoped_mpbq  a(m), b(m);
   m.set(a, 5);
   m.set(b, 3);
   m.approx_div(a, b, a, 128);
   std::cout << a << "\n";
 }

void tst_mpbq() {
    tst1();
    tst2();
}
Tip: Filter by directory path e.g. /media app.js to search for public/media/app.js.
Tip: Use camelCasing e.g. ProjME to search for ProjectModifiedEvent.java.
Tip: Filter by extension type e.g. /repo .js to search for all .js files in the /repo directory.
Tip: Separate your search with spaces e.g. /ssh pom.xml to search for src/ssh/pom.xml.
Tip: Use ↑ and ↓ arrow keys to navigate and return to view the file.
Tip: You can also navigate files with Ctrl+j (next) and Ctrl+k (previous) and view the file with Ctrl+o.
Tip: You can also navigate files with Alt+j (next) and Alt+k (previous) and view the file with Alt+o.