3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 02:15:19 +00:00
This commit is contained in:
Nikolaj Bjorner 2021-03-19 16:42:45 -07:00
parent 731cf9b885
commit a1f484fa35
6 changed files with 261 additions and 136 deletions

View file

@ -233,8 +233,8 @@ namespace dd {
bdd_manager* m;
bdd(unsigned root, bdd_manager* m): root(root), m(m) { m->inc_ref(root); }
public:
bdd(bdd & other): root(other.root), m(other.m) { m->inc_ref(root); }
bdd(bdd && other): root(0), m(other.m) { std::swap(root, other.root); }
bdd(bdd const & other): root(other.root), m(other.m) { m->inc_ref(root); }
bdd(bdd && other) noexcept : root(0), m(other.m) { std::swap(root, other.root); }
bdd& operator=(bdd const& other);
~bdd() { m->dec_ref(root); }
bdd lo() const { return bdd(m->lo(root), m); }

View file

@ -43,51 +43,157 @@ namespace polysat {
return false;
}
/*
struct del_var;
struct del_constraint;
struct var_unassign;
struct solver::del_var : public trail {
solver& s;
del_var(solver& s): s(s) {}
void undo() override { s.do_del_var(); }
};
void push();
void pop(unsigned n);
struct solver::del_constraint : public trail {
solver& s;
del_constraint(solver& s): s(s) {}
void undo() override { s.do_del_constraint(); }
};
solver(trail_stack& s);
~solver() {}
struct solver::var_unassign : public trail {
solver& s;
var_unassign(solver& s): s(s) {}
void undo() override { s.do_var_unassign(); }
};
solver::solver(trail_stack& s):
m_trail(s),
m_region(s.get_region()),
m_pdd(1000),
m_bdd(1000),
m_free_vars(m_activity) {
}
lbool check_sat();
solver::~solver() {}
lbool solver::check_sat() {
return l_undef;
}
unsigned add_var(unsigned sz);
unsigned solver::add_var(unsigned sz) {
unsigned v = m_viable.size();
// TODO: set var size sz into m_pdd.
m_value.push_back(rational::zero());
m_justification.push_back(justification::unassigned());
m_viable.push_back(m_bdd.mk_true());
m_vdeps.push_back(m_dep_manager.mk_empty());
m_pdeps.push_back(vector<poly>());
m_watch.push_back(unsigned_vector());
m_activity.push_back(0);
m_vars.push_back(m_pdd.mk_var(v));
m_trail.push(del_var(*this));
return v;
}
poly var(unsigned v);
poly mul(rational cons& r, poly const& p);
poly num(rational const& r, unsigned sz);
poly add(poly const& p, poly const& q);
void solver::do_del_var() {
unsigned v = m_viable.size() - 1;
m_free_vars.del_var_eh(v);
m_viable.pop_back();
m_vdeps.pop_back();
m_pdeps.pop_back();
m_value.pop_back();
m_justification.pop_back();
m_watch.pop_back();
m_activity.pop_back();
m_vars.pop_back();
}
vector<mono> poly2monos(poly const& p) const;
void solver::do_del_constraint() {
// TODO remove variables from watch lists
m_constraints.pop_back();
m_cdeps.pop_back();
}
void add_eq(poly const& p, unsigned dep);
void add_diseq(poly const& p, unsigned dep);
void add_ule(poly const& p, poly const& q, unsigned dep);
void add_sle(poly const& p, poly const& q, unsigned dep);
void assign(unsigned var, unsigned index, bool value, unsigned dep);
void solver::do_var_unassign() {
bool can_propagate();
lbool propagate();
}
bool can_decide();
void decide(rational & val, unsigned& var);
void assign(unsigned var, rational const& val);
poly solver::var(unsigned v) {
return poly(*this, m_vars[v]);
}
vector<mono> solver::poly2monos(poly const& p) const {
return vector<mono>();
}
void solver::add_eq(poly const& p, unsigned dep) {
m_constraints.push_back(constraint::eq(p));
m_cdeps.push_back(m_dep_manager.mk_leaf(dep));
// TODO init watch list
m_trail.push(del_constraint(*this));
}
void solver::add_diseq(poly const& p, unsigned dep) {
#if 0
// Basically:
auto slack = add_var(p.size());
p = p + var(slack);
add_eq(p, dep);
m_viable[slack] &= slack != 0;
#endif
}
void solver::add_ule(poly const& p, poly const& q, unsigned dep) {
// save for later
}
void solver::add_sle(poly const& p, poly const& q, unsigned dep) {
// save for later
}
void solver::assign(unsigned var, unsigned index, bool value, unsigned dep) {
}
bool solver::can_propagate() {
return false;
}
lbool solver::propagate() {
return l_false;
}
bool solver::can_decide() {
return false;
}
void solver::decide(rational & val, unsigned& var) {
}
void solver::assign(unsigned var, rational const& val) {
}
bool is_conflict();
unsigned resolve_conflict(unsigned_vector& deps);
bool solver::is_conflict() {
return false;
}
unsigned resolve_conflict(unsigned_vector& deps) {
return 0;
}
bool can_learn();
void learn(constraint& c, unsigned_vector& deps);
void learn(vector<constraint>& cs, unsigned_vector& deps);
bool solver::can_learn() {
return false;
}
std::ostream& display(std::ostream& out) const;
void solver::learn(constraint& c, unsigned_vector& deps) {
}
void solver::learn(vector<constraint>& cs, unsigned_vector& deps) {
}
std::ostream& solver::display(std::ostream& out) const {
return out;
}
*/
}

View file

@ -19,6 +19,7 @@ Author:
#include "util/dependency.h"
#include "util/trail.h"
#include "util/lbool.h"
#include "util/var_queue.h"
#include "math/dd/dd_pdd.h"
#include "math/dd/dd_bdd.h"
@ -29,13 +30,18 @@ namespace polysat {
typedef dd::bdd bdd;
class poly {
friend class solver;
solver& s;
pdd m_pdd;
unsigned m_lidx { UINT_MAX };
public:
poly(solver& s, pdd const& p): s(s), m_pdd(p) {}
poly(solver& s, pdd const& p, unsigned lidx): s(s), m_pdd(p), m_lidx(lidx) {}
poly(solver& s, rational const& r, unsigned sz);
std::ostream& display(std::ostream& out) const;
unsigned size() const { throw default_exception("nyi query pdd for size"); }
poly operator*(rational const& r);
poly operator+(poly const& other) { return poly(s, m_pdd + other.m_pdd); }
poly operator*(poly const& other) { return poly(s, m_pdd * other.m_pdd); }
};
inline std::ostream& operator<<(std::ostream& out, poly const& p) { return p.display(out); }
@ -101,16 +107,20 @@ namespace polysat {
static justification propagation(unsigned idx) { return justification(justification_k::propagation, idx); }
justification_k kind() const { return m_kind; }
unsigned constraint_index() const { return m_idx; }
std::ostream& display(std::ostream& out) const;
};
inline std::ostream& operator<<(std::ostream& out, justification const& j) { return j.display(out); }
class solver {
friend class poly;
trail_stack& m_trail;
region& m_region;
dd::pdd_manager m_pdd;
dd::bdd_manager m_bdd;
u_dependency_manager m_dep_manager;
trail_stack& m_trail;
region& m_region;
dd::pdd_manager m_pdd;
dd::bdd_manager m_bdd;
u_dependency_manager m_dep_manager;
var_queue m_free_vars;
/**
* store of linear polynomials. The l_idx points to linear monomials.
@ -119,16 +129,22 @@ namespace polysat {
vector<linear> m_linear;
// Per constraint state
vector<u_dependency> m_cdeps; // each constraint has set of dependencies
ptr_vector<u_dependency> m_cdeps; // each constraint has set of dependencies
vector<constraint> m_constraints;
// Per variable information
vector<bdd> m_viable; // set of viable values.
vector<u_dependency> m_vdeps; // dependencies for viable values
ptr_vector<u_dependency> m_vdeps; // dependencies for viable values
vector<vector<poly>> m_pdeps; // dependencies in polynomial form
vector<rational> m_value; // assigned value
vector<justification> m_justification; // justification for variable assignment
vector<unsigned_vector> m_watch; // watch list datastructure into constraints.
unsigned_vector m_activity;
vector<pdd> m_vars;
// search state that lists assigned variables
unsigned_vector m_search;
unsigned m_qhead { 0 };
/**
* retrieve bit-size associated with polynomial.
@ -148,11 +164,15 @@ namespace polysat {
struct del_constraint;
struct var_unassign;
void do_del_var();
void do_del_constraint();
void do_var_unassign();
/**
* push / pop are used only in self-contained mode from check_sat.
*/
void push();
void pop(unsigned n);
void push() { m_trail.push_scope(); }
void pop(unsigned n) { m_trail.pop_scope(n); }
public:
@ -162,7 +182,7 @@ namespace polysat {
* by pushing an undo action on the trail stack.
*/
solver(trail_stack& s);
~solver() {}
~solver();
/**
* Self-contained satisfiability checker.
@ -179,9 +199,6 @@ namespace polysat {
* Create polynomial terms
*/
poly var(unsigned v);
poly mul(rational const& r, poly const& p);
poly num(rational const& r, unsigned sz);
poly add(poly const& p, poly const& q);
/**
* deconstruct polynomials into sum of monomials.

View file

@ -19,11 +19,19 @@ Revision History:
#pragma once
#include <cmath>
#include "util/var_queue.h"
#include "util/params.h"
#include "util/statistics.h"
#include "util/stopwatch.h"
#include "util/ema.h"
#include "util/trace.h"
#include "util/rlimit.h"
#include "util/scoped_ptr_vector.h"
#include "util/scoped_limit_trail.h"
#include "sat/sat_types.h"
#include "sat/sat_clause.h"
#include "sat/sat_watched.h"
#include "sat/sat_justification.h"
#include "sat/sat_var_queue.h"
#include "sat/sat_extension.h"
#include "sat/sat_config.h"
#include "sat/sat_cleaner.h"
@ -38,14 +46,6 @@ Revision History:
#include "sat/sat_parallel.h"
#include "sat/sat_local_search.h"
#include "sat/sat_solver_core.h"
#include "util/params.h"
#include "util/statistics.h"
#include "util/stopwatch.h"
#include "util/ema.h"
#include "util/trace.h"
#include "util/rlimit.h"
#include "util/scoped_ptr_vector.h"
#include "util/scoped_limit_trail.h"
namespace pb {
class solver;

View file

@ -1,78 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
sat_var_queue.h
Abstract:
SAT variable priority queue.
Author:
Leonardo de Moura (leonardo) 2011-05-21.
Revision History:
--*/
#pragma once
#include "util/heap.h"
#include "sat/sat_types.h"
namespace sat {
class var_queue {
struct lt {
svector<unsigned> & m_activity;
lt(svector<unsigned> & act):m_activity(act) {}
bool operator()(bool_var v1, bool_var v2) const { return m_activity[v1] > m_activity[v2]; }
};
heap<lt> m_queue;
public:
var_queue(svector<unsigned> & act):m_queue(128, lt(act)) {}
void activity_increased_eh(bool_var v) {
if (m_queue.contains(v))
m_queue.decreased(v);
}
void activity_changed_eh(bool_var v, bool up) {
if (m_queue.contains(v)) {
if (up)
m_queue.decreased(v);
else
m_queue.increased(v);
}
}
void mk_var_eh(bool_var v) {
m_queue.reserve(v+1);
m_queue.insert(v);
}
void del_var_eh(bool_var v) {
if (m_queue.contains(v))
m_queue.erase(v);
}
void unassign_var_eh(bool_var v) {
if (!m_queue.contains(v))
m_queue.insert(v);
}
void reset() {
m_queue.reset();
}
bool empty() const { return m_queue.empty(); }
bool_var next_var() { SASSERT(!empty()); return m_queue.erase_min(); }
bool_var min_var() { SASSERT(!empty()); return m_queue.min_value(); }
bool more_active(bool_var v1, bool_var v2) const { return m_queue.less_than(v1, v2); }
};
};

80
src/util/var_queue.h Normal file
View file

@ -0,0 +1,80 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
var_queue.h
Abstract:
SAT variable priority queue.
Author:
Leonardo de Moura (leonardo) 2011-05-21.
Revision History:
--*/
#pragma once
#include "util/heap.h"
class var_queue {
typedef unsigned var;
struct lt {
svector<unsigned> & m_activity;
lt(svector<unsigned> & act):m_activity(act) {}
bool operator()(var v1, var v2) const { return m_activity[v1] > m_activity[v2]; }
};
heap<lt> m_queue;
public:
var_queue(svector<unsigned> & act):m_queue(128, lt(act)) {}
void activity_increased_eh(var v) {
if (m_queue.contains(v))
m_queue.decreased(v);
}
void activity_changed_eh(var v, bool up) {
if (m_queue.contains(v)) {
if (up)
m_queue.decreased(v);
else
m_queue.increased(v);
}
}
void mk_var_eh(var v) {
m_queue.reserve(v+1);
m_queue.insert(v);
}
void del_var_eh(var v) {
if (m_queue.contains(v))
m_queue.erase(v);
}
void unassign_var_eh(var v) {
if (!m_queue.contains(v))
m_queue.insert(v);
}
void reset() {
m_queue.reset();
}
bool empty() const { return m_queue.empty(); }
var next_var() { SASSERT(!empty()); return m_queue.erase_min(); }
var min_var() { SASSERT(!empty()); return m_queue.min_value(); }
bool more_active(var v1, var v2) const { return m_queue.less_than(v1, v2); }
};