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
/*++
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();
// Auxiliary constraints (atoms of nla lemmas) stay in the cone of
// influence: a case-split literal is not implied by the other constraints,
// so nlsat needs it. nra_solver filters the dyadic artifacts among them.
for (auto ci : lra.constraints().indices()) {
auto const& c = lra.constraints()[ci];
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());
}
}
// Transcendental applications (sin(x), cos(x), ...) are not monomials
// or lar_solver terms, so without this they would never be reachable
// by the occurs-graph traversal below: seed both the argument and the
// output variable of every registered application directly, so any
// linear constraint that mentions either one (e.g. an assertion on
// sin(x), or the Taylor-sandwich axiom nra_solver adds relating val to
// arg) gets pulled into the COI, and nra_solver's setup_solver_poly
// creates nlsat variables/definitions for them.
for (auto const& a : c.get_transcendentals().apps()) {
todo.push_back(a.arg);
todo.push_back(a.val);
}
for (auto const& a : c.get_transcendentals().atan2_apps()) {
todo.push_back(a.y);
todo.push_back(a.x);
todo.push_back(a.val);
}
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);
}
}
}
}