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


/*++
  Copyright (c) 2025 Microsoft Corporation

  Author:
    Lev Nachmanson (levnach)
    Nikolaj Bjorner (nbjorner)
  --*/

#include "math/lp/nla_core.h"
#include "math/lp/nla_coi.h"

namespace nla {

  void coi::init() {
      indexed_uint_set visited;
      unsigned_vector todo;
      vector<occurs> var2occurs;
      m_term_set.reset();
      m_mon_set.reset();
      m_constraint_set.reset();
      m_var_set.reset();
      auto& lra = c.lra_solver();

      for (auto ci : lra.constraints().indices()) {
          auto const& c = lra.constraints()[ci];
          if (c.is_auxiliary())
              continue;
          for (auto const& [coeff, v] : c.coeffs()) {
              var2occurs.reserve(v + 1);
              var2occurs[v].constraints.push_back(ci);
          }
      }

      for (auto const& m : c.emons()) {
          for (auto v : m.vars()) {
              var2occurs.reserve(v + 1);
              var2occurs[v].monics.push_back(m.var());
          }
      }

      for (const auto *t :  lra.terms() ) {
          for (auto const iv : *t) {
              auto v = iv.j();
              var2occurs.reserve(v + 1);
              var2occurs[v].terms.push_back(t->j());
          }
      }

      for (auto const& m : c.to_refine())
          todo.push_back(m);

      for (unsigned i = 0; i < todo.size(); ++i) {
          auto v = todo[i];
          if (visited.contains(v))
              continue;
          visited.insert(v);
          m_var_set.insert(v);
          var2occurs.reserve(v + 1);
          for (auto ci : var2occurs[v].constraints) {
              m_constraint_set.insert(ci);
              auto const& c = lra.constraints()[ci];
              for (auto const& [coeff, w] : c.coeffs())
                  todo.push_back(w);
          }
          for (auto w : var2occurs[v].monics)
              todo.push_back(w);

          for (auto ti : var2occurs[v].terms) {
              for (auto iv : lra.get_term(ti))
                  todo.push_back(iv.j());
              todo.push_back(ti);
          }

          if (lra.column_has_term(v)) {
              m_term_set.insert(v);
              for (auto kv : lra.get_term(v))
                  todo.push_back(kv.j());
          }            

          if (c.is_monic_var(v)) {
              m_mon_set.insert(v);
              for (auto w : c.emons()[v])
                  todo.push_back(w);
          }
      }
  }
}