z3-src 501.0.1

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

/*++
Copyright (c) 2018 Arie Gurfinkel

Module Name:

    spacer_sat_answer.h

Abstract:

  Compute refutation proof for CHC

Author:

    Arie Gurfinkel

Revision History:

--*/

#pragma once

#include "muz/spacer/spacer_context.h"
#include "ast/ast.h"
#include "util/obj_hashtable.h"
#include "model/model.h"
#include "solver/solver.h"

namespace spacer {

class ground_sat_answer_op {
    const context &m_ctx;
    ast_manager &m;
    const manager &m_pm;

    expr_ref_vector m_pinned;
    obj_map<expr, proof*> m_cache;

    ref<solver> m_solver;

    struct frame;

    proof *mk_proof_step(frame &fr);
    void mk_children(frame &fr, vector<frame> &todo);
    void mk_child_subst_from_model(func_decl *pred, unsigned i,
                                   model_ref &mdl, expr_ref_vector &subst);

public:
    ground_sat_answer_op(const context &ctx);

    proof_ref operator() (pred_transformer &query);
};
}