z3-src 503.2.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
52
53
54
55
56
57
58

/*++
Copyright (c) 2022 Microsoft Corporation

Module Name:

    extract_eqs.h

Abstract:

    simplifier for solving equations

Author:

    Nikolaj Bjorner (nbjorner) 2022-11-2.

--*/


#pragma once

#include "ast/ast_pp.h"
#include "ast/simplifiers/dependent_expr_state.h"
#include "ast/rewriter/th_rewriter.h"
#include "ast/expr_substitution.h"
#include "util/scoped_ptr_vector.h"


namespace euf {

    struct dependent_eq {
        expr* orig;       // original expression that encoded equation
        app* var;         // isolated variable
        expr_ref term;    // defined term
        expr_dependency_ref dep;
        proof_ref pr;
        dependent_eq(expr* orig, app* var, expr_ref const& term, expr_dependency* d, proof* p = nullptr) :
            orig(orig), var(var), term(term), dep(d, term.get_manager()), pr(p, term.get_manager()) {}
    };

    typedef vector<dependent_eq> dep_eq_vector;

    class extract_eq {
    public:
        virtual ~extract_eq() = default;
        virtual void get_eqs(dependent_expr const& e, dep_eq_vector& eqs) = 0;
        virtual void pre_process(dependent_expr_state& fmls) {}
        virtual void updt_params(params_ref const& p) {}
        virtual void set_allow_booleans(bool f) {}
        virtual bool supports_proofs() const { return false; }
    };

    void register_extract_eqs(ast_manager& m, scoped_ptr_vector<extract_eq>& ex);

}

inline std::ostream& operator<<(std::ostream& out, euf::dependent_eq const& eq) {
    return out << mk_pp(eq.var, eq.term.m()) << " = " << eq.term << "\n";
}