mirror of
https://github.com/Z3Prover/z3
synced 2025-04-24 09:35:32 +00:00
Merge branch 'polysat' of https://github.com/Z3Prover/z3 into polysat
This commit is contained in:
Clemens Eisenhofer
commit
2b7fd152c4
34 changed files with 948 additions and 613 deletions
|
|
@ -185,7 +185,20 @@ namespace dd {
|
|||
pdd v_val = mk_var(v) + val;
|
||||
return pdd(apply(s.root, v_val.root, pdd_subst_add_op), this);
|
||||
}
|
||||
|
||||
|
||||
bool pdd_manager::subst_get(pdd const& s, unsigned v, rational& out_val) {
|
||||
unsigned level_v = m_var2level[v];
|
||||
PDD p = s.root;
|
||||
while (/* !is_val(p) && */ level(p) > level_v) {
|
||||
SASSERT(is_val(lo(p)));
|
||||
p = hi(p);
|
||||
}
|
||||
if (!is_val(p) && level(p) == level_v) {
|
||||
out_val = val(lo(p));
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
pdd_manager::PDD pdd_manager::apply(PDD arg1, PDD arg2, pdd_op op) {
|
||||
bool first = true;
|
||||
|
|
|
|||
|
|
@ -10,7 +10,7 @@ Abstract:
|
|||
Poly DD package
|
||||
|
||||
It is a mild variant of ZDDs.
|
||||
In PDDs arithmetic is either standard or using mod 2 (over GF2).
|
||||
In PDDs arithmetic is either standard or using mod 2^n.
|
||||
|
||||
Non-leaf nodes are of the form x*hi + lo
|
||||
where
|
||||
|
|
@ -343,6 +343,7 @@ namespace dd {
|
|||
pdd subst_val(pdd const& a, unsigned v, rational const& val);
|
||||
pdd subst_val(pdd const& a, pdd const& s);
|
||||
pdd subst_add(pdd const& s, unsigned v, rational const& val);
|
||||
bool subst_get(pdd const& s, unsigned v, rational& out_val);
|
||||
bool resolve(unsigned v, pdd const& p, pdd const& q, pdd& r);
|
||||
pdd reduce(unsigned v, pdd const& a, pdd const& b);
|
||||
void quot_rem(pdd const& a, pdd const& b, pdd& q, pdd& r);
|
||||
|
|
@ -459,7 +460,8 @@ namespace dd {
|
|||
pdd subst_val0(vector<std::pair<unsigned, rational>> const& s) const { return m.subst_val0(*this, s); }
|
||||
pdd subst_val(pdd const& s) const { return m.subst_val(*this, s); }
|
||||
pdd subst_val(unsigned v, rational const& val) const { return m.subst_val(*this, v, val); }
|
||||
pdd subst_add(unsigned var, rational const& val) { return m.subst_add(*this, var, val); }
|
||||
pdd subst_add(unsigned var, rational const& val) const { return m.subst_add(*this, var, val); }
|
||||
bool subst_get(unsigned var, rational& out_val) const { return m.subst_get(*this, var, out_val); }
|
||||
|
||||
/**
|
||||
* \brief substitute variable v by r.
|
||||
|
|
|
|||
|
|
@ -1,5 +1,6 @@
|
|||
z3_add_component(polysat
|
||||
SOURCES
|
||||
assignment.cpp
|
||||
boolean.cpp
|
||||
clause.cpp
|
||||
clause_builder.cpp
|
||||
|
|
|
|||
107
src/math/polysat/assignment.cpp
Normal file
107
src/math/polysat/assignment.cpp
Normal file
|
|
@ -0,0 +1,107 @@
|
|||
/*++
|
||||
Copyright (c) 2021 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
polysat substitution and assignment
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2021-03-19
|
||||
Jakob Rath 2021-04-06
|
||||
|
||||
--*/
|
||||
|
||||
#include "math/polysat/assignment.h"
|
||||
#include "math/polysat/solver.h"
|
||||
|
||||
namespace polysat {
|
||||
|
||||
substitution::substitution(pdd p)
|
||||
: m_subst(std::move(p)) { }
|
||||
|
||||
substitution::substitution(dd::pdd_manager& m)
|
||||
: m_subst(m.one()) { }
|
||||
|
||||
substitution substitution::add(pvar var, rational const& value) const {
|
||||
return {m_subst.subst_add(var, value)};
|
||||
}
|
||||
|
||||
pdd substitution::apply_to(pdd const& p) const {
|
||||
return p.subst_val(m_subst);
|
||||
}
|
||||
|
||||
bool substitution::value(pvar var, rational& out_value) const {
|
||||
return m_subst.subst_get(var, out_value);
|
||||
}
|
||||
|
||||
assignment::assignment(solver& s)
|
||||
: m_solver(&s) { }
|
||||
|
||||
assignment assignment::clone() const {
|
||||
assignment a(s());
|
||||
a.m_pairs = m_pairs;
|
||||
a.m_subst.reserve(m_subst.size());
|
||||
for (unsigned i = m_subst.size(); i-- > 0; )
|
||||
if (m_subst[i])
|
||||
a.m_subst.set(i, alloc(substitution, *m_subst[i]));
|
||||
a.m_subst_trail = m_subst_trail;
|
||||
return a;
|
||||
}
|
||||
|
||||
substitution& assignment::subst(unsigned sz) {
|
||||
return const_cast<substitution&>(std::as_const(*this).subst(sz));
|
||||
}
|
||||
|
||||
substitution const& assignment::subst(unsigned sz) const {
|
||||
m_subst.reserve(sz + 1);
|
||||
if (!m_subst[sz])
|
||||
m_subst.set(sz, alloc(substitution, s().sz2pdd(sz)));
|
||||
return *m_subst[sz];
|
||||
}
|
||||
|
||||
void assignment::push(pvar var, rational const& value) {
|
||||
SASSERT(all_of(m_pairs, [var](assignment_item_t const& item) { return item.first != var; }));
|
||||
m_pairs.push_back({var, value});
|
||||
unsigned const sz = s().size(var);
|
||||
substitution& sub = subst(sz);
|
||||
m_subst_trail.push_back(sub);
|
||||
sub = sub.add(var, value);
|
||||
SASSERT_EQ(sub, *m_subst[sz]);
|
||||
}
|
||||
|
||||
void assignment::pop() {
|
||||
substitution& sub = m_subst_trail.back();
|
||||
unsigned sz = sub.bit_width();
|
||||
SASSERT_EQ(sz, s().size(m_pairs.back().first));
|
||||
*m_subst[sz] = sub;
|
||||
m_subst_trail.pop_back();
|
||||
m_pairs.pop_back();
|
||||
}
|
||||
|
||||
pdd assignment::apply_to(pdd const& p) const {
|
||||
unsigned const sz = p.power_of_2();
|
||||
return subst(sz).apply_to(p);
|
||||
}
|
||||
|
||||
std::ostream& substitution::display(std::ostream& out) const {
|
||||
char const* delim = "";
|
||||
pdd p = m_subst;
|
||||
while (!p.is_val()) {
|
||||
SASSERT(p.lo().is_val());
|
||||
out << delim << "v" << p.var() << " := " << p.lo();
|
||||
delim = " ";
|
||||
p = p.hi();
|
||||
}
|
||||
return out;
|
||||
}
|
||||
|
||||
std::ostream& assignment::display(std::ostream& out) const {
|
||||
char const* delim = "";
|
||||
for (auto const& [var, value] : m_pairs) {
|
||||
out << delim << assignment_pp(s(), var, value);
|
||||
delim = " ";
|
||||
}
|
||||
return out;
|
||||
}
|
||||
}
|
||||
114
src/math/polysat/assignment.h
Normal file
114
src/math/polysat/assignment.h
Normal file
|
|
@ -0,0 +1,114 @@
|
|||
/*++
|
||||
Copyright (c) 2021 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
polysat substitution and assignment
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2021-03-19
|
||||
Jakob Rath 2021-04-06
|
||||
|
||||
--*/
|
||||
#pragma once
|
||||
#include "math/polysat/types.h"
|
||||
|
||||
namespace polysat {
|
||||
|
||||
using assignment_item_t = std::pair<pvar, rational>;
|
||||
|
||||
class substitution_iterator {
|
||||
pdd m_current;
|
||||
substitution_iterator(pdd current) : m_current(std::move(current)) {}
|
||||
friend class substitution;
|
||||
|
||||
public:
|
||||
using value_type = assignment_item_t;
|
||||
using difference_type = std::ptrdiff_t;
|
||||
using pointer = value_type const*;
|
||||
using reference = value_type const&;
|
||||
using iterator_category = std::input_iterator_tag;
|
||||
|
||||
substitution_iterator& operator++() {
|
||||
SASSERT(!m_current.is_val());
|
||||
m_current = m_current.hi();
|
||||
return *this;
|
||||
}
|
||||
|
||||
value_type operator*() const {
|
||||
SASSERT(!m_current.is_val());
|
||||
return { m_current.var(), m_current.lo().val() };
|
||||
}
|
||||
|
||||
bool operator==(substitution_iterator const& other) const { return m_current == other.m_current; }
|
||||
bool operator!=(substitution_iterator const& other) const { return !operator==(other); }
|
||||
};
|
||||
|
||||
/** Substitution for a single bit width. */
|
||||
class substitution {
|
||||
pdd m_subst;
|
||||
|
||||
substitution(pdd p);
|
||||
|
||||
public:
|
||||
substitution(dd::pdd_manager& m);
|
||||
substitution add(pvar var, rational const& value) const;
|
||||
pdd apply_to(pdd const& p) const;
|
||||
|
||||
bool value(pvar var, rational& out_value) const;
|
||||
|
||||
bool empty() const { return m_subst.is_one(); }
|
||||
|
||||
pdd const& to_pdd() const { return m_subst; }
|
||||
unsigned bit_width() const { return to_pdd().power_of_2(); }
|
||||
|
||||
bool operator==(substitution const& other) const { return &m_subst.manager() == &other.m_subst.manager() && m_subst == other.m_subst; }
|
||||
bool operator!=(substitution const& other) const { return !operator==(other); }
|
||||
|
||||
std::ostream& display(std::ostream& out) const;
|
||||
|
||||
using const_iterator = substitution_iterator;
|
||||
const_iterator begin() const { return {m_subst}; }
|
||||
const_iterator end() const { return {m_subst.manager().one()}; }
|
||||
};
|
||||
|
||||
/** Full variable assignment, may include variables of varying bit widths. */
|
||||
class assignment {
|
||||
solver* m_solver;
|
||||
vector<assignment_item_t> m_pairs; // TODO: do we still need this?
|
||||
mutable scoped_ptr_vector<substitution> m_subst;
|
||||
vector<substitution> m_subst_trail;
|
||||
|
||||
substitution& subst(unsigned sz);
|
||||
solver& s() const { return *m_solver; }
|
||||
public:
|
||||
assignment(solver& s);
|
||||
// prevent implicit copy, use clone() if you do need a copy
|
||||
assignment(assignment const&) = delete;
|
||||
assignment& operator=(assignment const&) = delete;
|
||||
assignment(assignment&&) = default;
|
||||
assignment& operator=(assignment&&) = default;
|
||||
assignment clone() const;
|
||||
|
||||
void push(pvar var, rational const& value);
|
||||
void pop();
|
||||
|
||||
pdd apply_to(pdd const& p) const;
|
||||
|
||||
bool empty() const { return pairs().empty(); }
|
||||
substitution const& subst(unsigned sz) const;
|
||||
vector<assignment_item_t> const& pairs() const { return m_pairs; }
|
||||
using const_iterator = decltype(m_pairs)::const_iterator;
|
||||
const_iterator begin() const { return pairs().begin(); }
|
||||
const_iterator end() const { return pairs().end(); }
|
||||
|
||||
std::ostream& display(std::ostream& out) const;
|
||||
};
|
||||
|
||||
using assignment_t = assignment;
|
||||
|
||||
inline std::ostream& operator<<(std::ostream& out, substitution const& sub) { return sub.display(out); }
|
||||
|
||||
inline std::ostream& operator<<(std::ostream& out, assignment const& a) { return a.display(out); }
|
||||
}
|
||||
|
|
@ -66,25 +66,25 @@ namespace polysat {
|
|||
}
|
||||
|
||||
void bool_var_manager::propagate(sat::literal lit, unsigned lvl, clause& reason) {
|
||||
LOG("Propagate literal " << lit << " @ " << lvl << " by " << reason);
|
||||
LOG("Propagate " << lit << " @ " << lvl << " by " << reason);
|
||||
assign(kind_t::bool_propagation, lit, lvl, &reason);
|
||||
SASSERT(is_bool_propagation(lit));
|
||||
}
|
||||
|
||||
void bool_var_manager::eval(sat::literal lit, unsigned lvl) {
|
||||
LOG_V("Eval literal " << lit << " @ " << lvl);
|
||||
LOG_V("Evaluate " << lit << " @ " << lvl);
|
||||
assign(kind_t::evaluation, lit, lvl, nullptr);
|
||||
SASSERT(is_evaluation(lit));
|
||||
}
|
||||
|
||||
void bool_var_manager::assumption(sat::literal lit, unsigned lvl, dependency dep) {
|
||||
LOG("Asserted " << lit << " @ " << lvl);
|
||||
LOG("Assert " << lit << " @ " << lvl);
|
||||
assign(kind_t::assumption, lit, lvl, nullptr, dep);
|
||||
SASSERT(is_assumption(lit));
|
||||
}
|
||||
|
||||
void bool_var_manager::decision(sat::literal lit, unsigned lvl) {
|
||||
LOG("Decided " << lit << " @ " << lvl);
|
||||
LOG("Decide " << lit << " @ " << lvl);
|
||||
assign(kind_t::decision, lit, lvl, nullptr);
|
||||
SASSERT(is_decision(lit));
|
||||
}
|
||||
|
|
|
|||
|
|
@ -12,12 +12,9 @@ Author:
|
|||
--*/
|
||||
#pragma once
|
||||
#include "math/polysat/types.h"
|
||||
#include "util/sat_literal.h"
|
||||
|
||||
namespace polysat {
|
||||
|
||||
class clause;
|
||||
|
||||
class bool_var_manager {
|
||||
|
||||
enum class kind_t {
|
||||
|
|
|
|||
|
|
@ -71,8 +71,8 @@ namespace polysat {
|
|||
bool try_resolve_value(pvar v, conflict& core) {
|
||||
if (m_poly_sup.perform(v, core))
|
||||
return true;
|
||||
if (m_saturate.perform(v, core))
|
||||
return true;
|
||||
// if (m_saturate.perform(v, core))
|
||||
// return true;
|
||||
return false;
|
||||
}
|
||||
|
||||
|
|
@ -153,7 +153,6 @@ namespace polysat {
|
|||
SASSERT(m_vars_occurring.empty());
|
||||
SASSERT(m_lemmas.empty());
|
||||
SASSERT(m_narrow_queue.empty());
|
||||
SASSERT_EQ(m_max_jump_level, UINT_MAX);
|
||||
}
|
||||
return is_empty;
|
||||
}
|
||||
|
|
@ -166,7 +165,6 @@ namespace polysat {
|
|||
m_lemmas.reset();
|
||||
m_narrow_queue.reset();
|
||||
m_level = UINT_MAX;
|
||||
m_max_jump_level = UINT_MAX;
|
||||
SASSERT(empty());
|
||||
}
|
||||
|
||||
|
|
@ -209,8 +207,7 @@ namespace polysat {
|
|||
}
|
||||
else {
|
||||
// Constraint c conflicts with the variable assignment
|
||||
// SASSERT(c.bvalue(s) == l_true); // "morally" the bvalue should always be true. But (at least for now) some literals may be undef when they are only justified by a side lemma.
|
||||
// TODO: maybe we can set them to true (without putting them on the search stack). But need to make sure to set them to false when finalizing the conflict; and before backjumping/learning. (tag:true_by_side_lemma)
|
||||
SASSERT_EQ(c.bvalue(s), l_true);
|
||||
SASSERT(c.is_currently_false(s));
|
||||
insert(c);
|
||||
insert_vars(c);
|
||||
|
|
@ -223,7 +220,7 @@ namespace polysat {
|
|||
m_level = s.m_level;
|
||||
for (auto lit : cl) {
|
||||
auto c = s.lit2cnstr(lit);
|
||||
SASSERT(c.bvalue(s) == l_false);
|
||||
SASSERT_EQ(c.bvalue(s), l_false);
|
||||
insert(~c);
|
||||
}
|
||||
SASSERT(!empty());
|
||||
|
|
@ -269,7 +266,7 @@ namespace polysat {
|
|||
if (c.is_always_true())
|
||||
return;
|
||||
LOG("Inserting " << lit_pp(s, c));
|
||||
// SASSERT_EQ(c.bvalue(s), l_true); // TODO: see comment in 'set_impl' (tag:true_by_side_lemma)
|
||||
SASSERT_EQ(c.bvalue(s), l_true);
|
||||
SASSERT(!c.is_always_false()); // if we added c, the core would be a tautology
|
||||
SASSERT(!c->vars().empty());
|
||||
m_literals.insert(c.blit().index());
|
||||
|
|
@ -308,57 +305,20 @@ namespace polysat {
|
|||
void conflict::add_lemma(signed_constraint const* cs, size_t cs_len) {
|
||||
clause_builder cb(s);
|
||||
for (size_t i = 0; i < cs_len; ++i)
|
||||
cb.insert(cs[i]);
|
||||
cb.insert_eval(cs[i]);
|
||||
add_lemma(cb.build());
|
||||
}
|
||||
|
||||
void conflict::add_lemma(clause_ref lemma) {
|
||||
SASSERT(lemma);
|
||||
lemma->set_redundant(true);
|
||||
LOG_H3("Side lemma: " << *lemma);
|
||||
LOG_H3("Lemma: " << *lemma);
|
||||
for (sat::literal lit : *lemma) {
|
||||
LOG(lit_pp(s, lit));
|
||||
SASSERT(s.m_bvars.value(lit) != l_true);
|
||||
}
|
||||
// TODO: call clause simplifier here?
|
||||
// maybe it reduces the level we have to consider.
|
||||
|
||||
// Two kinds of side lemmas:
|
||||
// 1. If all constraints are false, then the side lemma is an alternative conflict lemma.
|
||||
// => we should at least jump back to the second-highest level in the lemma (could be lower, if so justified by another lemma)
|
||||
// 2. If there is an undef constraint, then it is is a justification for this new constraint.
|
||||
// (Can there be more than one undef constraint? Should not happen for these lemmas.)
|
||||
// => TODO: (unclear) jump at least to the max level in the lemma and hope the propagation helps there? or ignore it for jump level computation?
|
||||
unsigned max_level = 0; // highest level in lemma
|
||||
unsigned jump_level = 0; // second-highest level in lemma
|
||||
bool has_unassigned = false;
|
||||
for (sat::literal lit : *lemma) {
|
||||
if (!s.m_bvars.is_assigned(lit)) {
|
||||
has_unassigned = true;
|
||||
continue;
|
||||
}
|
||||
unsigned const lit_level = s.m_bvars.level(lit);
|
||||
if (lit_level > max_level) {
|
||||
jump_level = max_level;
|
||||
max_level = lit_level;
|
||||
} else if (max_level > lit_level && lit_level > jump_level) {
|
||||
jump_level = lit_level;
|
||||
}
|
||||
}
|
||||
if (has_unassigned)
|
||||
jump_level = max_level;
|
||||
LOG("Jump level: " << jump_level);
|
||||
m_max_jump_level = std::min(m_max_jump_level, jump_level);
|
||||
m_lemmas.push_back(std::move(lemma));
|
||||
// If possible, we should set the new constraint to l_true;
|
||||
// and re-enable the assertions marked with "tag:true_by_side_lemma".
|
||||
// Or we adjust the conflict invariant:
|
||||
// - l_true constraints is the default case as before,
|
||||
// - l_undef constraints are new and justified by some side lemma, but
|
||||
// should be treated by the conflict resolution methods like l_true
|
||||
// constraints,
|
||||
// - l_false constraints are disallowed in the conflict (as before).
|
||||
}
|
||||
}
|
||||
|
||||
void conflict::remove(signed_constraint c) {
|
||||
SASSERT(contains(c));
|
||||
|
|
@ -433,27 +393,22 @@ namespace polysat {
|
|||
|
||||
bool conflict::resolve_value(pvar v) {
|
||||
SASSERT(contains_pvar(v));
|
||||
auto const& j = s.m_justification[v];
|
||||
SASSERT(s.m_justification[v].is_propagation());
|
||||
|
||||
s.inc_activity(v);
|
||||
m_vars.remove(v);
|
||||
|
||||
if (j.is_propagation()) {
|
||||
for (auto const& c : s.m_viable.get_constraints(v))
|
||||
insert_eval(c);
|
||||
for (auto const& i : s.m_viable.units(v)) {
|
||||
insert_eval(s.eq(i.lo(), i.lo_val()));
|
||||
insert_eval(s.eq(i.hi(), i.hi_val()));
|
||||
}
|
||||
m_vars.remove(v);
|
||||
for (auto const& c : s.m_viable.get_constraints(v))
|
||||
insert(c);
|
||||
for (auto const& i : s.m_viable.units(v)) {
|
||||
insert(s.eq(i.lo(), i.lo_val()));
|
||||
insert(s.eq(i.hi(), i.hi_val()));
|
||||
}
|
||||
logger().log(inf_resolve_value(s, v));
|
||||
|
||||
if (m_resolver->try_resolve_value(v, *this))
|
||||
return true;
|
||||
|
||||
// Need to keep the variable in case of decision
|
||||
if (s.is_assigned(v) && j.is_decision())
|
||||
m_vars.insert(v);
|
||||
return false;
|
||||
}
|
||||
|
||||
|
|
@ -481,7 +436,7 @@ namespace polysat {
|
|||
return lemma.build();
|
||||
}
|
||||
|
||||
clause_ref_vector conflict::take_side_lemmas() {
|
||||
clause_ref_vector conflict::take_lemmas() {
|
||||
#ifndef NDEBUG
|
||||
on_scope_exit check_empty([this]() {
|
||||
SASSERT(m_lemmas.empty());
|
||||
|
|
@ -542,7 +497,7 @@ namespace polysat {
|
|||
for (auto v : m_vars)
|
||||
out << " v" << v;
|
||||
if (!m_lemmas.empty())
|
||||
out << " side lemmas";
|
||||
out << " lemmas";
|
||||
for (clause const* lemma : m_lemmas)
|
||||
out << " " << show_deref(lemma);
|
||||
return out;
|
||||
|
|
|
|||
|
|
@ -91,11 +91,8 @@ namespace polysat {
|
|||
unsigned_vector m_var_occurrences; // for each variable, the number of constraints in m_literals that contain it
|
||||
uint_set m_vars_occurring; // set of variables that occur in at least one of the constraints in m_literals
|
||||
|
||||
// Additional lemmas that justify new constraints generated during conflict resolution
|
||||
// Lemmas that been accumulated during conflict resolution
|
||||
clause_ref_vector m_lemmas;
|
||||
// The maximal level on which none of the side lemmas is falsified.
|
||||
// (If we backjump to a level higher than max_jump_level, at least one side lemma will be false.)
|
||||
unsigned m_max_jump_level = UINT_MAX;
|
||||
|
||||
// Store constraints that should be narrowed after backjumping.
|
||||
// This allows us to perform propagations that are missed by the two-watched-variables scheme,
|
||||
|
|
@ -189,15 +186,10 @@ namespace polysat {
|
|||
/** Convert the core into a lemma to be learned. */
|
||||
clause_ref build_lemma();
|
||||
|
||||
/** Move the accumulated side lemmas out of the conflict */
|
||||
clause_ref_vector take_side_lemmas();
|
||||
/**
|
||||
* Backjump at least to this level (or possibly to a lower level),
|
||||
* to ensure all side lemmas can be propagated.
|
||||
*/
|
||||
unsigned max_jump_level() const { return m_max_jump_level; }
|
||||
/** Move the accumulated lemmas out of the conflict */
|
||||
clause_ref_vector take_lemmas();
|
||||
|
||||
clause_ref_vector const& side_lemmas() const { return m_lemmas; }
|
||||
clause_ref_vector const& lemmas() const { return m_lemmas; }
|
||||
|
||||
/** Move the literals to be narrowed out of the conflict */
|
||||
sat::literal_vector take_narrow_queue();
|
||||
|
|
|
|||
|
|
@ -24,6 +24,10 @@ Author:
|
|||
|
||||
namespace polysat {
|
||||
|
||||
lbool constraint::eval(solver const& s) const {
|
||||
return eval(s.assignment());
|
||||
}
|
||||
|
||||
bool signed_constraint::is_eq() const {
|
||||
return is_positive() && m_constraint->is_eq();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -15,7 +15,7 @@ Author:
|
|||
#include "math/polysat/boolean.h"
|
||||
#include "math/polysat/types.h"
|
||||
#include "math/polysat/interval.h"
|
||||
#include "math/polysat/search_state.h"
|
||||
#include "math/polysat/assignment.h"
|
||||
#include "math/polysat/univariate/univariate_solver.h"
|
||||
#include <iostream>
|
||||
|
||||
|
|
@ -59,7 +59,6 @@ namespace polysat {
|
|||
ckind_t m_kind;
|
||||
unsigned_vector m_vars;
|
||||
lbool m_external_sign = l_undef;
|
||||
bool m_is_active = false;
|
||||
bool m_is_pwatched = false;
|
||||
/** The boolean variable associated to this constraint */
|
||||
sat::bool_var m_bvar = sat::null_bool_var;
|
||||
|
|
@ -84,12 +83,18 @@ namespace polysat {
|
|||
virtual std::ostream& display(std::ostream& out, lbool status) const = 0;
|
||||
virtual std::ostream& display(std::ostream& out) const = 0;
|
||||
|
||||
virtual bool is_always_false(bool is_positive) const = 0;
|
||||
virtual bool is_currently_false(solver& s, bool is_positive) const = 0;
|
||||
virtual bool is_currently_false(solver& s, assignment_t const& sub, bool is_positive) const = 0;
|
||||
bool is_always_true(bool is_positive) const { return is_always_false(!is_positive); }
|
||||
bool is_currently_true(solver& s, bool is_positive) const { return is_currently_false(s, !is_positive); }
|
||||
bool is_currently_true(solver& s, assignment_t const& sub, bool is_positive) const { return is_currently_false(s, sub, !is_positive); }
|
||||
/** Evaluate the positive-polarity constraint under the empty assignment */
|
||||
virtual lbool eval() const = 0;
|
||||
/** Evaluate the positive-polarity constraint under the given assignment */
|
||||
virtual lbool eval(assignment const& a) const = 0;
|
||||
/** Evaluate the positive-polarity constraint under the solver's current assignment */
|
||||
lbool eval(solver const& s) const;
|
||||
bool is_always_true(bool is_positive) const { return eval() == to_lbool(is_positive); }
|
||||
bool is_always_false(bool is_positive) const { return is_always_true(!is_positive); }
|
||||
bool is_currently_true(assignment const& a, bool is_positive) const { return eval(a) == to_lbool(is_positive); }
|
||||
bool is_currently_false(assignment const& a, bool is_positive) const { return is_currently_true(a, !is_positive); }
|
||||
bool is_currently_true(solver const& s, bool is_positive) const { return eval(s) == to_lbool(is_positive); }
|
||||
bool is_currently_false(solver const& s, bool is_positive) const { return is_currently_true(s, !is_positive); }
|
||||
|
||||
virtual void narrow(solver& s, bool is_positive, bool first) = 0;
|
||||
virtual inequality as_inequality(bool is_positive) const = 0;
|
||||
|
|
@ -114,9 +119,6 @@ namespace polysat {
|
|||
bool is_external() const { return m_external_sign != l_undef; }
|
||||
bool external_sign() const { SASSERT(is_external()); return m_external_sign == l_true; }
|
||||
|
||||
bool is_active() const { return m_is_active; }
|
||||
void set_active(bool f) { m_is_active = f; }
|
||||
|
||||
bool is_pwatched() const { return m_is_pwatched; }
|
||||
void set_pwatched(bool f) { m_is_pwatched = f; }
|
||||
|
||||
|
|
@ -151,12 +153,18 @@ namespace polysat {
|
|||
bool is_positive() const { return m_positive; }
|
||||
bool is_negative() const { return !is_positive(); }
|
||||
|
||||
/** Evaluate the constraint under the empty assignment */
|
||||
lbool eval() const { return is_positive() ? get()->eval() : ~get()->eval(); }
|
||||
/** Evaluate the constraint under the given assignment */
|
||||
lbool eval(assignment const& a) const { return is_positive() ? get()->eval(a) : ~get()->eval(a); }
|
||||
/** Evaluate the constraint under the solver's current assignment */
|
||||
lbool eval(solver const& s) const { return is_positive() ? get()->eval(s) : ~get()->eval(s); }
|
||||
bool is_always_false() const { return get()->is_always_false(is_positive()); }
|
||||
bool is_always_true() const { return get()->is_always_false(is_negative()); }
|
||||
bool is_currently_false(solver& s) const { return get()->is_currently_false(s, is_positive()); }
|
||||
bool is_currently_true(solver& s) const { return get()->is_currently_false(s, is_negative()); }
|
||||
bool is_currently_false(solver& s, assignment_t const& sub) const { return get()->is_currently_false(s, sub, is_positive()); }
|
||||
bool is_currently_true(solver& s, assignment_t const& sub) const { return get()->is_currently_false(s, sub, is_negative()); }
|
||||
bool is_always_true() const { return get()->is_always_true(is_positive()); }
|
||||
bool is_currently_false(assignment const& a) const { return get()->is_currently_false(a, is_positive()); }
|
||||
bool is_currently_true(assignment const& a) const { return get()->is_currently_true(a, is_positive()); }
|
||||
bool is_currently_false(solver const& s) const { return get()->is_currently_false(s, is_positive()); }
|
||||
bool is_currently_true(solver const& s) const { return get()->is_currently_true(s, is_positive()); }
|
||||
lbool bvalue(solver& s) const;
|
||||
void narrow(solver& s, bool first) { get()->narrow(s, is_positive(), first); }
|
||||
inequality as_inequality() const { return get()->as_inequality(is_positive()); }
|
||||
|
|
|
|||
|
|
@ -62,9 +62,11 @@ namespace polysat {
|
|||
|
||||
|
||||
void constraint_manager::register_clause(clause* cl) {
|
||||
while (m_clauses.size() <= s.base_level())
|
||||
unsigned clause_level = s.base_level();
|
||||
clause_level = 0; // TODO: s.base_level() may be too high, if the clause is propagated at an earlier level. For now just use 0.
|
||||
while (m_clauses.size() <= clause_level)
|
||||
m_clauses.push_back({});
|
||||
m_clauses[s.base_level()].push_back(cl);
|
||||
m_clauses[clause_level].push_back(cl);
|
||||
}
|
||||
|
||||
void constraint_manager::store(clause* cl, bool value_propagate) {
|
||||
|
|
@ -276,12 +278,24 @@ namespace polysat {
|
|||
std::pair<pdd, pdd> constraint_manager::quot_rem(pdd const& a, pdd const& b) {
|
||||
auto& m = a.manager();
|
||||
unsigned sz = m.power_of_2();
|
||||
if (a.is_val() && b.is_val()) {
|
||||
rational r;
|
||||
rational q = machine_div_rem(a.val(), b.val(), r);
|
||||
return { m.mk_val(r), m.mk_val(q) };
|
||||
if (b.is_zero()) {
|
||||
// By SMT-LIB specification, b = 0 ==> q = -1, r = a.
|
||||
return {m.mk_val(m.max_value()), a};
|
||||
}
|
||||
if (a.is_val() && b.is_val()) {
|
||||
rational const av = a.val();
|
||||
rational const bv = b.val();
|
||||
SASSERT(!bv.is_zero());
|
||||
rational rv;
|
||||
rational qv = machine_div_rem(av, bv, rv);
|
||||
pdd q = m.mk_val(qv);
|
||||
pdd r = m.mk_val(rv);
|
||||
SASSERT_EQ(a, b * q + r);
|
||||
SASSERT(b.val()*q.val() + r.val() <= m.max_value());
|
||||
SASSERT(r.val() <= (b*q+r).val());
|
||||
SASSERT(r.val() < b.val());
|
||||
return {std::move(q), std::move(r)};
|
||||
}
|
||||
|
||||
constraint_dedup::quot_rem_args args({ a, b });
|
||||
auto it = m_dedup.quot_rem_expr.find_iterator(args);
|
||||
if (it != m_dedup.quot_rem_expr.end())
|
||||
|
|
@ -294,18 +308,27 @@ namespace polysat {
|
|||
// Axioms for quotient/remainder:
|
||||
// a = b*q + r
|
||||
// multiplication does not overflow in b*q
|
||||
// addition does not overflow in (b*q) + r; for now expressed as: r <= bq+r (TODO: maybe the version with disjunction is easier for the solver; should compare later)
|
||||
// addition does not overflow in (b*q) + r; for now expressed as: r <= bq+r
|
||||
// b ≠ 0 ==> r < b
|
||||
// b = 0 ==> q = -1
|
||||
s.add_eq(a, b * q + r);
|
||||
s.add_umul_noovfl(b, q);
|
||||
s.add_ule(r, b * q + r);
|
||||
// r <= b*q+r
|
||||
// { apply equivalence: p <= q <=> q-p <= -p-1 }
|
||||
// b*q <= -r-1
|
||||
s.add_ule(b*q, -r-1);
|
||||
#if 0
|
||||
// b*q <= b*q+r
|
||||
// { apply equivalence: p <= q <=> q-p <= -p-1 }
|
||||
// r <= - b*q - 1
|
||||
s.add_ule(r, -b*q-1); // redundant, but may help propagation
|
||||
#endif
|
||||
|
||||
auto c_eq = eq(b);
|
||||
s.add_clause(c_eq, ult(r, b), false);
|
||||
s.add_clause(~c_eq, eq(q + 1), false);
|
||||
|
||||
return { q, r };
|
||||
return {std::move(q), std::move(r)};
|
||||
}
|
||||
|
||||
pdd constraint_manager::bnot(pdd const& p) {
|
||||
|
|
|
|||
|
|
@ -73,8 +73,8 @@ namespace polysat {
|
|||
out_indent() << assignment_pp(s, v, s.get_value(v)) << "\n";
|
||||
m_used_vars.insert(v);
|
||||
}
|
||||
for (clause* lemma : core.side_lemmas()) {
|
||||
out_indent() << "Side lemma: " << *lemma << "\n";
|
||||
for (clause* lemma : core.lemmas()) {
|
||||
out_indent() << "Lemma: " << *lemma << "\n";
|
||||
for (sat::literal lit : *lemma)
|
||||
out_indent() << " " << lit_pp(s, lit) << "\n";
|
||||
}
|
||||
|
|
|
|||
|
|
@ -51,6 +51,14 @@ namespace polysat {
|
|||
SASSERT(c != code::not_op);
|
||||
}
|
||||
|
||||
lbool op_constraint::eval() const {
|
||||
return eval(p(), q(), r());
|
||||
}
|
||||
|
||||
lbool op_constraint::eval(assignment const& a) const {
|
||||
return eval(a.apply_to(p()), a.apply_to(q()), a.apply_to(r()));
|
||||
}
|
||||
|
||||
lbool op_constraint::eval(pdd const& p, pdd const& q, pdd const& r) const {
|
||||
switch (m_op) {
|
||||
case code::lshr_op:
|
||||
|
|
@ -64,30 +72,6 @@ namespace polysat {
|
|||
}
|
||||
}
|
||||
|
||||
bool op_constraint::is_always_false(bool is_positive, pdd const& p, pdd const& q, pdd const& r) const {
|
||||
switch (eval(p, q, r)) {
|
||||
case l_true: return !is_positive;
|
||||
case l_false: return is_positive;
|
||||
default: return false;
|
||||
}
|
||||
}
|
||||
|
||||
bool op_constraint::is_always_true(bool is_positive, pdd const& p, pdd const& q, pdd const& r) const {
|
||||
return is_always_false(!is_positive, p, q, r);
|
||||
}
|
||||
|
||||
bool op_constraint::is_always_false(bool is_positive) const {
|
||||
return is_always_false(is_positive, p(), q(), r());
|
||||
}
|
||||
|
||||
bool op_constraint::is_currently_false(solver& s, bool is_positive) const {
|
||||
return is_always_false(is_positive, s.subst(p()), s.subst(q()), s.subst(r()));
|
||||
}
|
||||
|
||||
bool op_constraint::is_currently_false(solver& s, assignment_t const& sub, bool is_positive) const {
|
||||
return is_always_false(is_positive, s.subst(sub, p()), s.subst(sub, q()), s.subst(sub, r()));
|
||||
}
|
||||
|
||||
std::ostream& op_constraint::display(std::ostream& out, lbool status) const {
|
||||
switch (status) {
|
||||
case l_true: return display(out);
|
||||
|
|
@ -403,4 +387,5 @@ namespace polysat {
|
|||
break;
|
||||
}
|
||||
}
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -38,9 +38,6 @@ namespace polysat {
|
|||
pdd m_r;
|
||||
|
||||
op_constraint(constraint_manager& m, code c, pdd const& p, pdd const& q, pdd const& r);
|
||||
void simplify() {}
|
||||
bool is_always_false(bool is_positive, pdd const& p, pdd const& q, pdd const& r) const;
|
||||
bool is_always_true(bool is_positive, pdd const& p, pdd const& q, pdd const& r) const;
|
||||
lbool eval(pdd const& p, pdd const& q, pdd const& r) const;
|
||||
|
||||
void narrow_lshr(solver& s);
|
||||
|
|
@ -59,9 +56,8 @@ namespace polysat {
|
|||
pdd const& r() const { return m_r; }
|
||||
std::ostream& display(std::ostream& out, lbool status) const override;
|
||||
std::ostream& display(std::ostream& out) const override;
|
||||
bool is_always_false(bool is_positive) const override;
|
||||
bool is_currently_false(solver& s, bool is_positive) const override;
|
||||
bool is_currently_false(solver& s, assignment_t const& sub, bool is_positive) const override;
|
||||
lbool eval() const override;
|
||||
lbool eval(assignment const& a) const override;
|
||||
void narrow(solver& s, bool is_positive, bool first) override;
|
||||
inequality as_inequality(bool is_positive) const override { throw default_exception("is not an inequality"); }
|
||||
unsigned hash() const override;
|
||||
|
|
|
|||
|
|
@ -8,7 +8,7 @@ Module Name:
|
|||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2021-03-19
|
||||
Jakob Rath 2021-04-6
|
||||
Jakob Rath 2021-04-06
|
||||
|
||||
--*/
|
||||
|
||||
|
|
@ -89,7 +89,7 @@ namespace polysat {
|
|||
std::ostream& search_state::display(std::ostream& out) const {
|
||||
for (auto const& item : m_items)
|
||||
display(item, out) << " ";
|
||||
return out;
|
||||
return out;
|
||||
}
|
||||
|
||||
bool search_state::value(pvar v, rational& val) const {
|
||||
|
|
@ -103,28 +103,7 @@ namespace polysat {
|
|||
|
||||
void search_state::push_assignment(pvar p, rational const& r) {
|
||||
m_items.push_back(search_item::assignment(p));
|
||||
m_assignment.push_back({p, r});
|
||||
unsigned sz = s.size(p);
|
||||
pdd& s = assignment(sz);
|
||||
m_subst_trail.push_back(s);
|
||||
s = s.subst_add(p, r);
|
||||
SASSERT(s == *m_subst[sz]);
|
||||
}
|
||||
|
||||
pdd& search_state::assignment(unsigned sz) const {
|
||||
m_subst.reserve(sz + 1);
|
||||
if (!m_subst[sz])
|
||||
m_subst.set(sz, alloc(pdd, s.sz2pdd(sz).one()));
|
||||
return *m_subst[sz];
|
||||
}
|
||||
|
||||
void search_state::pop_assignment() {
|
||||
m_assignment.pop_back();
|
||||
pdd& s = m_subst_trail.back();
|
||||
auto& m = s.manager();
|
||||
unsigned sz = m.power_of_2();
|
||||
*m_subst[sz] = s;
|
||||
m_subst_trail.pop_back();
|
||||
m_assignment.push(p, r);
|
||||
}
|
||||
|
||||
void search_state::push_boolean(sat::literal lit) {
|
||||
|
|
@ -133,8 +112,10 @@ namespace polysat {
|
|||
|
||||
void search_state::pop() {
|
||||
auto const& item = m_items.back();
|
||||
if (item.is_assignment() && !m_assignment.empty() && item.var() == m_assignment.back().first)
|
||||
pop_assignment();
|
||||
if (item.is_assignment()) {
|
||||
SASSERT_EQ(item.var(), m_assignment.pairs().back().first);
|
||||
m_assignment.pop();
|
||||
}
|
||||
m_items.pop_back();
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -8,20 +8,15 @@ Module Name:
|
|||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2021-03-19
|
||||
Jakob Rath 2021-04-6
|
||||
Jakob Rath 2021-04-06
|
||||
|
||||
--*/
|
||||
#pragma once
|
||||
#include "math/polysat/boolean.h"
|
||||
#include "math/polysat/types.h"
|
||||
#include "math/polysat/assignment.h"
|
||||
|
||||
namespace polysat {
|
||||
|
||||
typedef std::pair<pvar, rational> assignment_item_t;
|
||||
typedef vector<assignment_item_t> assignment_t;
|
||||
|
||||
class solver;
|
||||
|
||||
enum class search_item_k
|
||||
{
|
||||
assignment,
|
||||
|
|
@ -46,7 +41,7 @@ namespace polysat {
|
|||
bool is_resolved() const { return m_resolved; }
|
||||
search_item_k kind() const { return m_kind; }
|
||||
pvar var() const { SASSERT(is_assignment()); return m_var; }
|
||||
sat::literal lit() const { SASSERT(is_boolean()); return m_lit; }
|
||||
sat::literal lit() const { SASSERT(is_boolean()); return m_lit; }
|
||||
void set_resolved() { m_resolved = true; }
|
||||
};
|
||||
|
||||
|
|
@ -54,27 +49,28 @@ namespace polysat {
|
|||
solver& s;
|
||||
|
||||
vector<search_item> m_items;
|
||||
assignment_t m_assignment; // First-order part of the search state
|
||||
mutable scoped_ptr_vector<pdd> m_subst;
|
||||
vector<pdd> m_subst_trail;
|
||||
assignment m_assignment;
|
||||
|
||||
bool value(pvar v, rational& r) const;
|
||||
|
||||
public:
|
||||
search_state(solver& s): s(s) {}
|
||||
search_state(solver& s): s(s), m_assignment(s) {}
|
||||
unsigned size() const { return m_items.size(); }
|
||||
search_item const& back() const { return m_items.back(); }
|
||||
search_item const& operator[](unsigned i) const { return m_items[i]; }
|
||||
|
||||
assignment_t const& assignment() const { return m_assignment; }
|
||||
pdd& assignment(unsigned sz) const;
|
||||
substitution const& subst(unsigned sz) const { return m_assignment.subst(sz); }
|
||||
|
||||
// TODO: implement the following method if we actually need the assignments without resolved items already during conflict resolution
|
||||
// (no separate trail needed, just a second m_subst and an index into the trail, I think)
|
||||
// (update on set_resolved? might be one iteration too early, looking at the old solver::resolve_conflict loop)
|
||||
substitution const& unresolved_assignment(unsigned sz) const;
|
||||
|
||||
void push_assignment(pvar p, rational const& r);
|
||||
void push_boolean(sat::literal lit);
|
||||
void pop();
|
||||
|
||||
void pop_assignment();
|
||||
|
||||
void set_resolved(unsigned i) { m_items[i].set_resolved(); }
|
||||
|
||||
using const_iterator = decltype(m_items)::const_iterator;
|
||||
|
|
@ -106,74 +102,4 @@ namespace polysat {
|
|||
|
||||
inline std::ostream& operator<<(std::ostream& out, search_item_pp const& p) { return p.verbose ? p.s.display_verbose(p.i, out) : p.s.display(p.i, out); }
|
||||
|
||||
// Go backwards over the search_state.
|
||||
// If new entries are added during processing an item, they will be queued for processing next after the current item.
|
||||
class search_iterator {
|
||||
|
||||
search_state* m_search;
|
||||
|
||||
unsigned current;
|
||||
unsigned first; // highest index + 1
|
||||
|
||||
struct idx_range {
|
||||
unsigned current;
|
||||
unsigned first; // highest index + 1
|
||||
};
|
||||
vector<idx_range> m_index_stack;
|
||||
|
||||
void init() {
|
||||
first = m_search->size();
|
||||
current = first; // we start one before the beginning
|
||||
}
|
||||
|
||||
void try_push_block() {
|
||||
if (first != m_search->size()) {
|
||||
m_index_stack.push_back({current, first});
|
||||
init();
|
||||
}
|
||||
}
|
||||
|
||||
void pop_block() {
|
||||
current = m_index_stack.back().current;
|
||||
// We don't restore 'first', otherwise 'next()' will immediately push a new block again.
|
||||
// Instead, the current block is merged with the popped one.
|
||||
m_index_stack.pop_back();
|
||||
}
|
||||
|
||||
unsigned last() {
|
||||
return m_index_stack.empty() ? 0 : m_index_stack.back().first;
|
||||
}
|
||||
|
||||
public:
|
||||
search_iterator(search_state& search):
|
||||
m_search(&search) {
|
||||
init();
|
||||
}
|
||||
|
||||
void set_resolved() {
|
||||
m_search->set_resolved(current);
|
||||
}
|
||||
|
||||
search_item const& operator*() {
|
||||
return (*m_search)[current];
|
||||
}
|
||||
|
||||
bool next() {
|
||||
#if 1 // If you want to resolve over constraints that have been added during conflict resolution, enable this.
|
||||
try_push_block();
|
||||
#endif
|
||||
if (current > last()) {
|
||||
--current;
|
||||
return true;
|
||||
}
|
||||
else {
|
||||
SASSERT(current == last());
|
||||
if (m_index_stack.empty())
|
||||
return false;
|
||||
pop_block();
|
||||
return next();
|
||||
}
|
||||
}
|
||||
};
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -133,9 +133,9 @@ namespace polysat {
|
|||
cl[j++] = cl[i];
|
||||
else {
|
||||
DEBUG_CODE({
|
||||
auto a = s.assignment();
|
||||
a.push_back({v, k});
|
||||
SASSERT(s.lit2cnstr(lit).is_currently_false(s, a));
|
||||
auto a = s.assignment().clone();
|
||||
a.push(v, k);
|
||||
SASSERT(s.lit2cnstr(lit).is_currently_false(a));
|
||||
});
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -40,7 +40,7 @@ namespace polysat {
|
|||
case l_true: return display(out);
|
||||
case l_false: return display(out << "~");
|
||||
case l_undef: return display(out << "?");
|
||||
}
|
||||
}
|
||||
return out;
|
||||
}
|
||||
|
||||
|
|
@ -48,12 +48,12 @@ namespace polysat {
|
|||
if (m_is_overflow)
|
||||
return out << "sovfl*(" << m_p << ", " << m_q << ")";
|
||||
else
|
||||
return out << "sudfl*(" << m_p << ", " << m_q << ")";
|
||||
return out << "sudfl*(" << m_p << ", " << m_q << ")";
|
||||
}
|
||||
|
||||
/**
|
||||
* TODO - verify the rules for small bit-widths.
|
||||
*
|
||||
*
|
||||
* sovfl(p,q) => p >= 2, q >= 2
|
||||
* sovfl(p,q) => p >s 0 <=> q >s 0
|
||||
* sovfl(p,q) & p >s 0 => p*q < 0 or ovfl(p,q)
|
||||
|
|
@ -67,8 +67,8 @@ namespace polysat {
|
|||
* sudfl(p, q) & p >s 0 => p*q > 0 or ovfl(p, -q)
|
||||
* sudfl(p, q) & q >s 0 => p*q > 0 or ovfl(-p, q)
|
||||
*
|
||||
* ~sudfl(p, q) & p >s 0 & q <s 0 => ~ovfl(p, -q) & p*q <s 0
|
||||
* ~sudfl(p, q) & p <s 0 & q >s 0 => ~ovfl(-p, q) & p*q <s 0
|
||||
* ~sudfl(p, q) & p >s 0 & q <s 0 => ~ovfl(p, -q) & p*q <s 0
|
||||
* ~sudfl(p, q) & p <s 0 & q >s 0 => ~ovfl(-p, q) & p*q <s 0
|
||||
*/
|
||||
void smul_fl_constraint::narrow(solver& s, bool is_positive, bool first) {
|
||||
if (!first)
|
||||
|
|
@ -103,8 +103,8 @@ namespace polysat {
|
|||
s.add_clause(sc, ~s.sgt(p(), 0), ~s.slt(q(), 0), s.umul_ovfl(p(), -q()), false);
|
||||
s.add_clause(sc, ~s.sgt(p(), 0), ~s.slt(q(), 0), s.slt(p()*q(), 0), false);
|
||||
s.add_clause(sc, ~s.slt(p(), 0), ~s.sgt(q(), 0), s.umul_ovfl(-p(), q()), false);
|
||||
s.add_clause(sc, ~s.slt(p(), 0), ~s.sgt(q(), 0), s.slt(p()*q(), 0), false);
|
||||
}
|
||||
s.add_clause(sc, ~s.slt(p(), 0), ~s.sgt(q(), 0), s.slt(p()*q(), 0), false);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -26,7 +26,7 @@ namespace polysat {
|
|||
|
||||
void simplify();
|
||||
smul_fl_constraint(constraint_manager& m, pdd const& p, pdd const& q, bool is_overflow);
|
||||
|
||||
|
||||
public:
|
||||
~smul_fl_constraint() override {}
|
||||
bool is_overflow() const { return m_is_overflow; }
|
||||
|
|
@ -34,10 +34,9 @@ namespace polysat {
|
|||
pdd const& q() const { return m_q; }
|
||||
std::ostream& display(std::ostream& out, lbool status) const override;
|
||||
std::ostream& display(std::ostream& out) const override;
|
||||
bool is_always_false(bool is_positive) const override { return false; }
|
||||
lbool eval() const override { return l_undef; } // TODO
|
||||
lbool eval(assignment const& a) const override { return l_undef; } // TODO
|
||||
void narrow(solver& s, bool is_positive, bool first) override;
|
||||
bool is_currently_false(solver & s, bool is_positive) const override { return false; }
|
||||
bool is_currently_false(solver& s, assignment_t const& sub, bool is_positive) const override { return false; }
|
||||
|
||||
inequality as_inequality(bool is_positive) const override { throw default_exception("is not an inequality"); }
|
||||
unsigned hash() const override;
|
||||
|
|
|
|||
|
|
@ -97,7 +97,7 @@ namespace polysat {
|
|||
return *m_pdd[sz];
|
||||
}
|
||||
|
||||
dd::pdd_manager& solver::var2pdd(pvar v) {
|
||||
dd::pdd_manager& solver::var2pdd(pvar v) const {
|
||||
return sz2pdd(size(v));
|
||||
}
|
||||
|
||||
|
|
@ -202,16 +202,12 @@ namespace polysat {
|
|||
}
|
||||
|
||||
/**
|
||||
* Propagate assignment to a Boolean variable
|
||||
*/
|
||||
* Propagate assignment to a Boolean variable
|
||||
*/
|
||||
void solver::propagate(sat::literal lit) {
|
||||
LOG_H2("Propagate bool " << lit << "@" << m_bvars.level(lit) << " " << m_level << " qhead: " << m_qhead);
|
||||
LOG("Literal " << lit_pp(*this, lit));
|
||||
signed_constraint c = lit2cnstr(lit);
|
||||
SASSERT(c);
|
||||
// TODO: review active and activate_constraint
|
||||
if (c->is_active())
|
||||
return;
|
||||
activate_constraint(c);
|
||||
auto& wlist = m_bvars.watch(~lit);
|
||||
unsigned i = 0, j = 0, sz = wlist.size();
|
||||
|
|
@ -224,8 +220,8 @@ namespace polysat {
|
|||
}
|
||||
|
||||
/**
|
||||
* Propagate assignment to a pvar
|
||||
*/
|
||||
* Propagate assignment to a pvar
|
||||
*/
|
||||
void solver::propagate(pvar v) {
|
||||
LOG_H2("Propagate " << assignment_pp(*this, v, get_value(v)));
|
||||
SASSERT(!m_locked_wlist);
|
||||
|
|
@ -262,11 +258,9 @@ namespace polysat {
|
|||
return true;
|
||||
}
|
||||
}
|
||||
// at most one poly variable remains unassigned.
|
||||
// at most one pvar remains unassigned
|
||||
if (m_bvars.is_assigned(c->bvar())) {
|
||||
// constraint state: bool-propagated
|
||||
// // constraint is active, propagate it
|
||||
// SASSERT(c->is_active()); // TODO: what exactly does 'active' mean now ... use 'pwatched' and similar instead, to make meaning explicit?
|
||||
signed_constraint sc(c, m_bvars.value(c->bvar()) == l_true);
|
||||
if (c->vars().size() >= 2) {
|
||||
unsigned other_v = c->var(1 - idx);
|
||||
|
|
@ -275,9 +269,7 @@ namespace polysat {
|
|||
}
|
||||
sc.narrow(*this, false);
|
||||
} else {
|
||||
// constraint state: active but unassigned (bvalue undef, but pwatch is set and active; e.g., new constraints generated for lemmas)
|
||||
// // constraint is not yet active, try to evaluate it
|
||||
// SASSERT(!c->is_active());
|
||||
// constraint state: active but unassigned (bvalue undef, but pwatch is set; e.g., new constraints generated for lemmas)
|
||||
if (c->vars().size() >= 2) {
|
||||
unsigned other_v = c->var(1 - idx);
|
||||
// Wait for the remaining variable to be assigned
|
||||
|
|
@ -423,7 +415,6 @@ namespace polysat {
|
|||
case trail_instr_t::pwatch_i: {
|
||||
constraint* c = m_pwatch_trail.back();
|
||||
erase_pwatch(c);
|
||||
c->set_active(false); // TODO: review meaning of "active"
|
||||
m_pwatch_trail.pop_back();
|
||||
break;
|
||||
}
|
||||
|
|
@ -471,13 +462,9 @@ namespace polysat {
|
|||
}
|
||||
case trail_instr_t::assign_bool_i: {
|
||||
sat::literal lit = m_search.back().lit();
|
||||
signed_constraint c = lit2cnstr(lit);
|
||||
LOG_V("Undo assign_bool_i: " << lit);
|
||||
unsigned active_level = m_bvars.level(lit);
|
||||
|
||||
if (c->is_active())
|
||||
deactivate_constraint(c);
|
||||
|
||||
if (active_level <= target_level)
|
||||
replay.push_back(lit);
|
||||
else
|
||||
|
|
@ -509,6 +496,15 @@ namespace polysat {
|
|||
// when substituting polynomials, it will now take into account the replayed variables, which may itself depend on previous propagations.
|
||||
// will we get into trouble with cyclic dependencies?
|
||||
// But we do want to take into account variables that are assigned but not yet propagated.
|
||||
// Possible solutions:
|
||||
// - keep the replay queue outside of this method?
|
||||
// prioritize putting stuff on the stack from the replay queue.
|
||||
// this might however introduce new propagations in between? maybe that is ok?
|
||||
// - when evaluating/narrowing instead of passing the full assignment,
|
||||
// we pass a "dependency level" which is basically an index into the search stack.
|
||||
// then we get an assignment up to that dependency level.
|
||||
// each literal can only depend on entries with lower dependency level
|
||||
// (that is the invariant that propagations are justified by a prefix of the search stack.)
|
||||
}
|
||||
else
|
||||
static_assert(always_false<T>::value, "non-exhaustive visitor");
|
||||
|
|
@ -531,7 +527,6 @@ namespace polysat {
|
|||
void solver::decide() {
|
||||
LOG_H2("Decide");
|
||||
SASSERT(can_decide());
|
||||
SASSERT(can_pdecide()); // if !can_pdecide(), all boolean literals have been propagated...
|
||||
if (can_bdecide())
|
||||
bdecide();
|
||||
else
|
||||
|
|
@ -546,11 +541,17 @@ namespace polysat {
|
|||
};
|
||||
|
||||
LOG_H2("Decide on non-asserting lemma: " << lemma);
|
||||
for (sat::literal lit : lemma) {
|
||||
LOG(lit_pp(*this, lit));
|
||||
}
|
||||
sat::literal choice = sat::null_literal;
|
||||
for (sat::literal lit : lemma) {
|
||||
switch (m_bvars.value(lit)) {
|
||||
case l_true:
|
||||
// Clause is satisfied; nothing to do here
|
||||
// Happens when all other branches of the lemma have been tried.
|
||||
// The last branch is entered due to propagation, while the lemma is still on the stack as a decision point.
|
||||
LOG("Skip decision (clause already satisfied)");
|
||||
return;
|
||||
case l_false:
|
||||
break;
|
||||
|
|
@ -561,10 +562,9 @@ namespace polysat {
|
|||
}
|
||||
}
|
||||
LOG("Choice is " << lit_pp(*this, choice));
|
||||
// SASSERT(2 <= count_if(lemma, [this](sat::literal lit) { return !m_bvars.is_assigned(lit); });
|
||||
SASSERT(choice != sat::null_literal);
|
||||
// TODO: is the case after backtracking correct?
|
||||
// => the backtracking code has to handle this. making sure that the decision literal is set to false.
|
||||
SASSERT(2 <= count_if(lemma, [this](sat::literal lit) { return !m_bvars.is_assigned(lit); }));
|
||||
SASSERT(can_pdecide()); // if !can_pdecide(), all boolean literals have been evaluated
|
||||
push_level();
|
||||
assign_decision(choice);
|
||||
}
|
||||
|
|
@ -693,26 +693,32 @@ namespace polysat {
|
|||
|
||||
SASSERT(is_conflict());
|
||||
|
||||
search_iterator search_it(m_search);
|
||||
while (search_it.next()) {
|
||||
auto& item = *search_it;
|
||||
search_it.set_resolved();
|
||||
for (unsigned i = m_search.size(); i-- > 0; ) {
|
||||
auto& item = m_search[i];
|
||||
m_search.set_resolved(i);
|
||||
if (item.is_assignment()) {
|
||||
// Resolve over variable assignment
|
||||
pvar v = item.var();
|
||||
if (!m_conflict.is_relevant_pvar(v)) {
|
||||
m_search.pop_assignment();
|
||||
continue;
|
||||
}
|
||||
LOG_H2("Working on " << search_item_pp(m_search, item));
|
||||
LOG(m_justification[v]);
|
||||
LOG("Conflict: " << m_conflict);
|
||||
justification& j = m_justification[v];
|
||||
if (j.level() > base_level() && !m_conflict.resolve_value(v) && j.is_decision()) {
|
||||
justification const& j = m_justification[v];
|
||||
// NOTE: propagation level may be out of order (cf. replay), but decisions are always in order
|
||||
if (j.level() <= base_level()) {
|
||||
if (j.is_decision()) {
|
||||
report_unsat();
|
||||
return;
|
||||
}
|
||||
continue;
|
||||
}
|
||||
if (j.is_decision()) {
|
||||
revert_decision(v);
|
||||
return;
|
||||
}
|
||||
m_search.pop_assignment();
|
||||
m_conflict.resolve_value(v);
|
||||
}
|
||||
else {
|
||||
// Resolve over boolean literal
|
||||
|
|
@ -725,9 +731,13 @@ namespace polysat {
|
|||
LOG(bool_justification_pp(m_bvars, lit));
|
||||
LOG("Literal " << lit << " is " << lit2cnstr(lit));
|
||||
LOG("Conflict: " << m_conflict);
|
||||
// NOTE: the levels of boolean literals on the stack aren't always ordered by level (cf. replay functionality in pop_levels).
|
||||
// Thus we can only skip base level literals here, instead of aborting the loop.
|
||||
if (m_bvars.level(var) <= base_level()) {
|
||||
// NOTE: the levels of boolean literals on the stack aren't always ordered by level (cf. replay functionality in pop_levels).
|
||||
// Thus we can only skip base level literals here, instead of aborting the loop.
|
||||
if (m_bvars.is_decision(var)) {
|
||||
report_unsat(); // decisions are always in order
|
||||
return;
|
||||
}
|
||||
continue;
|
||||
}
|
||||
SASSERT(!m_bvars.is_assumption(var));
|
||||
|
|
@ -736,11 +746,11 @@ namespace polysat {
|
|||
return;
|
||||
}
|
||||
if (m_bvars.is_bool_propagation(var))
|
||||
// TODO: this could be a propagation at an earlier level.
|
||||
// do we really want to resolve these eagerly?
|
||||
m_conflict.resolve_bool(lit, *m_bvars.reason(lit));
|
||||
else {
|
||||
SASSERT(m_bvars.is_evaluation(var));
|
||||
else
|
||||
m_conflict.resolve_with_assignment(lit);
|
||||
}
|
||||
}
|
||||
}
|
||||
LOG("End of resolve_conflict loop");
|
||||
|
|
@ -791,6 +801,7 @@ namespace polysat {
|
|||
*
|
||||
*/
|
||||
void solver::revert_decision(pvar v) {
|
||||
#if 0
|
||||
rational val = m_value[v];
|
||||
LOG_H2("Reverting decision: pvar " << v << " := " << val);
|
||||
SASSERT(m_justification[v].is_decision());
|
||||
|
|
@ -805,9 +816,13 @@ namespace polysat {
|
|||
|
||||
unsigned jump_level = get_level(v) - 1;
|
||||
backjump_and_learn(jump_level, *lemma);
|
||||
#endif
|
||||
unsigned max_jump_level = get_level(v) - 1;
|
||||
backjump_and_learn(max_jump_level);
|
||||
}
|
||||
|
||||
void solver::revert_bool_decision(sat::literal const lit) {
|
||||
#if 0
|
||||
LOG_H2("Reverting decision: " << lit_pp(*this, lit));
|
||||
sat::bool_var const var = lit.var();
|
||||
|
||||
|
|
@ -830,29 +845,149 @@ namespace polysat {
|
|||
// If there is more than one undef choice left in that lemma,
|
||||
// then the next bdecide will take care of that (after all outstanding propagations).
|
||||
SASSERT(can_bdecide());
|
||||
#endif
|
||||
unsigned max_jump_level = m_bvars.level(lit) - 1;
|
||||
backjump_and_learn(max_jump_level);
|
||||
}
|
||||
|
||||
void solver::backjump_and_learn(unsigned jump_level, clause& lemma) {
|
||||
#ifndef NDEBUG
|
||||
assignment_t old_assignment;
|
||||
// We can't use solver::assignment() here because we already used search_sate::pop_assignment().
|
||||
// TODO: fix search_state design; it should show a consistent state.
|
||||
search_iterator search_it(m_search);
|
||||
while (search_it.next()) {
|
||||
auto& item = *search_it;
|
||||
if (item.is_assignment()) {
|
||||
pvar v = item.var();
|
||||
old_assignment.push_back({v, get_value(v)});
|
||||
std::optional<lemma_score> solver::compute_lemma_score(clause const& lemma) {
|
||||
unsigned max_level = 0; // highest level in lemma
|
||||
unsigned at_max_level = 0; // how many literals at the highest level in lemma
|
||||
unsigned snd_level = 0; // second-highest level in lemma
|
||||
for (sat::literal lit : lemma) {
|
||||
SASSERT(m_bvars.is_assigned(lit)); // any new constraints should have been assign_eval'd
|
||||
if (m_bvars.is_true(lit)) // may happen if we only use the clause to justify a new constraint; it is not a real lemma
|
||||
return std::nullopt;
|
||||
|
||||
unsigned const lit_level = m_bvars.level(lit);
|
||||
if (lit_level > max_level) {
|
||||
snd_level = max_level;
|
||||
max_level = lit_level;
|
||||
at_max_level = 1;
|
||||
} else if (lit_level == max_level) {
|
||||
at_max_level++;
|
||||
} else if (max_level > lit_level && lit_level > snd_level) {
|
||||
snd_level = lit_level;
|
||||
}
|
||||
}
|
||||
sat::literal_vector lemma_invariant_todo;
|
||||
SASSERT(lemma_invariant_part1(lemma, old_assignment, lemma_invariant_todo));
|
||||
// SASSERT(lemma_invariant(lemma, old_assignment));
|
||||
#endif
|
||||
clause_ref_vector side_lemmas = m_conflict.take_side_lemmas();
|
||||
SASSERT(lemma.empty() || at_max_level > 0);
|
||||
// The MCSAT paper distinguishes between "UIP clauses" and "semantic split clauses".
|
||||
// It is the same as our distinction between "asserting" and "non-asserting" lemmas.
|
||||
// - UIP clause: a single literal on the highest decision level in the lemma.
|
||||
// Do the standard backjumping known from SAT solving (back to second-highest level in the lemma, propagate it there).
|
||||
// - Semantic split clause: multiple literals on the highest level in the lemma.
|
||||
// Backtrack to "highest level - 1" and split on the lemma there.
|
||||
// For now, we follow the same convention for computing the jump levels.
|
||||
unsigned jump_level;
|
||||
if (at_max_level <= 1)
|
||||
jump_level = snd_level;
|
||||
else
|
||||
jump_level = (max_level == 0) ? 0 : (max_level - 1);
|
||||
return {{jump_level, at_max_level}};
|
||||
}
|
||||
|
||||
void solver::backjump_and_learn(unsigned max_jump_level) {
|
||||
sat::literal_vector narrow_queue = m_conflict.take_narrow_queue();
|
||||
clause_ref_vector lemmas = m_conflict.take_lemmas();
|
||||
|
||||
// Select the "best" lemma
|
||||
// - lowest jump level
|
||||
// - lowest number of literals at the highest level
|
||||
// We must do so before backjump() when the search stack is still intact.
|
||||
lemma_score best_score = lemma_score::max();
|
||||
clause* best_lemma = nullptr;
|
||||
|
||||
auto appraise_lemma = [&](clause* lemma) {
|
||||
m_simplify_clause.apply(*lemma);
|
||||
auto score = compute_lemma_score(*lemma);
|
||||
if (score && *score < best_score) {
|
||||
best_score = *score;
|
||||
best_lemma = lemma;
|
||||
}
|
||||
};
|
||||
|
||||
for (clause* lemma : lemmas)
|
||||
appraise_lemma(lemma);
|
||||
if (!best_lemma || best_score.jump_level() > max_jump_level) {
|
||||
// No (good) lemma has been found, so build the fallback lemma from the conflict state.
|
||||
lemmas.push_back(m_conflict.build_lemma());
|
||||
appraise_lemma(lemmas.back());
|
||||
}
|
||||
SASSERT(best_score < lemma_score::max());
|
||||
SASSERT(best_lemma);
|
||||
|
||||
unsigned const jump_level = best_score.jump_level();
|
||||
SASSERT(jump_level <= max_jump_level);
|
||||
|
||||
m_conflict.reset();
|
||||
backjump(jump_level);
|
||||
|
||||
for (sat::literal lit : narrow_queue) {
|
||||
LOG("Narrow queue: " << lit_pp(*this, lit));
|
||||
switch (m_bvars.value(lit)) {
|
||||
case l_true:
|
||||
lit2cnstr(lit).narrow(*this, false);
|
||||
break;
|
||||
case l_false:
|
||||
lit2cnstr(~lit).narrow(*this, false);
|
||||
break;
|
||||
case l_undef:
|
||||
/* do nothing */
|
||||
break;
|
||||
default:
|
||||
UNREACHABLE();
|
||||
}
|
||||
}
|
||||
|
||||
for (clause* lemma : lemmas) {
|
||||
add_clause(*lemma);
|
||||
// NOTE: currently, the backjump level is an overapproximation,
|
||||
// since the level of evaluated constraints may not be exact (see TODO in assign_eval).
|
||||
// For this reason, we may actually get a conflict at this point
|
||||
// (because the actual jump_level of the lemma may be lower that best_level.)
|
||||
if (is_conflict()) {
|
||||
// until this is fixed (if possible; and there may be other causes of conflict at this point),
|
||||
// we just forget about the remaining lemmas and restart conflict analysis.
|
||||
return;
|
||||
}
|
||||
SASSERT(!is_conflict()); // TODO: is this true in general? No lemma by itself should lead to a conflict here. But can there be conflicting asserting lemmas?
|
||||
}
|
||||
|
||||
LOG("best_score: " << best_score);
|
||||
LOG("best_lemma: " << *best_lemma);
|
||||
|
||||
if (best_score.literals_at_max_level() > 1) {
|
||||
// NOTE: at this point it is possible that the best_lemma is non-asserting.
|
||||
// We need to double-check, because the backjump level may not be exact (see comment on checking is_conflict above).
|
||||
bool const is_asserting = all_of(*best_lemma, [this](sat::literal lit) { return m_bvars.is_assigned(lit); });
|
||||
if (!is_asserting) {
|
||||
LOG_H3("Main lemma is not asserting: " << *best_lemma);
|
||||
for (sat::literal lit : *best_lemma) {
|
||||
LOG(lit_pp(*this, lit));
|
||||
}
|
||||
m_lemmas.push_back(best_lemma);
|
||||
m_trail.push_back(trail_instr_t::add_lemma_i);
|
||||
// TODO: currently we forget non-asserting lemmas when backjumping over them.
|
||||
// We surely don't want to keep them in m_lemmas because then we will start doing case splits
|
||||
// even if the lemma should instead be waiting for propagations.
|
||||
// We could instead watch its pvars and re-insert into m_lemmas when all but one are assigned.
|
||||
// The same could even be done in general for all lemmas, instead of distinguishing between
|
||||
// asserting and non-asserting lemmas.
|
||||
// (Note that the same lemma can be asserting in one branch of the search but non-asserting in another,
|
||||
// depending on which pvars are assigned.)
|
||||
SASSERT(can_bdecide());
|
||||
}
|
||||
}
|
||||
} // backjump_and_learn
|
||||
|
||||
#if 0
|
||||
void solver::backjump_and_learn(unsigned jump_level, clause& lemma) {
|
||||
clause_ref_vector lemmas = m_conflict.take_lemmas();
|
||||
sat::literal_vector narrow_queue = m_conflict.take_narrow_queue();
|
||||
|
||||
m_conflict.reset();
|
||||
backjump(jump_level);
|
||||
|
||||
for (sat::literal lit : narrow_queue) {
|
||||
switch (m_bvars.value(lit)) {
|
||||
case l_true:
|
||||
|
|
@ -868,14 +1003,15 @@ namespace polysat {
|
|||
UNREACHABLE();
|
||||
}
|
||||
}
|
||||
for (auto cl : side_lemmas) {
|
||||
for (clause* cl : lemmas) {
|
||||
m_simplify_clause.apply(*cl);
|
||||
add_clause(*cl);
|
||||
}
|
||||
SASSERT(lemma_invariant_part2(lemma_invariant_todo));
|
||||
learn_lemma(lemma);
|
||||
}
|
||||
#endif
|
||||
|
||||
#if 0
|
||||
void solver::learn_lemma(clause& lemma) {
|
||||
SASSERT(!lemma.empty());
|
||||
m_simplify_clause.apply(lemma);
|
||||
|
|
@ -898,41 +1034,7 @@ namespace polysat {
|
|||
SASSERT(can_bdecide());
|
||||
}
|
||||
}
|
||||
|
||||
bool solver::lemma_invariant_part1(clause const& lemma, assignment_t const& assignment, sat::literal_vector& out_todo) {
|
||||
SASSERT(out_todo.empty());
|
||||
LOG("Lemma: " << lemma);
|
||||
// LOG("assignment: " << assignment);
|
||||
for (sat::literal lit : lemma) {
|
||||
auto const c = lit2cnstr(lit);
|
||||
bool const currently_false = c.is_currently_false(*this, assignment);
|
||||
LOG(" " << lit_pp(*this, lit) << " currently_false? " << currently_false);
|
||||
if (!currently_false && m_bvars.value(lit) == l_undef)
|
||||
out_todo.push_back(lit); // undefs might only be set false after the side lemmas are propagated, so check them later.
|
||||
else
|
||||
SASSERT(m_bvars.value(lit) == l_false || currently_false);
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
bool solver::lemma_invariant_part2(sat::literal_vector const& todo) {
|
||||
// Check that undef literals are now propagated by the side lemmas.
|
||||
for (sat::literal lit : todo)
|
||||
SASSERT(m_bvars.value(lit) == l_false);
|
||||
return true;
|
||||
}
|
||||
|
||||
bool solver::lemma_invariant(clause const& lemma, assignment_t const& old_assignment) {
|
||||
LOG("Lemma: " << lemma);
|
||||
// LOG("old_assignment: " << old_assignment);
|
||||
for (sat::literal lit : lemma) {
|
||||
auto const c = lit2cnstr(lit);
|
||||
bool const currently_false = c.is_currently_false(*this, old_assignment);
|
||||
LOG(" " << lit_pp(*this, lit) << " currently_false? " << currently_false);
|
||||
SASSERT(m_bvars.value(lit) == l_false || currently_false);
|
||||
}
|
||||
return true;
|
||||
}
|
||||
#endif
|
||||
|
||||
unsigned solver::level(sat::literal lit0, clause const& cl) {
|
||||
unsigned lvl = 0;
|
||||
|
|
@ -958,19 +1060,34 @@ namespace polysat {
|
|||
}
|
||||
|
||||
void solver::assign_eval(sat::literal lit) {
|
||||
// SASSERT(lit2cnstr(lit).is_currently_true(*this)); // "morally" this should hold, but currently fails because of pop_assignment during resolve_conflict
|
||||
SASSERT(!lit2cnstr(lit).is_currently_false(*this));
|
||||
signed_constraint const c = lit2cnstr(lit);
|
||||
SASSERT(c.is_currently_true(*this));
|
||||
unsigned level = 0;
|
||||
// NOTE: constraint may be evaluated even if some variables are still unassigned (e.g., 0*x doesn't depend on x).
|
||||
// TODO: level might be too low! because pop_assignment may already have removed necessary variables (cf. comment on assertion above).
|
||||
for (auto v : lit2cnstr(lit)->vars())
|
||||
for (auto v : c->vars())
|
||||
if (is_assigned(v))
|
||||
level = std::max(get_level(v), level);
|
||||
// TODO: the level computed here is not exact, because evaluation of constraints may not depend on all variables that occur in the constraint.
|
||||
// For example, consider x := 0 @ 1 and y := 0 @ 3. Then x*y == 0 eval@3, even though we can already evaluate it at level 1.
|
||||
// To get the exact level:
|
||||
// - consider the levels get_level(var) for var in c->vars().
|
||||
// - the maximum of these is the estimate we start with (and which we currently use)
|
||||
// - successively reduce the level, as long as the constraint still evaluates
|
||||
m_bvars.eval(lit, level);
|
||||
m_trail.push_back(trail_instr_t::assign_bool_i);
|
||||
m_search.push_boolean(lit);
|
||||
}
|
||||
|
||||
/** Push c onto \Gamma, unless it is already true. */
|
||||
void solver::try_assign_eval(signed_constraint c) {
|
||||
sat::literal const lit = c.blit();
|
||||
if (m_bvars.is_assigned(lit))
|
||||
return;
|
||||
if (c.is_always_true())
|
||||
return;
|
||||
assign_eval(lit);
|
||||
}
|
||||
|
||||
/**
|
||||
* Activate constraint immediately
|
||||
* Activation and de-activation of constraints follows the scope controlled by push/pop.
|
||||
|
|
@ -980,9 +1097,7 @@ namespace polysat {
|
|||
void solver::activate_constraint(signed_constraint c) {
|
||||
SASSERT(c);
|
||||
LOG("Activating constraint: " << c);
|
||||
SASSERT(m_bvars.value(c.blit()) == l_true);
|
||||
SASSERT(!c->is_active());
|
||||
c->set_active(true);
|
||||
SASSERT_EQ(m_bvars.value(c.blit()), l_true);
|
||||
add_pwatch(c.get());
|
||||
if (c->vars().size() == 1)
|
||||
m_viable_fallback.push_constraint(c->var(0), c);
|
||||
|
|
@ -992,12 +1107,6 @@ namespace polysat {
|
|||
#endif
|
||||
}
|
||||
|
||||
/// Deactivate constraint
|
||||
void solver::deactivate_constraint(signed_constraint c) {
|
||||
LOG_V("Deactivating constraint: " << c.blit());
|
||||
c->set_active(false);
|
||||
}
|
||||
|
||||
void solver::backjump(unsigned new_level) {
|
||||
if (m_level != new_level) {
|
||||
LOG_H3("Backjumping to level " << new_level << " from level " << m_level);
|
||||
|
|
@ -1172,9 +1281,7 @@ namespace polysat {
|
|||
}
|
||||
|
||||
std::ostream& assignments_pp::display(std::ostream& out) const {
|
||||
for (auto const& [var, val] : s.assignment())
|
||||
out << assignment_pp(s, var, val) << " ";
|
||||
return out;
|
||||
return out << s.assignment();
|
||||
}
|
||||
|
||||
std::ostream& assignment_pp::display(std::ostream& out) const {
|
||||
|
|
@ -1204,8 +1311,6 @@ namespace polysat {
|
|||
}
|
||||
if (c->is_pwatched())
|
||||
out << " pwatched";
|
||||
if (c->is_active())
|
||||
out << " active";
|
||||
if (c->is_external())
|
||||
out << " ext";
|
||||
out << " ]";
|
||||
|
|
@ -1284,18 +1389,7 @@ namespace polysat {
|
|||
}
|
||||
|
||||
pdd solver::subst(pdd const& p) const {
|
||||
unsigned sz = p.manager().power_of_2();
|
||||
pdd const& s = m_search.assignment(sz);
|
||||
return p.subst_val(s);
|
||||
}
|
||||
|
||||
pdd solver::subst(assignment_t const& sub, pdd const& p) const {
|
||||
unsigned sz = p.manager().power_of_2();
|
||||
pdd s = p.manager().mk_val(1);
|
||||
for (auto const& [var, val] : sub)
|
||||
if (size(var) == sz)
|
||||
s = p.manager().subst_add(s, var, val);
|
||||
return p.subst_val(s);
|
||||
return assignment().apply_to(p);
|
||||
}
|
||||
|
||||
/** Check that boolean assignment and constraint evaluation are consistent */
|
||||
|
|
|
|||
|
|
@ -31,6 +31,7 @@ Author:
|
|||
#include "math/polysat/justification.h"
|
||||
#include "math/polysat/linear_solver.h"
|
||||
#include "math/polysat/search_state.h"
|
||||
#include "math/polysat/assignment.h"
|
||||
#include "math/polysat/trail.h"
|
||||
#include "math/polysat/viable.h"
|
||||
#include "math/polysat/log.h"
|
||||
|
|
@ -45,6 +46,52 @@ namespace polysat {
|
|||
bool m_log_conflicts = false;
|
||||
};
|
||||
|
||||
/**
|
||||
* A metric to evaluate lemmas from conflict analysis.
|
||||
* Lower is better.
|
||||
*
|
||||
* Comparison criterion:
|
||||
* - Lowest jump level has priority, because otherwise, some of the accumulated lemmas may still be false after backjumping.
|
||||
* - To break ties on jump level, choose clause with the fewest literals at its highest decision level;
|
||||
* to limit case splits.
|
||||
*/
|
||||
class lemma_score {
|
||||
unsigned m_jump_level;
|
||||
unsigned m_literals_at_max_level;
|
||||
|
||||
public:
|
||||
lemma_score(unsigned jump_level, unsigned at_max_level)
|
||||
: m_jump_level(jump_level), m_literals_at_max_level(at_max_level)
|
||||
{ }
|
||||
|
||||
unsigned jump_level() const { return m_jump_level; }
|
||||
unsigned literals_at_max_level() const { return m_literals_at_max_level; }
|
||||
|
||||
static lemma_score max() {
|
||||
return {UINT_MAX, UINT_MAX};
|
||||
}
|
||||
|
||||
bool operator==(lemma_score const& other) const {
|
||||
return m_jump_level == other.m_jump_level
|
||||
&& m_literals_at_max_level == other.m_literals_at_max_level;
|
||||
}
|
||||
bool operator!=(lemma_score const& other) const { return !operator==(other); }
|
||||
|
||||
bool operator<(lemma_score const& other) const {
|
||||
return m_jump_level < other.m_jump_level
|
||||
|| (m_jump_level == other.m_jump_level && m_literals_at_max_level < other.m_literals_at_max_level);
|
||||
}
|
||||
bool operator>(lemma_score const& other) const { return other.operator<(*this); }
|
||||
bool operator<=(lemma_score const& other) const { return operator==(other) || operator<(other); }
|
||||
bool operator>=(lemma_score const& other) const { return operator==(other) || operator>(other); }
|
||||
|
||||
std::ostream& display(std::ostream& out) const {
|
||||
return out << "jump_level=" << m_jump_level << " at_max_level=" << m_literals_at_max_level;
|
||||
}
|
||||
};
|
||||
|
||||
inline std::ostream& operator<<(std::ostream& out, lemma_score const& ls) { return ls.display(out); }
|
||||
|
||||
class solver {
|
||||
|
||||
struct stats {
|
||||
|
|
@ -58,6 +105,7 @@ namespace polysat {
|
|||
stats() { reset(); }
|
||||
};
|
||||
|
||||
friend class assignment;
|
||||
friend class constraint;
|
||||
friend class ule_constraint;
|
||||
friend class umul_ovfl_constraint;
|
||||
|
|
@ -125,8 +173,6 @@ namespace polysat {
|
|||
unsigned_vector m_size; // store size of variables (bit width)
|
||||
|
||||
search_state m_search;
|
||||
assignment_t const& assignment() const { return m_search.assignment(); }
|
||||
pdd subst(assignment_t const& sub, pdd const& p) const;
|
||||
|
||||
unsigned m_qhead = 0; // next item to propagate (index into m_search)
|
||||
unsigned m_level = 0;
|
||||
|
|
@ -150,7 +196,6 @@ namespace polysat {
|
|||
m_qhead_trail.pop_back();
|
||||
}
|
||||
|
||||
|
||||
unsigned size(pvar v) const { return m_size[v]; }
|
||||
|
||||
/**
|
||||
|
|
@ -161,16 +206,19 @@ namespace polysat {
|
|||
void del_var();
|
||||
|
||||
dd::pdd_manager& sz2pdd(unsigned sz) const;
|
||||
dd::pdd_manager& var2pdd(pvar v);
|
||||
dd::pdd_manager& var2pdd(pvar v) const;
|
||||
|
||||
assignment const& assignment() const { return m_search.assignment(); }
|
||||
|
||||
void push_level();
|
||||
void pop_levels(unsigned num_levels);
|
||||
|
||||
void try_assign_eval(signed_constraint c);
|
||||
|
||||
void assign_propagate(sat::literal lit, clause& reason);
|
||||
void assign_decision(sat::literal lit);
|
||||
void assign_eval(sat::literal lit);
|
||||
void activate_constraint(signed_constraint c);
|
||||
void deactivate_constraint(signed_constraint c);
|
||||
unsigned level(sat::literal lit, clause const& cl);
|
||||
|
||||
void assign_propagate(pvar v, rational const& val);
|
||||
|
|
@ -212,6 +260,8 @@ namespace polysat {
|
|||
void revert_decision(pvar v);
|
||||
void revert_bool_decision(sat::literal lit);
|
||||
void backjump_and_learn(unsigned jump_level, clause& lemma);
|
||||
void backjump_and_learn(unsigned max_jump_level);
|
||||
std::optional<lemma_score> compute_lemma_score(clause const& lemma);
|
||||
|
||||
// activity of variables based on standard VSIDS
|
||||
unsigned m_activity_inc = 128;
|
||||
|
|
@ -236,9 +286,6 @@ namespace polysat {
|
|||
|
||||
bool invariant();
|
||||
static bool invariant(signed_constraints const& cs);
|
||||
bool lemma_invariant(clause const& lemma, assignment_t const& assignment);
|
||||
bool lemma_invariant_part1(clause const& lemma, assignment_t const& assignment, sat::literal_vector& out_todo);
|
||||
bool lemma_invariant_part2(sat::literal_vector const& todo);
|
||||
bool wlist_invariant();
|
||||
bool assignment_invariant();
|
||||
bool verify_sat();
|
||||
|
|
@ -430,7 +477,7 @@ namespace polysat {
|
|||
|
||||
}; // class solver
|
||||
|
||||
class assignments_pp {
|
||||
class assignments_pp { // TODO: can probably remove this now.
|
||||
solver const& s;
|
||||
public:
|
||||
assignments_pp(solver const& s): s(s) {}
|
||||
|
|
|
|||
|
|
@ -15,8 +15,6 @@ Author:
|
|||
#include "math/polysat/log.h"
|
||||
#include "math/polysat/solver.h"
|
||||
|
||||
// TODO: rename file
|
||||
|
||||
namespace polysat {
|
||||
|
||||
struct inference_sup : public inference {
|
||||
|
|
@ -37,8 +35,8 @@ namespace polysat {
|
|||
SASSERT(c1.is_currently_true(s));
|
||||
SASSERT(c2.is_currently_false(s));
|
||||
LOG_H3("Resolving upon v" << v);
|
||||
LOG("c1: " << c1);
|
||||
LOG("c2: " << c2);
|
||||
LOG("c1: " << lit_pp(s, c1));
|
||||
LOG("c2: " << lit_pp(s, c2));
|
||||
pdd a = c1.eq();
|
||||
pdd b = c2.eq();
|
||||
unsigned degree_a = a.degree();
|
||||
|
|
@ -51,8 +49,6 @@ namespace polysat {
|
|||
return {};
|
||||
// Only keep result if the degree in c2 was reduced.
|
||||
// (this condition might be too strict, but we use it for now to prevent looping)
|
||||
// TODO: check total degree; only keep if total degree smaller or equal.
|
||||
// can always do this if c1 is linear.
|
||||
if (b.degree(v) <= r.degree(v))
|
||||
return {};
|
||||
if (a.degree(v) <= r.degree(v))
|
||||
|
|
@ -76,7 +72,6 @@ namespace polysat {
|
|||
SASSERT(c1.is_currently_true(s));
|
||||
SASSERT(c2.is_currently_false(s));
|
||||
SASSERT_EQ(c1.bvalue(s), l_true);
|
||||
// SASSERT_EQ(c2.bvalue(s), l_true); // TODO: should always be l_true but currently it's not guaranteed if c2 was derived via side lemma (tag:true_by_side_lemma)
|
||||
SASSERT(c2.bvalue(s) != l_false);
|
||||
|
||||
signed_constraint c = resolve1(v, c1, c2);
|
||||
|
|
@ -84,37 +79,25 @@ namespace polysat {
|
|||
continue;
|
||||
SASSERT(c.is_currently_false(s));
|
||||
|
||||
// TODO: move this case distinction into conflict::add_lemma?
|
||||
char const* inf_name = "?";
|
||||
// char const* inf_name = "?";
|
||||
switch (c.bvalue(s)) {
|
||||
case l_false:
|
||||
// new conflict state based on propagation and theory conflict
|
||||
core.remove_all();
|
||||
core.insert(c1);
|
||||
core.insert(c2);
|
||||
core.insert(~c);
|
||||
core.log_inference(inference_sup("l_false", v, c2, c1));
|
||||
core.add_lemma({c, ~c1, ~c2});
|
||||
// core.log_inference(inference_sup("l_false", v, c2, c1));
|
||||
return l_true;
|
||||
case l_undef:
|
||||
inf_name = "l_undef";
|
||||
// c evaluates to false,
|
||||
// c should be unit-propagated to l_true by c1 /\ c2 ==> c
|
||||
// inf_name = "l_undef";
|
||||
core.add_lemma({c, ~c1, ~c2});
|
||||
core.log_inference(inference_sup("l_undef lemma", v, c2, c1));
|
||||
// SASSERT_EQ(l_true, c.bvalue(s)); // not true anymore (TODO: but it should be) (tag:true_by_side_lemma)
|
||||
// core.log_inference(inference_sup("l_undef lemma", v, c2, c1));
|
||||
break;
|
||||
case l_true:
|
||||
// c is just another constraint on the search stack; could be equivalent or better
|
||||
inf_name = "l_true";
|
||||
break;
|
||||
default:
|
||||
UNREACHABLE();
|
||||
break;
|
||||
}
|
||||
|
||||
// c alone (+ variables) is now enough to represent the conflict.
|
||||
core.set(c);
|
||||
core.log_inference(inference_sup(inf_name, v, c2, c1));
|
||||
// // c alone (+ variables) is now enough to represent the conflict.
|
||||
// core.log_inference(inference_sup(inf_name, v, c2, c1));
|
||||
return c->contains_var(v) ? l_undef : l_true;
|
||||
}
|
||||
return l_false;
|
||||
|
|
|
|||
|
|
@ -18,6 +18,7 @@ Author:
|
|||
#include "util/scoped_ptr_vector.h"
|
||||
#include "util/var_queue.h"
|
||||
#include "util/ref_vector.h"
|
||||
#include "util/sat_literal.h"
|
||||
#include "math/dd/dd_pdd.h"
|
||||
#include "math/dd/dd_bdd.h"
|
||||
#include "math/dd/dd_fdd.h"
|
||||
|
|
@ -25,6 +26,8 @@ Author:
|
|||
namespace polysat {
|
||||
|
||||
class solver;
|
||||
class clause;
|
||||
|
||||
typedef dd::pdd pdd;
|
||||
typedef dd::bdd bdd;
|
||||
typedef dd::bddv bddv;
|
||||
|
|
|
|||
|
|
@ -17,7 +17,7 @@ Notes:
|
|||
|
||||
Rewrite rules to simplify expressions.
|
||||
In the following let k, k1, k2 be values.
|
||||
|
||||
|
||||
- k1 <= k2 ==> 0 <= 0 if k1 <= k2
|
||||
- k1 <= k2 ==> 1 <= 0 if k1 > k2
|
||||
- 0 <= p ==> 0 <= 0
|
||||
|
|
@ -39,7 +39,7 @@ Notes:
|
|||
|
||||
TODO: clause simplifications:
|
||||
|
||||
- p + k <= p ==> p + k <= k & p != 0 for k != 0
|
||||
- p + k <= p ==> p + k <= k & p != 0 for k != 0
|
||||
- p*q = 0 ==> p = 0 or q = 0 applies to any factoring
|
||||
- 2*p <= 2*q ==> (p >= 2^n-1 & q < 2^n-1) or (p >= 2^n-1 = q >= 2^n-1 & p <= q)
|
||||
==> (p >= 2^n-1 => q < 2^n-1 or p <= q) &
|
||||
|
|
@ -50,7 +50,7 @@ TODO: clause simplifications:
|
|||
|
||||
Note:
|
||||
case p <= p + k is already covered because we test (lhs - rhs).is_val()
|
||||
|
||||
|
||||
It can be seen as an instance of lemma 5.2 of Supratik and John.
|
||||
|
||||
--*/
|
||||
|
|
@ -168,7 +168,7 @@ namespace polysat {
|
|||
void ule_constraint::narrow(solver& s, bool is_positive, bool first) {
|
||||
auto p = s.subst(lhs());
|
||||
auto q = s.subst(rhs());
|
||||
|
||||
|
||||
signed_constraint sc(this, is_positive);
|
||||
|
||||
LOG_H3("Narrowing " << sc);
|
||||
|
|
@ -189,55 +189,43 @@ namespace polysat {
|
|||
s.m_viable.intersect(p, q, sc);
|
||||
}
|
||||
|
||||
bool ule_constraint::is_always_false(bool is_positive, pdd const& lhs, pdd const& rhs) {
|
||||
// Evaluate lhs <= rhs
|
||||
lbool ule_constraint::eval(pdd const& lhs, pdd const& rhs) {
|
||||
// NOTE: don't assume simplifications here because we also call this on partially substituted constraints
|
||||
if (is_positive) {
|
||||
// lhs <= rhs
|
||||
if (rhs.is_zero())
|
||||
return lhs.is_never_zero(); // p <= 0 implies p == 0
|
||||
return lhs.is_val() && rhs.is_val() && lhs.val() > rhs.val();
|
||||
}
|
||||
else {
|
||||
// lhs > rhs
|
||||
if (lhs.is_zero())
|
||||
return true; // 0 > ... is always false
|
||||
if (lhs == rhs)
|
||||
return true; // p > p
|
||||
if (rhs.is_max())
|
||||
return true; // p > -1
|
||||
if (lhs.is_one() && rhs.is_never_zero())
|
||||
return true; // 1 > p implies p == 0
|
||||
return lhs.is_val() && rhs.is_val() && lhs.val() <= rhs.val();
|
||||
}
|
||||
if (lhs.is_zero())
|
||||
return l_true; // 0 <= p
|
||||
if (lhs == rhs)
|
||||
return l_true; // p <= p
|
||||
if (rhs.is_max())
|
||||
return l_true; // p <= -1
|
||||
if (rhs.is_zero() && lhs.is_never_zero())
|
||||
return l_false; // p <= 0 implies p == 0
|
||||
if (lhs.is_one() && rhs.is_never_zero())
|
||||
return l_true; // 1 <= p implies p != 0
|
||||
if (lhs.is_val() && rhs.is_val())
|
||||
return to_lbool(lhs.val() <= rhs.val());
|
||||
return l_undef;
|
||||
}
|
||||
|
||||
lbool ule_constraint::eval() const {
|
||||
return eval(lhs(), rhs());
|
||||
}
|
||||
|
||||
bool ule_constraint::is_always_false(bool is_positive) const {
|
||||
return is_always_false(is_positive, lhs(), rhs());
|
||||
}
|
||||
|
||||
bool ule_constraint::is_currently_false(solver& s, bool is_positive) const {
|
||||
auto p = s.subst(lhs());
|
||||
auto q = s.subst(rhs());
|
||||
return is_always_false(is_positive, p, q);
|
||||
}
|
||||
|
||||
bool ule_constraint::is_currently_false(solver& s, assignment_t const& sub, bool is_positive) const {
|
||||
auto p = s.subst(sub, lhs());
|
||||
auto q = s.subst(sub, rhs());
|
||||
return is_always_false(is_positive, p, q);
|
||||
lbool ule_constraint::eval(assignment const& a) const {
|
||||
return eval(a.apply_to(lhs()), a.apply_to(rhs()));
|
||||
}
|
||||
|
||||
inequality ule_constraint::as_inequality(bool is_positive) const {
|
||||
if (is_positive)
|
||||
return inequality(lhs(), rhs(), false, this);
|
||||
else
|
||||
else
|
||||
return inequality(rhs(), lhs(), true, this);
|
||||
}
|
||||
|
||||
unsigned ule_constraint::hash() const {
|
||||
return mk_mix(lhs().hash(), rhs().hash(), kind());
|
||||
}
|
||||
|
||||
|
||||
bool ule_constraint::operator==(constraint const& other) const {
|
||||
return other.is_ule() && lhs() == other.to_ule().lhs() && rhs() == other.to_ule().rhs();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -27,7 +27,9 @@ namespace polysat {
|
|||
|
||||
ule_constraint(constraint_manager& m, pdd const& l, pdd const& r);
|
||||
static void simplify(bool& is_positive, pdd& lhs, pdd& rhs);
|
||||
static bool is_always_false(bool is_positive, pdd const& lhs, pdd const& rhs);
|
||||
static bool is_always_true(bool is_positive, pdd const& lhs, pdd const& rhs) { return eval(lhs, rhs) == to_lbool(is_positive); }
|
||||
static bool is_always_false(bool is_positive, pdd const& lhs, pdd const& rhs) { return is_always_true(!is_positive, lhs, rhs); }
|
||||
static lbool eval(pdd const& lhs, pdd const& rhs);
|
||||
|
||||
public:
|
||||
~ule_constraint() override {}
|
||||
|
|
@ -36,9 +38,8 @@ namespace polysat {
|
|||
static std::ostream& display(std::ostream& out, lbool status, pdd const& lhs, pdd const& rhs);
|
||||
std::ostream& display(std::ostream& out, lbool status) const override;
|
||||
std::ostream& display(std::ostream& out) const override;
|
||||
bool is_always_false(bool is_positive) const override;
|
||||
bool is_currently_false(solver& s, bool is_positive) const override;
|
||||
bool is_currently_false(solver& s, assignment_t const& sub, bool is_positive) const override;
|
||||
lbool eval() const override;
|
||||
lbool eval(assignment const& a) const override;
|
||||
void narrow(solver& s, bool is_positive, bool first) override;
|
||||
inequality as_inequality(bool is_positive) const override;
|
||||
unsigned hash() const override;
|
||||
|
|
|
|||
|
|
@ -40,15 +40,15 @@ namespace polysat {
|
|||
case l_true: return display(out);
|
||||
case l_false: return display(out << "~");
|
||||
case l_undef: return display(out << "?");
|
||||
}
|
||||
}
|
||||
return out;
|
||||
}
|
||||
|
||||
std::ostream& umul_ovfl_constraint::display(std::ostream& out) const {
|
||||
return out << "ovfl*(" << m_p << ", " << m_q << ")";
|
||||
return out << "ovfl*(" << m_p << ", " << m_q << ")";
|
||||
}
|
||||
|
||||
lbool umul_ovfl_constraint::eval(pdd const& p, pdd const& q) const {
|
||||
lbool umul_ovfl_constraint::eval(pdd const& p, pdd const& q) {
|
||||
if (p.is_zero() || q.is_zero() || p.is_one() || q.is_one())
|
||||
return l_false;
|
||||
|
||||
|
|
@ -61,30 +61,18 @@ namespace polysat {
|
|||
return l_undef;
|
||||
}
|
||||
|
||||
bool umul_ovfl_constraint::is_always_false(bool is_positive, pdd const& p, pdd const& q) const {
|
||||
switch (eval(p, q)) {
|
||||
case l_true: return !is_positive;
|
||||
case l_false: return is_positive;
|
||||
default: return false;
|
||||
}
|
||||
lbool umul_ovfl_constraint::eval() const {
|
||||
return eval(p(), q());
|
||||
}
|
||||
|
||||
bool umul_ovfl_constraint::is_always_true(bool is_positive, pdd const& p, pdd const& q) const {
|
||||
return is_always_false(!is_positive, p, q);
|
||||
lbool umul_ovfl_constraint::eval(assignment const& a) const {
|
||||
return eval(a.apply_to(p()), a.apply_to(q()));
|
||||
}
|
||||
|
||||
bool umul_ovfl_constraint::is_always_false(bool is_positive) const {
|
||||
return is_always_false(is_positive, m_p, m_q);
|
||||
}
|
||||
|
||||
bool umul_ovfl_constraint::is_currently_false(solver& s, bool is_positive) const {
|
||||
return is_always_false(is_positive, s.subst(p()), s.subst(q()));
|
||||
}
|
||||
|
||||
void umul_ovfl_constraint::narrow(solver& s, bool is_positive, bool first) {
|
||||
void umul_ovfl_constraint::narrow(solver& s, bool is_positive, bool first) {
|
||||
auto p1 = s.subst(p());
|
||||
auto q1 = s.subst(q());
|
||||
|
||||
|
||||
if (is_always_false(is_positive, p1, q1)) {
|
||||
s.set_conflict({ this, is_positive });
|
||||
return;
|
||||
|
|
@ -94,19 +82,19 @@ namespace polysat {
|
|||
|
||||
if (try_viable(s, is_positive, p(), q(), p1, q1))
|
||||
return;
|
||||
|
||||
|
||||
if (narrow_bound(s, is_positive, p(), q(), p1, q1))
|
||||
return;
|
||||
if (narrow_bound(s, is_positive, q(), p(), q1, p1))
|
||||
return;
|
||||
|
||||
|
||||
|
||||
}
|
||||
|
||||
/**
|
||||
* if p constant, q, propagate inequality
|
||||
*/
|
||||
bool umul_ovfl_constraint::narrow_bound(solver& s, bool is_positive,
|
||||
* if p constant, q, propagate inequality
|
||||
*/
|
||||
bool umul_ovfl_constraint::narrow_bound(solver& s, bool is_positive,
|
||||
pdd const& p0, pdd const& q0, pdd const& p, pdd const& q) {
|
||||
|
||||
if (!p.is_val())
|
||||
|
|
@ -118,13 +106,13 @@ namespace polysat {
|
|||
auto bound = ceil((max + 1) / p.val());
|
||||
|
||||
//
|
||||
// the clause that explains bound <= q or bound > q
|
||||
//
|
||||
// the clause that explains bound <= q or bound > q
|
||||
//
|
||||
// Ovfl(p, q) & p <= p.val() => q >= bound
|
||||
// ~Ovfl(p, q) & p >= p.val() => q < bound
|
||||
// ~Ovfl(p, q) & p >= p.val() => q < bound
|
||||
//
|
||||
|
||||
signed_constraint sc(this, is_positive);
|
||||
signed_constraint sc(this, is_positive);
|
||||
signed_constraint premise = is_positive ? s.ule(p0, p.val()) : s.ule(p.val(), p0);
|
||||
signed_constraint conseq = is_positive ? s.ule(bound, q0) : s.ult(q0, bound);
|
||||
|
||||
|
|
|
|||
|
|
@ -25,22 +25,21 @@ namespace polysat {
|
|||
|
||||
umul_ovfl_constraint(constraint_manager& m, pdd const& p, pdd const& q);
|
||||
void simplify();
|
||||
bool is_always_false(bool is_positive, pdd const& p, pdd const& q) const;
|
||||
bool is_always_true(bool is_positive, pdd const& p, pdd const& q) const;
|
||||
static bool is_always_true(bool is_positive, pdd const& p, pdd const& q) { return eval(p, q) == to_lbool(is_positive); }
|
||||
static bool is_always_false(bool is_positive, pdd const& p, pdd const& q) { return is_always_true(!is_positive, p, q); }
|
||||
static lbool eval(pdd const& p, pdd const& q);
|
||||
bool narrow_bound(solver& s, bool is_positive, pdd const& p0, pdd const& q0, pdd const& p, pdd const& q);
|
||||
bool try_viable(solver& s, bool is_positive, pdd const& p0, pdd const& q0, pdd const& p, pdd const& q);
|
||||
lbool eval(pdd const& p, pdd const& q) const;
|
||||
|
||||
|
||||
public:
|
||||
~umul_ovfl_constraint() override {}
|
||||
pdd const& p() const { return m_p; }
|
||||
pdd const& q() const { return m_q; }
|
||||
std::ostream& display(std::ostream& out, lbool status) const override;
|
||||
std::ostream& display(std::ostream& out) const override;
|
||||
bool is_always_false(bool is_positive) const override;
|
||||
lbool eval() const override;
|
||||
lbool eval(assignment const& a) const override;
|
||||
void narrow(solver& s, bool is_positive, bool first) override;
|
||||
bool is_currently_false(solver & s, bool is_positive) const override;
|
||||
bool is_currently_false(solver& s, assignment_t const& sub, bool is_positive) const override { return false; }
|
||||
|
||||
inequality as_inequality(bool is_positive) const override { throw default_exception("is not an inequality"); }
|
||||
unsigned hash() const override;
|
||||
|
|
|
|||
|
|
@ -380,6 +380,7 @@ namespace polysat {
|
|||
LOG("p2: " << p2);
|
||||
|
||||
clause_builder cb(s);
|
||||
|
||||
/*for (auto [w, wv] : a)
|
||||
cb.push(~s.eq(s.var(w), wv));*/
|
||||
cb.insert(~c);
|
||||
|
|
@ -394,19 +395,19 @@ namespace polysat {
|
|||
}
|
||||
|
||||
// Evaluate p under assignments in the core.
|
||||
pdd free_variable_elimination::eval(pdd const& p, conflict& core, assignment_t& out_assignment) {
|
||||
pdd free_variable_elimination::eval(pdd const& p, conflict& core, substitution& out_sub) {
|
||||
// TODO: this should probably be a helper method on conflict.
|
||||
// TODO: recognize constraints of the form "v1 == 27" to be used in the assignment?
|
||||
// (but maybe useful evaluations are always part of core.vars() anyway?)
|
||||
|
||||
assignment_t& a = out_assignment;
|
||||
SASSERT(a.empty());
|
||||
substitution& sub = out_sub;
|
||||
SASSERT(sub.empty());
|
||||
|
||||
for (auto v : p.free_vars())
|
||||
if (core.contains_pvar(v))
|
||||
a.push_back({v, s.get_value(v)});
|
||||
sub.add(v, s.get_value(v));
|
||||
|
||||
pdd q = s.subst(a, p);
|
||||
pdd q = sub.apply_to(p);
|
||||
|
||||
// TODO: like in the old conflict::minimize_vars, we can now try to remove unnecessary variables from a.
|
||||
|
||||
|
|
|
|||
|
|
@ -40,7 +40,7 @@ namespace polysat {
|
|||
std::pair<pdd, pdd> get_dyadic_valuation(pdd p);
|
||||
void find_lemma(pvar v, conflict& core);
|
||||
void find_lemma(pvar v, signed_constraint c, conflict& core);
|
||||
pdd eval(pdd const& p, conflict& core, assignment_t& out_assignment);
|
||||
pdd eval(pdd const& p, conflict& core, substitution& out_sub);
|
||||
bool inv(pdd const& p, pdd& out_p_inv);
|
||||
bool is_multiple(const pdd& p1, const pdd& p2, pdd &out);
|
||||
public:
|
||||
|
|
|
|||
|
|
@ -132,7 +132,7 @@ namespace polysat {
|
|||
rational val;
|
||||
switch (find_viable(v, val)) {
|
||||
case dd::find_t::singleton:
|
||||
s.assign_propagate(v, val);
|
||||
propagate(v, val);
|
||||
prop = true;
|
||||
break;
|
||||
case dd::find_t::empty:
|
||||
|
|
@ -150,6 +150,24 @@ namespace polysat {
|
|||
return prop;
|
||||
}
|
||||
|
||||
void viable::propagate(pvar v, rational const& val) {
|
||||
// NOTE: all propagations must be justified by a prefix of \Gamma,
|
||||
// otherwise dependencies may be missed during conflict resolution.
|
||||
// The propagation reason for v := val consists of the following constraints:
|
||||
// - source constraint (already on \Gamma)
|
||||
// - side conditions
|
||||
// - i.lo() == i.lo_val() for each unit interval i
|
||||
// - i.hi() == i.hi_val() for each unit interval i
|
||||
for (auto const& c : get_constraints(v)) {
|
||||
s.try_assign_eval(c);
|
||||
}
|
||||
for (auto const& i : units(v)) {
|
||||
s.try_assign_eval(s.eq(i.lo(), i.lo_val()));
|
||||
s.try_assign_eval(s.eq(i.hi(), i.hi_val()));
|
||||
}
|
||||
s.assign_propagate(v, val);
|
||||
}
|
||||
|
||||
bool viable::intersect(pvar v, signed_constraint const& c) {
|
||||
entry* ne = alloc_entry();
|
||||
if (!m_forbidden_intervals.get_interval(c, v, *ne)) {
|
||||
|
|
@ -187,6 +205,7 @@ namespace polysat {
|
|||
}
|
||||
|
||||
bool viable::intersect(pvar v, entry* ne) {
|
||||
SASSERT(!s.is_assigned(v));
|
||||
entry* e = m_units[v];
|
||||
if (e && e->interval.is_full()) {
|
||||
m_alloc.push_back(ne);
|
||||
|
|
@ -701,6 +720,7 @@ namespace polysat {
|
|||
lemma.insert_eval(~sc);
|
||||
lemma.insert(~e->src);
|
||||
core.insert(e->src);
|
||||
core.insert_vars(e->src);
|
||||
e = n;
|
||||
}
|
||||
while (e != first);
|
||||
|
|
|
|||
|
|
@ -63,6 +63,8 @@ namespace polysat {
|
|||
|
||||
void insert(entry* e, pvar v, ptr_vector<entry>& entries, entry_kind k);
|
||||
|
||||
void propagate(pvar v, rational const& val);
|
||||
|
||||
public:
|
||||
viable(solver& s);
|
||||
|
||||
|
|
|
|||
|
|
@ -571,6 +571,38 @@ public:
|
|||
}
|
||||
}
|
||||
|
||||
static void subst_get() {
|
||||
std::cout << "subst_get\n";
|
||||
pdd_manager m(4, pdd_manager::mod2N_e, 32);
|
||||
|
||||
unsigned const va = 0;
|
||||
unsigned const vb = 1;
|
||||
unsigned const vc = 2;
|
||||
unsigned const vd = 3;
|
||||
|
||||
rational val;
|
||||
pdd s = m.one();
|
||||
std::cout << s << "\n";
|
||||
VERIFY(!s.subst_get(va, val));
|
||||
VERIFY(!s.subst_get(vb, val));
|
||||
VERIFY(!s.subst_get(vc, val));
|
||||
VERIFY(!s.subst_get(vd, val));
|
||||
|
||||
s = s.subst_add(va, rational(5));
|
||||
std::cout << s << "\n";
|
||||
VERIFY(s.subst_get(va, val) && val == 5);
|
||||
VERIFY(!s.subst_get(vb, val));
|
||||
VERIFY(!s.subst_get(vc, val));
|
||||
VERIFY(!s.subst_get(vd, val));
|
||||
|
||||
s = s.subst_add(vc, rational(7));
|
||||
std::cout << s << "\n";
|
||||
VERIFY(s.subst_get(va, val) && val == 5);
|
||||
VERIFY(!s.subst_get(vb, val));
|
||||
VERIFY(s.subst_get(vc, val) && val == 7);
|
||||
VERIFY(!s.subst_get(vd, val));
|
||||
}
|
||||
|
||||
static void univariate() {
|
||||
std::cout << "univariate\n";
|
||||
pdd_manager m(4, pdd_manager::mod2N_e, 4);
|
||||
|
|
@ -671,6 +703,7 @@ void tst_pdd() {
|
|||
dd::test::binary_resolve();
|
||||
dd::test::pow();
|
||||
dd::test::subst_val();
|
||||
dd::test::subst_get();
|
||||
dd::test::univariate();
|
||||
dd::test::factors();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -9,6 +9,17 @@
|
|||
namespace {
|
||||
using namespace dd;
|
||||
|
||||
template <typename... Args>
|
||||
std::string concat(Args... args) {
|
||||
std::stringstream s;
|
||||
int dummy[sizeof...(Args)] = {
|
||||
// use dummy initializer list to sequence stream writes, cf. https://en.cppreference.com/w/cpp/language/parameter_pack
|
||||
(s << args, 0)...
|
||||
};
|
||||
(void)dummy;
|
||||
return s.str();
|
||||
}
|
||||
|
||||
void permute_args(unsigned k, pdd& a, pdd& b, pdd& c) {
|
||||
SASSERT(k < 6);
|
||||
unsigned i = k % 3;
|
||||
|
|
@ -90,6 +101,12 @@ namespace polysat {
|
|||
for (test_record const& r : recs)
|
||||
max_name_len = std::max(max_name_len, r.m_name.length());
|
||||
|
||||
size_t n_total = recs.size();
|
||||
size_t n_sat = 0;
|
||||
size_t n_unsat = 0;
|
||||
size_t n_wrong = 0;
|
||||
size_t n_error = 0;
|
||||
|
||||
for (test_record const& r : recs) {
|
||||
out << r.m_name;
|
||||
if (r.m_index != 1)
|
||||
|
|
@ -111,15 +128,40 @@ namespace polysat {
|
|||
case l_false: out << "UNSAT "; break;
|
||||
}
|
||||
switch (r.m_result) {
|
||||
case test_result::undefined: out << "???"; break;
|
||||
case test_result::ok: out << "ok"; break;
|
||||
case test_result::wrong_answer: out << color_red() << "wrong answer, expected " << r.m_expected << color_reset(); break;
|
||||
case test_result::wrong_model: out << color_red() << "wrong model" << color_reset(); break;
|
||||
case test_result::resource_out: out << color_yellow() << "resource out" << color_reset(); break;
|
||||
case test_result::error: out << color_red() << "error: " << r.m_error_message << color_reset(); break;
|
||||
case test_result::undefined:
|
||||
out << "???";
|
||||
break;
|
||||
case test_result::ok:
|
||||
out << "ok";
|
||||
if (r.m_answer == l_true)
|
||||
n_sat++;
|
||||
if (r.m_answer == l_false)
|
||||
n_unsat++;
|
||||
break;
|
||||
case test_result::wrong_answer:
|
||||
out << color_red() << "wrong answer, expected " << r.m_expected << color_reset();
|
||||
n_wrong++;
|
||||
break;
|
||||
case test_result::wrong_model:
|
||||
out << color_red() << "wrong model" << color_reset();
|
||||
n_wrong++;
|
||||
break;
|
||||
case test_result::resource_out:
|
||||
out << color_yellow() << "resource out" << color_reset();
|
||||
break;
|
||||
case test_result::error:
|
||||
out << color_red() << "error: " << r.m_error_message << color_reset();
|
||||
n_error++;
|
||||
break;
|
||||
}
|
||||
out << std::endl;
|
||||
}
|
||||
out << n_total << " tests, " << (n_sat + n_unsat) << " ok (" << n_sat << " sat, " << n_unsat << " unsat)";
|
||||
if (n_wrong)
|
||||
out << ", " << color_red() << n_wrong << " wrong!" << color_reset();
|
||||
if (n_error)
|
||||
out << ", " << color_red() << n_error << " error" << color_reset();
|
||||
out << std::endl;
|
||||
}
|
||||
|
||||
// test resolve, factoring routines
|
||||
|
|
@ -245,6 +287,29 @@ namespace polysat {
|
|||
}
|
||||
};
|
||||
|
||||
template <typename Test, typename... Args>
|
||||
void run(Test tst, Args... args)
|
||||
{
|
||||
bool got_exception = false;
|
||||
try {
|
||||
tst(args...);
|
||||
}
|
||||
catch(z3_exception const& e) {
|
||||
// TODO: collect in record
|
||||
got_exception = true;
|
||||
}
|
||||
catch(std::exception const& e) {
|
||||
// TODO: collect in record
|
||||
got_exception = true;
|
||||
}
|
||||
catch(...) {
|
||||
got_exception = true;
|
||||
}
|
||||
if (got_exception && !collect_test_records)
|
||||
throw;
|
||||
}
|
||||
|
||||
#define RUN(tst) run([]() { tst; })
|
||||
|
||||
class test_polysat {
|
||||
public:
|
||||
|
|
@ -550,7 +615,7 @@ namespace polysat {
|
|||
* We do overflow checks by doubling the base bitwidth here.
|
||||
*/
|
||||
static void test_monot(unsigned base_bw = 5) {
|
||||
scoped_solver s(std::string{__func__} + "(" + std::to_string(base_bw) + ")");
|
||||
scoped_solver s(concat(__func__, "(", base_bw, ")"));
|
||||
|
||||
auto max_int_const = rational::power_of_two(base_bw) - 1;
|
||||
|
||||
|
|
@ -1195,49 +1260,51 @@ namespace polysat {
|
|||
s.check();
|
||||
}
|
||||
|
||||
static void test_band(unsigned bw = 32) {
|
||||
{
|
||||
scoped_solver s(__func__);
|
||||
auto p = s.var(s.add_var(bw));
|
||||
auto q = s.var(s.add_var(bw));
|
||||
s.add_diseq(p - s.band(p, q));
|
||||
s.add_diseq(p - q);
|
||||
s.check();
|
||||
s.expect_sat();
|
||||
}
|
||||
{
|
||||
scoped_solver s(__func__);
|
||||
auto p = s.var(s.add_var(bw));
|
||||
auto q = s.var(s.add_var(bw));
|
||||
s.add_ult(p, s.band(p, q));
|
||||
s.check();
|
||||
s.expect_unsat();
|
||||
}
|
||||
{
|
||||
scoped_solver s(__func__);
|
||||
auto p = s.var(s.add_var(bw));
|
||||
auto q = s.var(s.add_var(bw));
|
||||
s.add_ult(q, s.band(p, q));
|
||||
s.check();
|
||||
s.expect_unsat();
|
||||
}
|
||||
{
|
||||
scoped_solver s(__func__);
|
||||
auto p = s.var(s.add_var(bw));
|
||||
auto q = s.var(s.add_var(bw));
|
||||
s.add_ule(p, s.band(p, q));
|
||||
s.check();
|
||||
s.expect_sat();
|
||||
}
|
||||
{
|
||||
scoped_solver s(__func__);
|
||||
auto p = s.var(s.add_var(bw));
|
||||
auto q = s.var(s.add_var(bw));
|
||||
s.add_ule(p, s.band(p, q));
|
||||
s.add_diseq(p - s.band(p, q));
|
||||
s.check();
|
||||
s.expect_unsat();
|
||||
}
|
||||
static void test_band1(unsigned bw = 32) {
|
||||
scoped_solver s(concat(__func__, " bw=", bw));
|
||||
auto p = s.var(s.add_var(bw));
|
||||
auto q = s.var(s.add_var(bw));
|
||||
s.add_diseq(p - s.band(p, q));
|
||||
s.add_diseq(p - q);
|
||||
s.check();
|
||||
s.expect_sat();
|
||||
}
|
||||
|
||||
static void test_band2(unsigned bw = 32) {
|
||||
scoped_solver s(concat(__func__, " bw=", bw));
|
||||
auto p = s.var(s.add_var(bw));
|
||||
auto q = s.var(s.add_var(bw));
|
||||
s.add_ult(p, s.band(p, q));
|
||||
s.check();
|
||||
s.expect_unsat();
|
||||
}
|
||||
|
||||
static void test_band3(unsigned bw = 32) {
|
||||
scoped_solver s(concat(__func__, " bw=", bw));
|
||||
auto p = s.var(s.add_var(bw));
|
||||
auto q = s.var(s.add_var(bw));
|
||||
s.add_ult(q, s.band(p, q));
|
||||
s.check();
|
||||
s.expect_unsat();
|
||||
}
|
||||
|
||||
static void test_band4(unsigned bw = 32) {
|
||||
scoped_solver s(concat(__func__, " bw=", bw));
|
||||
auto p = s.var(s.add_var(bw));
|
||||
auto q = s.var(s.add_var(bw));
|
||||
s.add_ule(p, s.band(p, q));
|
||||
s.check();
|
||||
s.expect_sat();
|
||||
}
|
||||
|
||||
static void test_band5(unsigned bw = 32) {
|
||||
scoped_solver s(concat(__func__, " bw=", bw));
|
||||
auto p = s.var(s.add_var(bw));
|
||||
auto q = s.var(s.add_var(bw));
|
||||
s.add_ule(p, s.band(p, q));
|
||||
s.add_diseq(p - s.band(p, q));
|
||||
s.check();
|
||||
s.expect_unsat();
|
||||
}
|
||||
|
||||
static void test_fi_zero() {
|
||||
|
|
@ -1444,10 +1511,15 @@ void tst_polysat() {
|
|||
|
||||
#if 0 // Enable this block to run a single unit test with detailed output.
|
||||
collect_test_records = false;
|
||||
// test_polysat::test_l2();
|
||||
// test_polysat::test_ineq1();
|
||||
// test_polysat::test_quot_rem();
|
||||
test_polysat::test_ineq_non_axiom1(32, 3);
|
||||
// test_polysat::test_monot(5);
|
||||
// test_polysat::test_ineq_non_axiom1(32, 3);
|
||||
// test_polysat::test_monot_bounds_full();
|
||||
// test_polysat::test_band2();
|
||||
// test_polysat::test_quot_rem_incomplete();
|
||||
// test_polysat::test_monot();
|
||||
test_polysat::test_fixed_point_arith_div_mul_inverse();
|
||||
return;
|
||||
#endif
|
||||
|
||||
|
|
@ -1459,67 +1531,68 @@ void tst_polysat() {
|
|||
set_log_enabled(false);
|
||||
}
|
||||
|
||||
test_polysat::test_clause_simplify1();
|
||||
RUN(test_polysat::test_clause_simplify1());
|
||||
|
||||
test_polysat::test_add_conflicts(); // ok
|
||||
test_polysat::test_wlist(); // ok
|
||||
test_polysat::test_cjust(); // uses viable_fallback; weak lemmas
|
||||
// test_polysat::test_subst(); // TODO: resource limit; needs polynomial superposition
|
||||
// test_polysat::test_subst_signed();
|
||||
test_polysat::test_pop_conflict(); // ok now (had bad conflict/pop interaction)
|
||||
RUN(test_polysat::test_add_conflicts());
|
||||
RUN(test_polysat::test_wlist());
|
||||
RUN(test_polysat::test_cjust());
|
||||
// RUN(test_polysat::test_subst());
|
||||
// RUN(test_polysat::test_subst_signed());
|
||||
RUN(test_polysat::test_pop_conflict());
|
||||
|
||||
test_polysat::test_l1(); // ok
|
||||
test_polysat::test_l2(); // ok but enumerates values
|
||||
test_polysat::test_l3(); // ok
|
||||
test_polysat::test_l4(); // ok now (had assertion failure in conflict::insert)
|
||||
test_polysat::test_l4b(); // ok
|
||||
test_polysat::test_l5(); // inefficient conflicts (needs equality reasoning)
|
||||
test_polysat::test_l6(); // ok (refine-equal-lin)
|
||||
RUN(test_polysat::test_l1());
|
||||
RUN(test_polysat::test_l2());
|
||||
RUN(test_polysat::test_l3());
|
||||
RUN(test_polysat::test_l4());
|
||||
RUN(test_polysat::test_l4b());
|
||||
RUN(test_polysat::test_l5());
|
||||
RUN(test_polysat::test_l6());
|
||||
|
||||
test_polysat::test_p1(); // ok (conflict @0 by viable_fallback)
|
||||
test_polysat::test_p2(); // ok (viable_fallback finds the correct value)
|
||||
test_polysat::test_p3(); // TODO: resource limit
|
||||
RUN(test_polysat::test_p1());
|
||||
RUN(test_polysat::test_p2());
|
||||
RUN(test_polysat::test_p3());
|
||||
|
||||
test_polysat::test_ineq_basic1(); // ok
|
||||
test_polysat::test_ineq_basic2(); // ok
|
||||
test_polysat::test_ineq_basic3(); // ok
|
||||
test_polysat::test_ineq_basic4(); // TODO: resource limit
|
||||
test_polysat::test_ineq_basic5(); // works, but only because variable order changes after the conflict
|
||||
// TODO: non-asserting lemma
|
||||
// possible variable selection heuristic: start with the most restricted interval?
|
||||
// (if we have a restricted and non-restricted variable; we should probably pick the restricted one first. hoping that we can propagate and uncover restrictions on the other variable.)
|
||||
test_polysat::test_ineq_basic6(); // same as ineq_basic5
|
||||
RUN(test_polysat::test_ineq_basic1());
|
||||
RUN(test_polysat::test_ineq_basic2());
|
||||
RUN(test_polysat::test_ineq_basic3());
|
||||
RUN(test_polysat::test_ineq_basic4());
|
||||
RUN(test_polysat::test_ineq_basic5());
|
||||
RUN(test_polysat::test_ineq_basic6());
|
||||
|
||||
test_polysat::test_var_minimize(); // works but var_minimized isn't used (UNSAT before lemma is created)
|
||||
RUN(test_polysat::test_var_minimize()); // works but var_minimize isn't used (UNSAT before lemma is created)
|
||||
|
||||
test_polysat::test_ineq1(); // TODO: resource limit
|
||||
test_polysat::test_ineq2(); // TODO: resource limit
|
||||
test_polysat::test_monot(); // TODO: assertion failure; resource limit
|
||||
test_polysat::test_monot_bounds(2);
|
||||
test_polysat::test_monot_bounds(8);
|
||||
test_polysat::test_monot_bounds();
|
||||
test_polysat::test_monot_bounds_full();
|
||||
test_polysat::test_monot_bounds_simple(8);
|
||||
test_polysat::test_fixed_point_arith_div_mul_inverse();
|
||||
RUN(test_polysat::test_ineq1());
|
||||
RUN(test_polysat::test_ineq2());
|
||||
RUN(test_polysat::test_monot());
|
||||
RUN(test_polysat::test_monot_bounds(2));
|
||||
RUN(test_polysat::test_monot_bounds(8));
|
||||
RUN(test_polysat::test_monot_bounds());
|
||||
RUN(test_polysat::test_monot_bounds_full());
|
||||
RUN(test_polysat::test_monot_bounds_simple(8));
|
||||
RUN(test_polysat::test_fixed_point_arith_div_mul_inverse());
|
||||
|
||||
test_polysat::test_ineq_axiom1();
|
||||
test_polysat::test_ineq_axiom2();
|
||||
test_polysat::test_ineq_axiom3();
|
||||
test_polysat::test_ineq_axiom4();
|
||||
test_polysat::test_ineq_axiom5();
|
||||
test_polysat::test_ineq_axiom6();
|
||||
test_polysat::test_ineq_non_axiom1();
|
||||
test_polysat::test_ineq_non_axiom4();
|
||||
RUN(test_polysat::test_ineq_axiom1());
|
||||
RUN(test_polysat::test_ineq_axiom2());
|
||||
RUN(test_polysat::test_ineq_axiom3());
|
||||
RUN(test_polysat::test_ineq_axiom4());
|
||||
RUN(test_polysat::test_ineq_axiom5());
|
||||
RUN(test_polysat::test_ineq_axiom6());
|
||||
RUN(test_polysat::test_ineq_non_axiom1());
|
||||
RUN(test_polysat::test_ineq_non_axiom4());
|
||||
|
||||
test_polysat::test_quot_rem_incomplete();
|
||||
test_polysat::test_quot_rem_fixed();
|
||||
test_polysat::test_band();
|
||||
test_polysat::test_quot_rem();
|
||||
RUN(test_polysat::test_quot_rem_incomplete());
|
||||
RUN(test_polysat::test_quot_rem_fixed());
|
||||
RUN(test_polysat::test_band1());
|
||||
RUN(test_polysat::test_band2());
|
||||
RUN(test_polysat::test_band3());
|
||||
RUN(test_polysat::test_band4());
|
||||
RUN(test_polysat::test_band5());
|
||||
RUN(test_polysat::test_quot_rem());
|
||||
|
||||
test_polysat::test_fi_zero();
|
||||
test_polysat::test_fi_nonzero();
|
||||
test_polysat::test_fi_nonmax();
|
||||
test_polysat::test_fi_disequal_mild();
|
||||
RUN(test_polysat::test_fi_zero());
|
||||
RUN(test_polysat::test_fi_nonzero());
|
||||
RUN(test_polysat::test_fi_nonmax());
|
||||
RUN(test_polysat::test_fi_disequal_mild());
|
||||
|
||||
// test_fi::exhaustive();
|
||||
// test_fi::randomized();
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue