z3-src 415.4.3

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

/*++
  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/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;
        };
        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;
        bool                     m_add_all_eqs = false;
        config                   m_config;
        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);

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

        // 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);
    }; 
}