mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 19:05:51 +00:00
Code Activity

include paths

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-08-04 17:08:08 -07:00
parent 1dc8089e6e
commit ec2e9105d3
5 changed files with 33 additions and 43 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/math/bigfix/Hacl_Bignum256.h
View file

@ -29,13 +29,13 @@
extern "C" {
#endif
#include "kremlin/internal/types.h"
#include "kremlin/lowstar_endianness.h"
#include "math/bigfix/internal/types.h"
#include "math/bigfix/kremlin/lowstar_endianness.h"
#include <string.h>
#include "kremlin/internal/target.h"
#include "math/bigfix/kremlin/internal/target.h"
#include "Hacl_Bignum.h"
#include "Hacl_Bignum_Base.h"
#include "math/bigfix/Hacl_Bignum.h"
#include "math/bigfix/Hacl_Bignum_Base.h"
/*******************************************************************************

10
src/math/polysat/fixplex.h
View file

@ -47,7 +47,7 @@ namespace polysat {
virtual void add_le(var_t v, var_t w, unsigned dep) = 0;
virtual void add_lt(var_t v, var_t w, unsigned dep) = 0;
virtual void restore_ineq() = 0;
virtual void get_infeasible_deps(unsigned_vector& deps) = 0;
virtual unsigned_vector const& get_unsat_core() const = 0;
};
@ -160,7 +160,7 @@ namespace polysat {
unsigned m_blands_rule_threshold { 1000 };
random_gen m_random;
uint_set m_left_basis;
unsigned m_infeasible_var { null_var };
unsigned_vector m_unsat_core;
unsigned_vector m_base_vars;
stats m_stats;
vector<stashed_bound> m_stashed_bounds;
@ -211,12 +211,10 @@ namespace polysat {
void add_row(var_t base, unsigned num_vars, var_t const* vars, numeral const* coeffs);
void get_infeasible_deps(unsigned_vector& deps) override;
unsigned_vector const& get_unsat_core() const override { return m_unsat_core; }
private:
row get_infeasible_row();
std::ostream& display_row(std::ostream& out, row const& r, bool values = true);
var_t get_base_var(row const& r) const { return m_rows[r.id()].m_base; }
@ -267,6 +265,8 @@ namespace polysat {
void check_blands_rule(var_t v, unsigned& num_repeated);
pivot_strategy_t pivot_strategy() { return m_bland ? S_BLAND : S_DEFAULT; }
var_t select_error_var(bool least);
void set_infeasible_base(var_t v);
void set_infeasible_bounds(var_t v);
// facilities for handling inequalities
void add_ineq(var_t v, var_t w, unsigned dep, bool strict);

39
src/math/polysat/fixplex_def.h
View file

@ -97,7 +97,7 @@ namespace polysat {
lbool fixplex<Ext>::make_feasible() {
++m_stats.m_num_checks;
m_left_basis.reset();
m_infeasible_var = null_var;
m_unsat_core.reset();
unsigned num_iterations = 0;
unsigned num_repeated = 0;
var_t v = null_var;
@ -114,7 +114,7 @@ namespace polysat {
break;
case l_false:
m_to_patch.insert(v);
m_infeasible_var = v;
set_infeasible_base(v);
++m_stats.m_num_infeasible;
return l_false;
case l_undef:
@ -792,32 +792,22 @@ namespace polysat {
return true;
}
template<typename Ext>
typename fixplex<Ext>::row
fixplex<Ext>::get_infeasible_row() {
SASSERT(is_base(m_infeasible_var));
return base2row(m_infeasible_var);
}
/***
* Extract dependencies for infeasible row.
* A safe approximation is to extract dependencies for all bounds.
*
* Different modes of infeasibility may not be based on a row:
* - inequalities
* - parity constraints between two rows.
* Record an infeasible row.
*/
template<typename Ext>
void fixplex<Ext>::get_infeasible_deps(unsigned_vector& deps) {
auto row = get_infeasible_row();
void fixplex<Ext>::set_infeasible_base(var_t v) {
m_unsat_core.reset();
SASSERT(is_base(v));
auto row = base2row(v);
for (auto const& e : M.row_entries(row)) {
var_t v = e.var();
auto lo = m_vars[v].m_lo_dep;
auto hi = m_vars[v].m_hi_dep;
if (lo != UINT_MAX)
deps.push_back(lo);
m_unsat_core.push_back(lo);
if (hi != UINT_MAX)
deps.push_back(hi);
m_unsat_core.push_back(hi);
}
}
@ -1164,8 +1154,10 @@ namespace polysat {
mod_interval<numeral> r(l, h);
bool was_fixed = lo(x) + 1 == hi(x);
m_vars[x] &= r;
if (m_vars[x].is_empty())
m_infeasible_var = x;
if (m_vars[x].is_empty()) {
// TODO
IF_VERBOSE(0, verbose_stream() << "infeasible\n");
}
else if (!was_fixed && lo(x) + 1 == hi(x)) {
// TBD: track based on inequality not row
// fixed_var_eh(r, x);
@ -1179,8 +1171,9 @@ namespace polysat {
bool was_fixed = lo(x) + 1 == hi(x);
m_vars[x] &= range;
IF_VERBOSE(0, verbose_stream() << "new-bound v" << x << " " << m_vars[x] << "\n");
if (m_vars[x].is_empty())
m_infeasible_var = x;
if (m_vars[x].is_empty()) {
IF_VERBOSE(0, verbose_stream() << "infeasible\n");
}
else if (!was_fixed && lo(x) + 1 == hi(x))
fixed_var_eh(r, x);
}

7
src/math/polysat/linear_solver.cpp
View file

@ -313,15 +313,12 @@ namespace polysat {
SASSERT(m_unsat_f);
deps.reset();
cs.reset();
m_unsat_f->get_infeasible_deps(deps);
unsigned j = 0;
for (unsigned dep : deps) {
for (unsigned dep : m_unsat_f->get_unsat_core()) {
if (is_constraint_dep(dep))
cs.push_back(m_active[dep2constraint_idx(dep)]);
else
deps[j++] = dep2external_dep(dep);
deps.push_back(dep2external_dep(dep));
}
deps.shrink(j);
}
// current value assigned to (linear) variable according to tableau.

10
src/math/polysat/linear_solver.h
View file

@ -111,11 +111,11 @@ namespace polysat {
// unsigned_vector var2mono(unsigned sz, var_t v) { throw default_exception("nyi"); }
// distinguish constraint and justification dependencies
unsigned external_dep2dep(unsigned dep) const { return UINT_MAX - dep; }
unsigned constraint_idx2dep(unsigned idx) const { return idx; }
bool is_constraint_dep(unsigned dep) const { return dep < UINT_MAX / 2; }
unsigned dep2constraint_idx(unsigned dep) const { return dep; }
unsigned dep2external_dep(unsigned dep) const { return UINT_MAX - dep; }
unsigned external_dep2dep(unsigned dep) const { return dep * 2; }
unsigned constraint_idx2dep(unsigned idx) const { return 1 + (idx * 2); }
bool is_constraint_dep(unsigned dep) const { return 0 != (dep & 0x1); }
unsigned dep2constraint_idx(unsigned dep) const { return dep >> 2; }
unsigned dep2external_dep(unsigned dep) const { return dep >> 2; }
public:
linear_solver(solver& s):