mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
fix build issues part 3
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
fcfaedd9ec
commit
6e021781cd
|
@ -66,16 +66,17 @@ namespace lean {
|
|||
lisp_elem m_formula_lisp_elem;
|
||||
|
||||
std::unordered_map<std::string, unsigned> m_name_to_var_index;
|
||||
std::vector<formula_constraint> m_constraints;
|
||||
std::string m_file_name;
|
||||
std::ifstream m_file_stream;
|
||||
std::string m_line;
|
||||
bool m_is_OK;
|
||||
unsigned m_line_number;
|
||||
std::vector<formula_constraint> m_constraints;
|
||||
bool m_is_OK;
|
||||
unsigned m_line_number;
|
||||
std::string m_file_name;
|
||||
std::ifstream m_file_stream;
|
||||
std::string m_line;
|
||||
smt_reader(std::string file_name):
|
||||
m_is_OK(true),
|
||||
m_line_number(0),
|
||||
m_file_name(file_name), m_file_stream(file_name) {
|
||||
m_file_name(file_name),
|
||||
m_file_stream(file_name) {
|
||||
}
|
||||
|
||||
void set_error() {
|
||||
|
|
|
@ -18,12 +18,13 @@ namespace lean {
|
|||
class bound_analyzer_on_row {
|
||||
|
||||
linear_combination_iterator<mpq> & m_it;
|
||||
unsigned m_row_or_term_index;
|
||||
int m_column_of_u; // index of an unlimited from above monoid
|
||||
// -1 means that such a value is not found, -2 means that at least two of such monoids were found
|
||||
int m_column_of_l; // index of an unlimited from below monoid
|
||||
impq m_rs;
|
||||
bound_propagator & m_bp;
|
||||
bound_propagator & m_bp;
|
||||
unsigned m_row_or_term_index;
|
||||
int m_column_of_u; // index of an unlimited from above monoid
|
||||
// -1 means that such a value is not found, -2 means that at least two of such monoids were found
|
||||
int m_column_of_l; // index of an unlimited from below monoid
|
||||
impq m_rs;
|
||||
|
||||
public :
|
||||
// constructor
|
||||
bound_analyzer_on_row(
|
||||
|
@ -34,11 +35,11 @@ public :
|
|||
)
|
||||
:
|
||||
m_it(it),
|
||||
m_row_or_term_index(row_or_term_index),
|
||||
m_rs(rs),
|
||||
m_bp(bp),
|
||||
m_row_or_term_index(row_or_term_index),
|
||||
m_column_of_u(-1),
|
||||
m_column_of_l(-1)
|
||||
m_column_of_l(-1),
|
||||
m_rs(rs)
|
||||
{}
|
||||
|
||||
|
||||
|
|
|
@ -8,15 +8,15 @@
|
|||
#include "util/lp/lar_term.h"
|
||||
namespace lean {
|
||||
struct iterator_on_term_with_basis_var:linear_combination_iterator<mpq> {
|
||||
std::unordered_map<unsigned, mpq>::const_iterator m_i; // the offset in term coeffs
|
||||
bool m_term_j_returned;
|
||||
const lar_term & m_term;
|
||||
unsigned m_term_j;
|
||||
std::unordered_map<unsigned, mpq>::const_iterator m_i; // the offset in term coeffs
|
||||
bool m_term_j_returned;
|
||||
unsigned m_term_j;
|
||||
unsigned size() const {return static_cast<unsigned>(m_term.m_coeffs.size() + 1);}
|
||||
iterator_on_term_with_basis_var(const lar_term & t, unsigned term_j) :
|
||||
m_term_j_returned(false),
|
||||
m_i(t.m_coeffs.begin()),
|
||||
m_term(t),
|
||||
m_i(t.m_coeffs.begin()),
|
||||
m_term_j_returned(false),
|
||||
m_term_j(term_j) {}
|
||||
|
||||
bool next(mpq & a, unsigned & i) {
|
||||
|
|
Loading…
Reference in a new issue