mirror of
https://github.com/Z3Prover/z3
synced 2025-06-05 21:53:23 +00:00
remove unused files
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
5e0da456a9
commit
7e0a7d73f2
3 changed files with 0 additions and 2290 deletions
File diff suppressed because it is too large
Load diff
|
|
@ -1,153 +0,0 @@
|
||||||
/*++
|
|
||||||
Copyright (c) 2017 Microsoft Corporation
|
|
||||||
|
|
||||||
Module Name:
|
|
||||||
|
|
||||||
<name>
|
|
||||||
|
|
||||||
Abstract:
|
|
||||||
|
|
||||||
<abstract>
|
|
||||||
|
|
||||||
Author:
|
|
||||||
|
|
||||||
Lev Nachmanson (levnach)
|
|
||||||
|
|
||||||
Revision History:
|
|
||||||
|
|
||||||
|
|
||||||
--*/
|
|
||||||
#include "util/lp/lar_solver.h"
|
|
||||||
namespace lp {
|
|
||||||
quick_xplain::quick_xplain(vector<std::pair<mpq, constraint_index>> & explanation, const lar_solver & ls, lar_solver & qsol) :
|
|
||||||
m_explanation(explanation),
|
|
||||||
m_parent_solver(ls),
|
|
||||||
m_qsol(qsol) {
|
|
||||||
}
|
|
||||||
void quick_xplain::add_constraint_to_qsol(unsigned j) {
|
|
||||||
auto & lar_c = m_constraints_in_local_vars[j];
|
|
||||||
auto ls = lar_c.get_left_side_coefficients();
|
|
||||||
auto ci = m_qsol.add_constraint(ls, lar_c.m_kind, lar_c.m_right_side);
|
|
||||||
m_local_ci_to_constraint_offsets[ci] = j;
|
|
||||||
}
|
|
||||||
|
|
||||||
void quick_xplain::copy_constraint_and_add_constraint_vars(const lar_constraint& lar_c) {
|
|
||||||
vector < std::pair<mpq, unsigned>> ls;
|
|
||||||
for (auto & p : lar_c.get_left_side_coefficients()) {
|
|
||||||
unsigned j = p.second;
|
|
||||||
unsigned lj = m_qsol.add_var(j, false);
|
|
||||||
ls.push_back(std::make_pair(p.first, lj));
|
|
||||||
}
|
|
||||||
m_constraints_in_local_vars.push_back(lar_constraint(ls, lar_c.m_kind, lar_c.m_right_side));
|
|
||||||
|
|
||||||
}
|
|
||||||
|
|
||||||
bool quick_xplain::infeasible() {
|
|
||||||
m_qsol.solve();
|
|
||||||
return m_qsol.get_status() == lp_status::INFEASIBLE;
|
|
||||||
}
|
|
||||||
|
|
||||||
// u - unexplored constraints
|
|
||||||
// c and x are assumed, in other words, all constrains of x and c are already added to m_qsol
|
|
||||||
void quick_xplain::minimize(const vector<unsigned>& u) {
|
|
||||||
unsigned k = 0;
|
|
||||||
unsigned initial_stack_size = m_qsol.constraint_stack_size();
|
|
||||||
for (; k < u.size();k++) {
|
|
||||||
m_qsol.push();
|
|
||||||
add_constraint_to_qsol(u[k]);
|
|
||||||
if (infeasible())
|
|
||||||
break;
|
|
||||||
}
|
|
||||||
m_x.insert(u[k]);
|
|
||||||
unsigned m = k / 2; // the split
|
|
||||||
if (m < k) {
|
|
||||||
m_qsol.pop(k + 1 - m);
|
|
||||||
add_constraint_to_qsol(u[k]);
|
|
||||||
if (!infeasible()) {
|
|
||||||
vector<unsigned> un;
|
|
||||||
for (unsigned j = m; j < k; j++)
|
|
||||||
un.push_back(u[j]);
|
|
||||||
minimize(un);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
if (m > 0) {
|
|
||||||
lp_assert(m_qsol.constraint_stack_size() >= initial_stack_size);
|
|
||||||
m_qsol.pop(m_qsol.constraint_stack_size() - initial_stack_size);
|
|
||||||
for (auto j : m_x)
|
|
||||||
add_constraint_to_qsol(j);
|
|
||||||
if (!infeasible()) {
|
|
||||||
vector<unsigned> un;
|
|
||||||
for (unsigned j = 0; j < m; j++)
|
|
||||||
un.push_back(u[j]);
|
|
||||||
minimize(un);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
void quick_xplain::run(vector<std::pair<mpq, constraint_index>> & explanation, const lar_solver & ls){
|
|
||||||
if (explanation.size() <= 2) return;
|
|
||||||
lar_solver qsol;
|
|
||||||
lp_assert(ls.explanation_is_correct(explanation));
|
|
||||||
quick_xplain q(explanation, ls, qsol);
|
|
||||||
q.solve();
|
|
||||||
}
|
|
||||||
|
|
||||||
void quick_xplain::copy_constraints_to_local_constraints() {
|
|
||||||
for (auto & p : m_explanation) {
|
|
||||||
const auto & lar_c = m_parent_solver.get_constraint(p.second);
|
|
||||||
m_local_constraint_offset_to_external_ci.push_back(p.second);
|
|
||||||
copy_constraint_and_add_constraint_vars(lar_c);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
bool quick_xplain::is_feasible(const vector<unsigned> & x, unsigned k) const {
|
|
||||||
lar_solver l;
|
|
||||||
for (unsigned i : x) {
|
|
||||||
if (i == k)
|
|
||||||
continue;
|
|
||||||
vector < std::pair<mpq, unsigned>> ls;
|
|
||||||
const lar_constraint & c = m_constraints_in_local_vars[i];
|
|
||||||
for (auto & p : c.get_left_side_coefficients()) {
|
|
||||||
unsigned lj = l.add_var(p.second, false);
|
|
||||||
ls.push_back(std::make_pair(p.first, lj));
|
|
||||||
}
|
|
||||||
l.add_constraint(ls, c.m_kind, c.m_right_side);
|
|
||||||
}
|
|
||||||
l.solve();
|
|
||||||
return l.get_status() != lp_status::INFEASIBLE;
|
|
||||||
}
|
|
||||||
|
|
||||||
bool quick_xplain::x_is_minimal() const {
|
|
||||||
vector<unsigned> x;
|
|
||||||
for (auto j : m_x)
|
|
||||||
x.push_back(j);
|
|
||||||
|
|
||||||
for (unsigned k = 0; k < x.size(); k++) {
|
|
||||||
lp_assert(is_feasible(x, x[k]));
|
|
||||||
}
|
|
||||||
return true;
|
|
||||||
}
|
|
||||||
|
|
||||||
void quick_xplain::solve() {
|
|
||||||
copy_constraints_to_local_constraints();
|
|
||||||
m_qsol.push();
|
|
||||||
lp_assert(m_qsol.constraint_count() == 0)
|
|
||||||
vector<unsigned> u;
|
|
||||||
for (unsigned k = 0; k < m_constraints_in_local_vars.size(); k++)
|
|
||||||
u.push_back(k);
|
|
||||||
minimize(u);
|
|
||||||
while (m_qsol.constraint_count() > 0)
|
|
||||||
m_qsol.pop();
|
|
||||||
for (unsigned i : m_x)
|
|
||||||
add_constraint_to_qsol(i);
|
|
||||||
m_qsol.solve();
|
|
||||||
lp_assert(m_qsol.get_status() == lp_status::INFEASIBLE);
|
|
||||||
m_qsol.get_infeasibility_explanation(m_explanation);
|
|
||||||
lp_assert(m_qsol.explanation_is_correct(m_explanation));
|
|
||||||
lp_assert(x_is_minimal());
|
|
||||||
for (auto & p : m_explanation) {
|
|
||||||
p.second = this->m_local_constraint_offset_to_external_ci[m_local_ci_to_constraint_offsets[p.second]];
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
@ -1,48 +0,0 @@
|
||||||
/*++
|
|
||||||
Copyright (c) 2017 Microsoft Corporation
|
|
||||||
|
|
||||||
Module Name:
|
|
||||||
|
|
||||||
<name>
|
|
||||||
|
|
||||||
Abstract:
|
|
||||||
|
|
||||||
<abstract>
|
|
||||||
|
|
||||||
Author:
|
|
||||||
|
|
||||||
Lev Nachmanson (levnach)
|
|
||||||
|
|
||||||
Revision History:
|
|
||||||
|
|
||||||
|
|
||||||
--*/
|
|
||||||
|
|
||||||
#pragma once
|
|
||||||
#include "util/vector.h"
|
|
||||||
#include <unordered_set>
|
|
||||||
|
|
||||||
namespace lp {
|
|
||||||
class lar_solver; // forward definition
|
|
||||||
|
|
||||||
class quick_xplain {
|
|
||||||
std::unordered_set<unsigned> m_x; // the minimal set of constraints, the core - it is empty at the begining
|
|
||||||
vector<lar_constraint> m_constraints_in_local_vars;
|
|
||||||
vector<std::pair<mpq, constraint_index>> & m_explanation;
|
|
||||||
const lar_solver& m_parent_solver;
|
|
||||||
lar_solver & m_qsol;
|
|
||||||
vector<constraint_index> m_local_constraint_offset_to_external_ci;
|
|
||||||
std::unordered_map<constraint_index, unsigned> m_local_ci_to_constraint_offsets;
|
|
||||||
quick_xplain(vector<std::pair<mpq, constraint_index>> & explanation, const lar_solver & parent_lar_solver, lar_solver & qsol);
|
|
||||||
void minimize(const vector<unsigned> & u);
|
|
||||||
void add_constraint_to_qsol(unsigned j);
|
|
||||||
void copy_constraint_and_add_constraint_vars(const lar_constraint& lar_c);
|
|
||||||
void copy_constraints_to_local_constraints();
|
|
||||||
bool infeasible();
|
|
||||||
bool is_feasible(const vector<unsigned> & x, unsigned k) const;
|
|
||||||
bool x_is_minimal() const;
|
|
||||||
public:
|
|
||||||
static void run(vector<std::pair<mpq, constraint_index>> & explanation,const lar_solver & ls);
|
|
||||||
void solve();
|
|
||||||
};
|
|
||||||
}
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue