mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix the build

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-08-23 16:36:17 -07:00
parent 58854fa44b
commit 3d2fc57b82
3 changed files with 14 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/math/lp/cross_nested.h
View file

@ -38,6 +38,7 @@ class cross_nested {
nex * m_e; nex * m_e;
std::function<bool (const nex*)> m_call_on_result; std::function<bool (const nex*)> m_call_on_result;
std::function<bool (unsigned)> m_var_is_fixed; std::function<bool (unsigned)> m_var_is_fixed;
std::function<unsigned ()> m_random;
bool m_done; bool m_done;
std::unordered_map<lpvar, occ> m_occurences_map; std::unordered_map<lpvar, occ> m_occurences_map;
std::unordered_map<lpvar, unsigned> m_powers; std::unordered_map<lpvar, unsigned> m_powers;
@ -45,6 +46,7 @@ class cross_nested {
ptr_vector<nex> m_b_split_vec; ptr_vector<nex> m_b_split_vec;
int m_reported; int m_reported;
bool m_random_bit; bool m_random_bit;
#ifdef Z3DEBUG #ifdef Z3DEBUG
nex* m_e_clone; nex* m_e_clone;
#endif #endif
@ -53,9 +55,11 @@ class cross_nested {
} }
public: public:
cross_nested(std::function<bool (const nex*)> call_on_result, cross_nested(std::function<bool (const nex*)> call_on_result,
std::function<bool (unsigned)> var_is_fixed): std::function<bool (unsigned)> var_is_fixed,
std::function<unsigned ()> random):
m_call_on_result(call_on_result), m_call_on_result(call_on_result),
m_var_is_fixed(var_is_fixed), m_var_is_fixed(var_is_fixed),
m_random(random),
m_done(false), m_done(false),
m_reported(0) m_reported(0)
{} {}
@ -363,7 +367,7 @@ public:
for (auto & p : m_occurences_map) for (auto & p : m_occurences_map)
vars.push_back(p.first); vars.push_back(p.first);
m_random_bit = random() % 2; m_random_bit = m_random() % 2;
TRACE("nla_cn", tout << "m_random_bit = " << m_random_bit << "\n";); TRACE("nla_cn", tout << "m_random_bit = " << m_random_bit << "\n";);
std::sort(vars.begin(), vars.end(), [this](lpvar j, lpvar k) std::sort(vars.begin(), vars.end(), [this](lpvar j, lpvar k)
{ {

5
src/math/lp/horner.cpp
View file

@ -91,8 +91,9 @@ template <typename T>
bool horner::lemmas_on_row(const T& row) { bool horner::lemmas_on_row(const T& row) {
cross_nested cn( cross_nested cn(
[this](const nex* n) { return check_cross_nested_expr(n); }, [this](const nex* n) { return check_cross_nested_expr(n); },
[this](unsigned j) { return c().var_is_fixed(j); } [this](unsigned j) { return c().var_is_fixed(j); },
); [this]() { return c().random(); }
);
SASSERT (row_is_interesting(row)); SASSERT (row_is_interesting(row));
create_sum_from_row(row, cn); create_sum_from_row(row, cn);

7
src/test/lp/lp.cpp
View file

@ -74,11 +74,14 @@ void test_cn_on_expr(nex_sum *t, cross_nested& cn) {
} }
void test_cn() { void test_cn() {
cross_nested cn([](const nex* n) { cross_nested cn(
[](const nex* n) {
TRACE("nla_cn_test", tout << *n << "\n";); TRACE("nla_cn_test", tout << *n << "\n";);
return false; return false;
} , } ,
[](unsigned) { return false; }); [](unsigned) { return false; },
[]{ return 1; }
);
enable_trace("nla_cn"); enable_trace("nla_cn");
enable_trace("nla_cn_details"); enable_trace("nla_cn_details");
nex_var* a = cn.mk_var(0); nex_var* a = cn.mk_var(0);