<commit_before>/*++
Copyright (c) 2013 Microsoft Corporation

Module Name:

    api_rcf.cpp

Abstract:

    Additional APIs for handling elements of the Z3 real closed field that contains:
       - transcendental extensions
       - infinitesimal extensions
       - algebraic extensions

Author:

    <NAME> (leonardo) 2012-01-05

Notes:
    
--*/
#include<iostream>
#include"z3.h"
#include"api_log_macros.h"
#include"api_context.h"
#include"realclosure.h"

extern "C" {

    static rcmanager & rcfm(Z3_context c) {
        return mk_c(c)->rcfm();
    }

    static void reset_rcf_cancel(Z3_context c) {
        rcfm(c).reset_cancel();
    }

    static rcnumeral to_rcnumeral(Z3_rcf_num a) { 
        return rcnumeral::mk(a); 
    }

    static Z3_rcf_num from_rcnumeral(rcnumeral a) { 
        return reinterpret_cast<Z3_rcf_num>(a.c_ptr()); 
    }

    void Z3_API Z3_rcf_del(Z3_context c, Z3_rcf_num a) {
        Z3_TRY;
        LOG_Z3_rcf_del(c, a);
        RESET_ERROR_CODE();
        rcnumeral _a = to_rcnumeral(a);
        rcfm(c).del(_a);
        Z3_CATCH;
    }

    Z3_rcf_num Z3_API Z3_rcf_mk_rational(Z3_context c, Z3_string val) {
        Z3_TRY;
        LOG_Z3_rcf_mk_rational(c, val);
        RESET_ERROR_CODE();
        reset_rcf_cancel(c);
        scoped_mpq q(rcfm(c).qm());
        rcfm(c).qm().set(q, val);
        rcnumeral r;
        rcfm(c).set(r, q);
        RETURN_Z3(from_rcnumeral(r));
        Z3_CATCH_RETURN(0);
    }

    Z3_rcf_num Z3_API Z3_rcf_mk_small_int(Z3_context c, int val) {
        Z3_TRY;
        LOG_Z3_rcf_mk_small_int(c, val);
        RESET_ERROR_CODE();
        reset_rcf_cancel(c);
        rcnumeral r;
        rcfm(c).set(r, val);
        RETURN_Z3(from_rcnumeral(r));
        Z3_CATCH_RETURN(0);
    }

    Z3_rcf_num Z3_API Z3_rcf_mk_pi(Z3_context c) {
        Z3_TRY;
        LOG_Z3_rcf_mk_pi(c);
        RESET_ERROR_CODE();
        reset_rcf_cancel(c);
        rcnumeral r;
        rcfm(c).mk_pi(r);
        RETURN_Z3(from_rcnumeral(r));
        Z3_CATCH_RETURN(0);
    }

    Z3_rcf_num Z3_API Z3_rcf_mk_e(Z3_context c) {
        Z3_TRY;
        LOG_Z3_rcf_mk_e(c);
        RESET_ERROR_CODE();
        reset_rcf_cancel(c);
        rcnumeral r;
        rcfm(c).mk_e(r);
        RETURN_Z3(from_rcnumeral(r));
        Z3_CATCH_RETURN(0);
    }

    Z3_rcf_num Z3_API Z3_rcf_mk_infinitesimal(Z3_context c, Z3_string name) {
        Z3_TRY;
        LOG_Z3_rcf_mk_infinitesimal(c, name);
        RESET_ERROR_CODE();
        reset_rcf_cancel(c);
        rcnumeral r;
        rcfm(c).mk_infinitesimal(name, r);
        RETURN_Z3(from_rcnumeral(r));
        Z3_CATCH_RETURN(0);
    }

    unsigned Z3_API Z3_rcf_mk_roots(Z3_context c, unsigned n, Z3_rcf_num const a[], Z3_rcf_num roots[]) {
        Z3_TRY;
        LOG_Z3_rcf_mk_roots(c, n, a, roots);
        RESET_ERROR_CODE();
        reset_rcf_cancel(c);
        rcnumeral_vector av;
        unsigned rz = 0;
        for (unsigned i = 0; i < n; i++) {
            if (!rcfm(c).is_zero(to_rcnumeral(a[i])))
                rz = i + 1;
            av.push_back(to_rcnumeral(a[i]));
        }
        if (rz == 0) {
            // it is the zero polynomial
            SET_ERROR_CODE(Z3_INVALID_ARG);
            return 0;
        }
        av.shrink(rz);
        rcnumeral_vector rs;
        rcfm(c).isolate_roots(av.size(), av.c_ptr(), rs);
        unsigned num_roots = rs.size();
        for (unsigned i = 0; i < num_roots; i++) {
            roots[i] = from_rcnumeral(rs[i]);
        }
        return num_roots;
        Z3_CATCH_RETURN(0);
    }<commit_msg>Fix RCF API logging bug<commit_after>/*++
Copyright (c) 2013 Microsoft Corporation

Module Name:

    api_rcf.cpp

Abstract:

    Additional APIs for handling elements of the Z3 real closed field that contains:
       - transcendental extensions
       - infinitesimal extensions
       - algebraic extensions

Author:

    <NAME> (leonardo) 2012-01-05

Notes:
    
--*/
#include<iostream>
#include"z3.h"
#include"api_log_macros.h"
#include"api_context.h"
#include"realclosure.h"

extern "C" {

    static rcmanager & rcfm(Z3_context c) {
        return mk_c(c)->rcfm();
    }

    static void reset_rcf_cancel(Z3_context c) {
        rcfm(c).reset_cancel();
    }

    static rcnumeral to_rcnumeral(Z3_rcf_num a) { 
        return rcnumeral::mk(a); 
    }

    static Z3_rcf_num from_rcnumeral(rcnumeral a) { 
        return reinterpret_cast<Z3_rcf_num>(a.c_ptr()); 
    }

    void Z3_API Z3_rcf_del(Z3_context c, Z3_rcf_num a) {
        Z3_TRY;
        LOG_Z3_rcf_del(c, a);
        RESET_ERROR_CODE();
        rcnumeral _a = to_rcnumeral(a);
        rcfm(c).del(_a);
        Z3_CATCH;
    }

    Z3_rcf_num Z3_API Z3_rcf_mk_rational(Z3_context c, Z3_string val) {
        Z3_TRY;
        LOG_Z3_rcf_mk_rational(c, val);
        RESET_ERROR_CODE();
        reset_rcf_cancel(c);
        scoped_mpq q(rcfm(c).qm());
        rcfm(c).qm().set(q, val);
        rcnumeral r;
        rcfm(c).set(r, q);
        RETURN_Z3(from_rcnumeral(r));
        Z3_CATCH_RETURN(0);
    }

    Z3_rcf_num Z3_API Z3_rcf_mk_small_int(Z3_context c, int val) {
        Z3_TRY;
        LOG_Z3_rcf_mk_small_int(c, val);
        RESET_ERROR_CODE();
        reset_rcf_cancel(c);
        rcnumeral r;
        rcfm(c).set(r, val);
        RETURN_Z3(from_rcnumeral(r));
        Z3_CATCH_RETURN(0);
    }

    Z3_rcf_num Z3_API Z3_rcf_mk_pi(Z3_context c) {
        Z3_TRY;
        LOG_Z3_rcf_mk_pi(c);
        RESET_ERROR_CODE();
        reset_rcf_cancel(c);
        rcnumeral r;
        rcfm(c).mk_pi(r);
        RETURN_Z3(from_rcnumeral(r));
        Z3_CATCH_RETURN(0);
    }

    Z3_rcf_num Z3_API Z3_rcf_mk_e(Z3_context c) {
        Z3_TRY;
        LOG_Z3_rcf_mk_e(c);
        RESET_ERROR_CODE();
        reset_rcf_cancel(c);
        rcnumeral r;
        rcfm(c).mk_e(r);
        RETURN_Z3(from_rcnumeral(r));
        Z3_CATCH_RETURN(0);
    }

    Z3_rcf_num Z3_API Z3_rcf_mk_infinitesimal(Z3_context c, Z3_string name) {
        Z3_TRY;
        LOG_Z3_rcf_mk_infinitesimal(c, name);
        RESET_ERROR_CODE();
        reset_rcf_cancel(c);
        rcnumeral r;
        rcfm(c).mk_infinitesimal(name, r);
        RETURN_Z3(from_rcnumeral(r));
        Z3_CATCH_RETURN(0);
    }

    unsigned Z3_API Z3_rcf_mk_roots(Z3_context c, unsigned n, Z3_rcf_num const a[], Z3_rcf_num roots[]) {
        Z3_TRY;
        LOG_Z3_rcf_mk_roots(c, n, a, roots);
        RESET_ERROR_CODE();
        reset_rcf_cancel(c);
        rcnumeral_vector av;
        unsigned rz = 0;
        for (unsigned i = 0; i < n; i++) {
            if (!rcfm(c).is_zero(to_rcnumeral(a[i])))
                rz = i + 1;
            av.push_back(to_rcnumeral(a[i]));
        }
        if (rz == 0) {
            // it is the zero polynomial
            SET_ERROR_CODE(Z3_INVALID_ARG);
            return 0;
        }
        av.shrink(rz);
        rcnumeral_vector rs;
        rcfm(c).isolate_roots(av.size(), av.c_ptr(), rs);
        unsigned num_roots = rs.size();
        for (unsigned i = 0; i < num_roots; i++) {
            roots[i] = from_rcnumeral(rs[i]);
        }
        RETURN_Z3_rcf_mk_roots num_roots;
        Z3_CATCH_RETURN(0);
    }
{'fraction_non_alphanumeric': 0.11397367684122095, 'fraction_numerical': 0.02506300756090731, 'mean_word_length': 2.2248306997742664, 'pattern_counts': {'":': 0, '<': 13, '<?xml version=': 0, '>': 11, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '191547', 'n_tokens_mistral': 2966, 'n_tokens_neox': 2838, 'n_words': 460}