z3-src 500.0.0

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

/*++
Copyright (c) 2012 Microsoft Corporation

Module Name:

    expr2subpaving.h

Abstract:

    Translator from Z3 expressions into generic subpaving data-structure.
    
    
Author:

    Leonardo (leonardo) 2012-08-08

Notes:

--*/
#pragma once

#include "ast/ast.h"
#include "math/subpaving/subpaving.h"

class expr2var;

class expr2subpaving {
    struct imp;
    imp *  m_imp;
public:
    expr2subpaving(ast_manager & m, subpaving::context & s, expr2var * e2v = nullptr);
    ~expr2subpaving();

    ast_manager & m() const;

    subpaving::context & s() const;
    
    /**
       \brief Return true if t was encoded as a variable by the translator.
    */
    bool is_var(expr * t) const;
       
    /**
       \brief Internalize a Z3 arithmetical expression into the subpaving data-structure.

       \remark throws subpaving::exception there is a translation error (when using imprecise representations, i.e. floats, in the subpaving module)
    */
    subpaving::var internalize_term(expr * t, /* out */ mpz & n, /* out */ mpz & d);
};