mirror of
https://github.com/Z3Prover/z3
synced 2025-04-13 20:38:43 +00:00
cleanup and some changes in TRACE statements
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson
parent
82115e69ac
commit
8d05894db7
|
|
@ -1,76 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2017 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
<name>
|
||||
|
||||
Abstract:
|
||||
|
||||
<abstract>
|
||||
|
||||
Author:
|
||||
Nikolaj Bjorner (nbjorner)
|
||||
Lev Nachmanson (levnach)
|
||||
|
||||
Revision History:
|
||||
|
||||
|
||||
--*/
|
||||
|
||||
#pragma once
|
||||
#include "math/lp/binary_heap_priority_queue.h"
|
||||
namespace lp {
|
||||
class active_set {
|
||||
std::unordered_set<constraint*, constraint_hash, constraint_equal> m_cs;
|
||||
binary_heap_priority_queue<int> m_q;
|
||||
std::unordered_map<unsigned, constraint *> m_id_to_constraint;
|
||||
public:
|
||||
std::unordered_set<constraint*, constraint_hash, constraint_equal> cs() const { return m_cs;}
|
||||
|
||||
bool contains(const constraint* c) const {
|
||||
return m_id_to_constraint.find(c->id()) != m_id_to_constraint.end();
|
||||
}
|
||||
|
||||
bool is_empty() const { return m_cs.size() == 0; }
|
||||
// low priority will be dequeued first
|
||||
void add_constraint(constraint* c, int priority) {
|
||||
if (contains(c))
|
||||
return;
|
||||
m_cs.insert(c);
|
||||
m_id_to_constraint[c->id()] = c;
|
||||
m_q.enqueue(c->id(), priority);
|
||||
}
|
||||
|
||||
void clear() {
|
||||
m_cs.clear();
|
||||
m_id_to_constraint.clear();
|
||||
m_q.clear();
|
||||
}
|
||||
|
||||
|
||||
constraint* remove_constraint() {
|
||||
if (m_cs.size() == 0)
|
||||
return nullptr;
|
||||
unsigned id = m_q.dequeue();
|
||||
auto it = m_id_to_constraint.find(id);
|
||||
lp_assert(it != m_id_to_constraint.end());
|
||||
constraint* c = it->second;
|
||||
m_cs.erase(c);
|
||||
m_id_to_constraint.erase(it);
|
||||
return c;
|
||||
}
|
||||
|
||||
unsigned size() const {
|
||||
return static_cast<unsigned>(m_cs.size());
|
||||
}
|
||||
|
||||
void remove_constraint(constraint * c) {
|
||||
if (! contains(c)) return;
|
||||
|
||||
m_cs.erase(c);
|
||||
m_id_to_constraint.erase(c->id());
|
||||
m_q.remove(c->id());
|
||||
}
|
||||
};
|
||||
}
|
||||
|
|
@ -1,99 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2017 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
<name>
|
||||
|
||||
Abstract:
|
||||
|
||||
<abstract>
|
||||
|
||||
Author:
|
||||
Nikolaj Bjorner (nbjorner)
|
||||
Lev Nachmanson (levnach)
|
||||
|
||||
Revision History:
|
||||
|
||||
|
||||
--*/
|
||||
|
||||
#pragma once
|
||||
namespace lp {
|
||||
class constraint; // forward definition
|
||||
struct constraint_hash {
|
||||
size_t operator() (const constraint* c) const;
|
||||
};
|
||||
|
||||
struct constraint_equal {
|
||||
bool operator() (const constraint * a, const constraint * b) const;
|
||||
};
|
||||
|
||||
class constraint { // we only have less or equal for the inequality sign, which is enough for integral variables
|
||||
int m_id;
|
||||
bool m_is_ineq;
|
||||
polynomial m_poly;
|
||||
mpq m_d; // the divider for the case of a divisibility constraint
|
||||
std::unordered_set<constraint_index> m_assert_origins; // these indices come from the client and get collected during tightening
|
||||
public :
|
||||
unsigned id() const { return m_id; }
|
||||
const polynomial & poly() const { return m_poly; }
|
||||
polynomial & poly() { return m_poly; }
|
||||
std::unordered_set<constraint_index> & assert_origins() { return m_assert_origins;}
|
||||
const std::unordered_set<constraint_index> & assert_origins() const { return m_assert_origins;}
|
||||
bool is_lemma() const { return !is_assert(); }
|
||||
bool is_assert() const { return m_assert_origins.size() == 1; }
|
||||
bool is_ineq() const { return m_is_ineq; }
|
||||
const mpq & divider() const { return m_d; }
|
||||
public:
|
||||
constraint(
|
||||
unsigned id,
|
||||
constraint_index assert_origin,
|
||||
const polynomial & p,
|
||||
bool is_ineq):
|
||||
m_id(id),
|
||||
m_is_ineq(is_ineq),
|
||||
m_poly(p)
|
||||
{ // creates an assert
|
||||
m_assert_origins.insert(assert_origin);
|
||||
}
|
||||
constraint(
|
||||
unsigned id,
|
||||
const std::unordered_set<constraint_index>& origins,
|
||||
const polynomial & p,
|
||||
bool is_ineq):
|
||||
m_id(id),
|
||||
m_is_ineq(is_ineq),
|
||||
m_poly(p),
|
||||
m_assert_origins(origins)
|
||||
{}
|
||||
|
||||
|
||||
|
||||
constraint(
|
||||
unsigned id,
|
||||
const polynomial & p,
|
||||
bool is_ineq):
|
||||
m_id(id),
|
||||
m_is_ineq(is_ineq),
|
||||
m_poly(p) { // creates a lemma
|
||||
}
|
||||
|
||||
public:
|
||||
constraint() {}
|
||||
|
||||
const mpq & coeff(var_index j) const {
|
||||
return m_poly.coeff(j);
|
||||
}
|
||||
const vector<monomial>& coeffs() const { return m_poly.m_coeffs;}
|
||||
|
||||
bool is_tight(unsigned j) const {
|
||||
const mpq & a = m_poly.coeff(j);
|
||||
return a == 1 || a == -1;
|
||||
}
|
||||
void add_predecessor(const constraint* p) {
|
||||
lp_assert(p != nullptr);
|
||||
for (auto m : p->assert_origins())
|
||||
m_assert_origins.insert(m); }
|
||||
};
|
||||
}
|
||||
|
|
@ -39,7 +39,7 @@ bool horner::row_has_monomial_to_refine(const T& row) const {
|
|||
// Returns true if the row has at least two monomials sharing a variable
|
||||
template <typename T>
|
||||
bool horner::row_is_interesting(const T& row) const {
|
||||
TRACE("nla_solver", m_core->print_term(row, tout););
|
||||
TRACE("nla_solver_details", m_core->print_term(row, tout););
|
||||
SASSERT(row_has_monomial_to_refine(row));
|
||||
std::unordered_set<lpvar> seen;
|
||||
for (const auto& p : row) {
|
||||
|
|
@ -67,6 +67,7 @@ bool horner::lemmas_on_expr(nex& e) {
|
|||
TRACE("nla_horner", tout << "e = " << e << "\n";);
|
||||
bool conflict = false;
|
||||
cross_nested cn(e, [this, & conflict](const nex& n) {
|
||||
TRACE("nla_horner", tout << "cross-nested n = " << n << "\n";);
|
||||
auto i = interval_of_expr(n);
|
||||
TRACE("nla_horner", tout << "callback n = " << n << "\ni="; m_intervals.display(tout, i) << "\n";);
|
||||
|
||||
|
|
|
|||
|
|
@ -1257,7 +1257,7 @@ lbool core::inner_check(bool derived) {
|
|||
return l_false;
|
||||
}
|
||||
|
||||
TRACE("nla_cn_details", print_terms(tout););
|
||||
TRACE("nla_solver", print_terms(tout); m_lar_solver.print_constraints(tout););
|
||||
for (int search_level = 0; search_level < 3 && !done(); search_level++) {
|
||||
TRACE("nla_solver", tout << "derived = " << derived << ", search_level = " << search_level << "\n";);
|
||||
if (search_level == 0) {
|
||||
|
|
|
|||
|
|
@ -289,9 +289,6 @@ public:
|
|||
lp::lp_settings& lp_settings();
|
||||
const lp::lp_settings& lp_settings() const;
|
||||
unsigned random();
|
||||
void map_monomial_vars_to_monomial_indices(unsigned i);
|
||||
|
||||
void map_vars_to_monomials();
|
||||
|
||||
// we look for octagon constraints here, with a left part +-x +- y
|
||||
void collect_equivs();
|
||||
|
|
|
|||
Loading…
Reference in a new issue