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
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
nlsat_interval_set.h
Abstract:
Sets of disjoint infeasible intervals.
Author:
Leonardo de Moura (leonardo) 2012-01-11.
Revision History:
--*/
#pragma once
#include "nlsat/nlsat_types.h"
namespace nlsat {
class interval_set;
class interval_set_manager {
anum_manager & m_am;
small_object_allocator & m_allocator;
svector<char> m_already_visited;
random_gen m_rand;
void del(interval_set * s);
bool find_complement_sup(interval_set const * s, unsigned & i);
public:
interval_set_manager(anum_manager & m, small_object_allocator & a);
void set_seed(unsigned s) { m_rand.set_seed(s); }
unsigned get_seed() const { return m_rand.get_seed(); }
/**
\brief Return the empty set.
*/
interval_set * mk_empty() { return nullptr; }
/**
\brief Return a set of composed of a single interval.
*/
interval_set * mk(bool lower_open, bool lower_inf, anum const & lower,
bool upper_open, bool upper_inf, anum const & upper,
literal justification, clause const* cls);
/**
\brief Return the union of two sets.
*/
interval_set * mk_union(interval_set const * s1, interval_set const * s2);
/**
\brief Reference counting
*/
void dec_ref(interval_set * s);
void inc_ref(interval_set * s);
/**
\brief Return true if s is the empty set.
*/
bool is_empty(interval_set const * s) {
return s == nullptr;
}
/**
\brief Return true if the set contains all real numbers.
*/
bool is_full(interval_set const * s);
/**
`\brief Return true if s1 is a subset of s2.
*/
bool subset(interval_set const * s1, interval_set const * s2);
/**
\brief Return true if s1 and s2 cover the same subset of R.
The justifications are ignored
*/
bool set_eq(interval_set const * s1, interval_set const * s2);
/**
\brief Return true if s1 and s2 are the same (the justifications are taking into account).
*/
bool eq(interval_set const * s1, interval_set const * s2);
/**
\brief Return a set of literals that justify s.
*/
void get_justifications(interval_set const * s, literal_vector & js, ptr_vector<clause>& clauses );
std::ostream& display(std::ostream & out, interval_set const * s) const;
unsigned num_intervals(interval_set const * s) const;
/**
\brief (For debugging purposes) Return one of the intervals in s.
\pre idx < num_intervals()
*/
interval_set * get_interval(interval_set const * s, unsigned idx) const;
/**
\brief Select a witness w in the complement of s.
\pre !is_full(s)
*/
void pick_in_complement(interval_set const * s, bool is_int, anum & w, bool randomize);
/**
\brief Pick the largest element of the complement of s.
Return false if the complement is unbounded above (w is not modified).
Otherwise w is set to the maximum of the complement when it is attained,
or to some element of the complement below its supremum when it is not.
*/
bool pick_max_in_complement(interval_set const * s, anum & w);
/**
\brief Compute the supremum of the complement of s.
Return false if the complement is unbounded above (sup is not modified).
Otherwise sup is set to the supremum of the complement, and attained
to true iff sup itself belongs to the complement.
*/
bool query_max_in_complement(interval_set const * s, anum & sup, bool & attained);
};
typedef obj_ref<interval_set, interval_set_manager> interval_set_ref;
inline std::ostream & operator<<(std::ostream & out, interval_set_ref const & s) {
s.m().display(out, s);
return out;
}
}