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
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
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123

/*++
Copyright (c) 2012 Microsoft Corporation

Module Name:

    check_sat_result.h

Abstract:
    Abstract interface for storing the result produced by 
    a check_sat like command

Author:

    Leonardo (leonardo) 2012-01-23

Notes:

--*/
#pragma once

#include "model/model.h"
#include "util/lbool.h"
#include "util/statistics.h"
#include "util/event_handler.h"
#include "util/timer.h"
#include "ast/converters/model_converter.h"

/**
   \brief Abstract interface for the result of a (check-sat) like command.
   It encapsulates information such as:
      - the actual result: l_true (satisfiable), l_false (unsatisfiable), l_undef (unknown)
      - statistics
      - model (if the result is satisfiable)
      - proof (if the result is unsatisfiable)
      - unsat-core (if the result is unsatisfiable)
      - reason-unknown (if the result is unknown, i.e., the solver failed to solve the problem)
      - label (if the result is satisfiable) this is legacy for Boogie
      
*/
class check_sat_result {
protected:
    ast_manager& m;
    expr_ref_vector m_log;
    proof_ref        m_proof;
    unsigned    m_ref_count = 0;
    lbool       m_status = l_undef; 
    model_converter_ref m_mc0;
    double      m_time = 0;
    statistics m_stats;

public:
    check_sat_result(ast_manager& m): m(m), m_log(m), m_proof(m) {}
    virtual ~check_sat_result() = default;
    void inc_ref() { m_ref_count++; }
    void dec_ref() { SASSERT(m_ref_count > 0); m_ref_count--; if (m_ref_count == 0) dealloc(this); }
    lbool set_status(lbool r) { return m_status = r; }
    lbool status() const { return m_status; }
    void collect_statistics(statistics &st) const {
        collect_statistics_core(st);
        st.copy(m_stats);       
    }
    void add_statistics(statistics const &st) {
        m_stats.copy(st);
    }
    void reset_statistics() {
        m_stats.reset();
    }
   
    virtual void collect_statistics_core(statistics &st) const = 0;
    virtual void get_unsat_core(expr_ref_vector & r) = 0;
    void set_model_converter(model_converter* mc) { m_mc0 = mc; }
    model_converter* mc0() const { return m_mc0.get(); }
    virtual void get_model_core(model_ref & m) = 0;
    void get_model(model_ref & m) {
        get_model_core(m);
        if (m && mc0()) (*mc0())(m);
    }
    void log_inference(proof* p) { m_log.push_back(p); }
    void set_proof(proof* p) { m_proof = p; }
    proof* get_proof();
    virtual proof * get_proof_core() = 0;
    virtual std::string reason_unknown() const = 0;
    virtual void set_reason_unknown(char const* msg) = 0;
    void set_reason_unknown(event_handler& eh, char const* msg);
    void set_reason_unknown(event_handler& eh, std::exception& ex);
    virtual void get_labels(svector<symbol> & r) = 0;
    virtual ast_manager& get_manager() const = 0;

    class scoped_solver_time {
        check_sat_result& c;
        timer t;
    public:
        scoped_solver_time(check_sat_result& c):c(c) { c.m_time = 0; }
        ~scoped_solver_time() { c.m_time = t.get_seconds(); }
    };

    void collect_timer_stats(statistics& st) const {
        if (m_time != 0) 
            st.update("time", m_time);
    }

};

/**
   \brief Very simple implementation of the check_sat_result object.
*/
struct simple_check_sat_result : public check_sat_result {
    model_ref       m_model;
    expr_ref_vector m_core;
    proof_ref       m_proof;
    std::string     m_unknown;
    
    simple_check_sat_result(ast_manager & m);
    ast_manager& get_manager() const override { return m_proof.get_manager(); }
    void get_unsat_core(expr_ref_vector & r) override;
    void get_model_core(model_ref & m) override;
    void collect_statistics_core(statistics &st) const override {}
    proof * get_proof_core() override;
    std::string reason_unknown() const override;
    void get_labels(svector<symbol> & r) override;
    void set_reason_unknown(char const* msg) override { m_unknown = msg; }
};