z3-src 416.0.2

Source distribution of the Z3 SMT solver, for use as a build dependency
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83

/*++
Copyright (c) 2012 Microsoft Corporation

Module Name:

    api_polynomial.cpp

Abstract:

    Polynomial manager and caches for the external API.

Author:

    Leonardo de Moura (leonardo) 2012-12-08

Notes:

--*/
#include "api/z3.h"
#include "api/api_log_macros.h"
#include "api/api_context.h"
#include "api/api_polynomial.h"
#include "api/api_ast_vector.h"
#include "ast/expr2polynomial.h"
#include "util/cancel_eh.h"
#include "util/scoped_timer.h"
#include "ast/expr2var.h"

extern "C" {

    Z3_ast_vector Z3_API Z3_polynomial_subresultants(Z3_context c, Z3_ast p, Z3_ast q, Z3_ast x) {
        Z3_TRY;
        LOG_Z3_polynomial_subresultants(c, p, q, x);
        RESET_ERROR_CODE();
        polynomial::manager & pm = mk_c(c)->pm();

        // Compute all polynomial results BEFORE allocating the result vector.
        // This avoids a memory corruption issue where allocating API objects
        // can interfere with the converter's internal state.
        expr_ref_vector results(mk_c(c)->m());
        {
            polynomial_ref _p(pm), _q(pm);
            polynomial::scoped_numeral d(pm.m());
            default_expr2polynomial converter(mk_c(c)->m(), pm);
            if (!converter.to_polynomial(to_expr(p), _p, d) ||
                !converter.to_polynomial(to_expr(q), _q, d)) {
                SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
                return nullptr;
            }

            if (converter.is_var(to_expr(x))) {
                expr2var const & mapping = converter.get_mapping();
                unsigned v_x = mapping.to_var(to_expr(x));
                if (v_x != UINT_MAX) {
                    polynomial_ref_vector rs(pm);
                    polynomial_ref r(pm);
                    expr_ref _r(mk_c(c)->m());

                    {
                        cancel_eh<reslimit> eh(mk_c(c)->poly_limit());
                        api::context::set_interruptable si(*(mk_c(c)), eh);
                        scoped_timer timer(mk_c(c)->params().m_timeout, &eh);
                        pm.psc_chain(_p, _q, v_x, rs);
                    }
                    for (unsigned i = 0; i < rs.size(); ++i) {
                        r = rs.get(i);
                        converter.to_expr(r, true, _r);
                        results.push_back(_r);
                    }
                }
            }
        }
        // Converter is now out of scope - safe to allocate result vector
        Z3_ast_vector_ref* result = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
        mk_c(c)->save_object(result);
        for (expr* e : results) {
            result->m_ast_vector.push_back(e);
        }
        RETURN_Z3(of_ast_vector(result));
        Z3_CATCH_RETURN(nullptr);
    }

};