z3-src 501.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
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

/*++
  Copyright (c) 2017 Microsoft Corporation

  Author:
  Nikolaj Bjorner (nbjorner)
  Lev Nachmanson (levnach)

  --*/
#pragma once

#include "math/lp/nla_common.h"
#include "math/lp/nla_intervals.h"
#include "math/lp/nex.h"
#include "math/lp/cross_nested.h"
#include "util/params.h"
#include "util/uint_set.h"
#include "math/grobner/pdd_solver.h"

namespace nla {
    class core;

    class grobner : common {
        struct config {
            bool m_propagate_quotients = false;
            bool m_gcd_test = false;
            bool m_expand_terms = false;
            // Adaptive growth (gated by arith.nl.grobner_adaptive). m_growth_boost
            // is in fixed-point units of 1/m_adaptive_unit (m_adaptive_unit == 1.0x).
            unsigned m_adaptive_unit       = 16;
            unsigned m_adaptive_max        = 4 * 16;
            unsigned m_adaptive_bump_after = 2;
        };
        config                   m_config;
        dd::pdd_manager          m_pdd_manager;
        dd::solver               m_solver;
        lp::lar_solver&          lra;
        indexed_uint_set         m_rows;
        unsigned                 m_quota = 0;
        unsigned                 m_delay_base = 0;
        unsigned                 m_delay = 0;
        unsigned                 m_growth_boost = m_config.m_adaptive_unit;
        unsigned                 m_hit_streak = 0;
        bool                     m_add_all_eqs = false;
        std::unordered_map<unsigned_vector, lpvar, hash_svector> m_mon2var;

        lp::lp_settings& lp_settings();

        // solving
        bool is_conflicting();
        bool is_conflicting(dd::solver::equation const& eq);

        bool propagate_eqs();
        bool propagate_fixed(dd::solver::equation const& eq);

        bool propagate_factorization();
        bool propagate_factorization(dd::solver::equation const& eq);

        bool propagate_linear_equations();
        bool propagate_linear_equations(dd::solver::equation const& eq);

        bool propagate_quotients();
        bool propagate_quotients(dd::solver::equation const& eq);

        svector<std::pair<unsigned, unsigned>> m_powers;
        bool propagate_gcd_test();
        bool propagate_gcd_test(dd::solver::equation const& eq);

        std::pair<lp::lar_term, rational> linear_to_term(dd::pdd q);
        
        void add_dependencies(lemma_builder& lemma, dd::solver::equation const& eq);
        void explain(dd::solver::equation const& eq, lp::explanation& exp);

        bool add_horner_conflict(dd::solver::equation const& eq);
        bool is_nla_conflict(dd::solver::equation const& eq);
        bool add_nla_conflict(dd::solver::equation const& eq);
        void check_missing_propagation(dd::solver::equation const& eq);

        // perfect-square conflict detection (arith.nl.grobner_perfect_squares),
        // a port of theory_arith_nl's is_inconsistent2.
        bool add_perfect_square_conflict(dd::solver::equation const& eq);
        template <dep_intervals::with_deps_t wd>
        void monomial_interval(rational const& coeff, unsigned_vector const& vars, scoped_dep_interval& r);

        bool equation_is_true(dd::solver::equation const& eq);

        // adaptive growth (gated by arith.nl.grobner_adaptive)
        void update_growth_boost(bool productive);

        // setup
        bool configure();
        void set_level2var();
        void find_nl_cluster();
        void prepare_rows_and_active_vars();
        void add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, svector<lpvar>& q);           
        void add_row(const std_vector<lp::row_cell<rational>>& row);
        void add_fixed_monic(unsigned j);
        bool is_solved(dd::pdd const& p, unsigned& v, dd::pdd& r);
        void add_eq(dd::pdd& p, u_dependency* dep);        
        bool is_pseudo_linear(monic const& m) const;
        const rational& val_of_fixed_var_with_deps(lpvar j, u_dependency*& dep);
        dd::pdd pdd_expr(const rational& c, lpvar j, u_dependency*& dep);  
        dd::pdd pdd_expr(lp::lar_term const& t, u_dependency*& dep);

        void display_matrix_of_m_rows(std::ostream& out) const;
        std::ostream& diagnose_pdd_miss(std::ostream& out);

    public:
        grobner(core *core);        
        void operator()();
        void updt_params(params_ref const& p);
    }; 
}