mirror of
https://github.com/Z3Prover/z3
synced 2025-04-22 16:45:31 +00:00
set, lemma, minor
This commit is contained in:
Jakob Rath
parent
2f65ce1026
commit
6abe0c9be8
16 changed files with 91 additions and 23 deletions
|
|
@ -5,8 +5,8 @@ z3_add_component(polysat
|
|||
clause_builder.cpp
|
||||
conflict.cpp
|
||||
constraint.cpp
|
||||
# eq_explain.cpp
|
||||
# explain.cpp
|
||||
eq_explain.cpp
|
||||
explain.cpp
|
||||
forbidden_intervals.cpp
|
||||
inference_logger.cpp
|
||||
justification.cpp
|
||||
|
|
@ -14,7 +14,7 @@ z3_add_component(polysat
|
|||
log.cpp
|
||||
op_constraint.cpp
|
||||
restart.cpp
|
||||
# saturation.cpp
|
||||
saturation.cpp
|
||||
search_state.cpp
|
||||
simplify.cpp
|
||||
simplify_clause.cpp
|
||||
|
|
@ -22,7 +22,7 @@ z3_add_component(polysat
|
|||
solver.cpp
|
||||
ule_constraint.cpp
|
||||
umul_ovfl_constraint.cpp
|
||||
# variable_elimination.cpp
|
||||
variable_elimination.cpp
|
||||
viable.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
util
|
||||
|
|
|
|||
|
|
@ -145,9 +145,32 @@ namespace polysat {
|
|||
|
||||
void conflict::init(signed_constraint c) {
|
||||
SASSERT(empty());
|
||||
set_impl(c);
|
||||
logger().begin_conflict();
|
||||
}
|
||||
|
||||
void conflict::set(signed_constraint c) {
|
||||
reset();
|
||||
set_impl(c);
|
||||
}
|
||||
|
||||
void conflict::set_impl(signed_constraint c) {
|
||||
if (c.bvalue(s) == l_false) {
|
||||
// boolean conflict
|
||||
NOT_IMPLEMENTED_YET();
|
||||
SASSERT(false); // fail here to force check when we encounter this case
|
||||
// TODO: if we set() and then log() it will be confusing if this branch is hit.
|
||||
// ideally the boolean resolution would be done separately afterwards
|
||||
auto* cl = s.m_bvars.reason(c.blit());
|
||||
#if 0
|
||||
if (cl)
|
||||
set(*cl); // why the whole clause? or do we want the boolean resolution?
|
||||
else
|
||||
insert(c);
|
||||
#else
|
||||
insert(c);
|
||||
if (cl)
|
||||
resolve_bool(c.blit(), *cl);
|
||||
#endif
|
||||
} else {
|
||||
// conflict due to assignment
|
||||
SASSERT(c.bvalue(s) == l_true);
|
||||
|
|
@ -156,7 +179,6 @@ namespace polysat {
|
|||
insert_vars(c);
|
||||
}
|
||||
SASSERT(!empty());
|
||||
logger().begin_conflict(); // TODO: we often call reset/set so doing this here doesn't really work... make subsequent begins a no-op? or separate init and set? (set could then do reset() internally ... and we only need set() for signed_constraint, not all three variations)
|
||||
}
|
||||
|
||||
void conflict::init(clause const& cl) {
|
||||
|
|
@ -239,6 +261,19 @@ namespace polysat {
|
|||
m_var_occurrences[v]--;
|
||||
}
|
||||
|
||||
void conflict::insert(signed_constraint c, clause_ref lemma) {
|
||||
unsigned const idx = c.blit().to_uint();
|
||||
SASSERT(!contains(c)); // not required, but this case should be checked
|
||||
SASSERT(!m_lemmas.contains(idx)); // not required, but this case should be checked
|
||||
insert(c);
|
||||
m_lemmas.insert(idx, lemma);
|
||||
}
|
||||
|
||||
clause* conflict::side_lemma(sat::literal lit) const {
|
||||
unsigned const idx = lit.to_uint();
|
||||
return m_lemmas.get(idx, {}).get();
|
||||
}
|
||||
|
||||
void conflict::resolve_bool(sat::literal lit, clause const& cl) {
|
||||
// Note: core: x, y, z; corresponds to clause ~x \/ ~y \/ ~z
|
||||
// clause: x \/ u \/ v
|
||||
|
|
@ -337,8 +372,8 @@ namespace polysat {
|
|||
clause_builder lemma(s);
|
||||
|
||||
// TODO: is this sound, doing it for each constraint separately?
|
||||
// for (auto c : *this)
|
||||
// minimize_vars(c);
|
||||
for (auto c : *this)
|
||||
minimize_vars(c);
|
||||
|
||||
for (auto c : *this)
|
||||
lemma.push(~c);
|
||||
|
|
@ -354,6 +389,8 @@ namespace polysat {
|
|||
logger().log_lemma(lemma);
|
||||
logger().end_conflict();
|
||||
|
||||
// TODO: additional lemmas
|
||||
|
||||
return lemma.build();
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -76,6 +76,7 @@ TODO:
|
|||
- may force backjumping without further conflict resolution (e.g., if applicable lemma was found by global analysis of search state)
|
||||
- bailout lemma if no method applies (log these cases in particular because it indicates where we are missing something)
|
||||
- force a restart if we get a bailout lemma or non-asserting conflict?
|
||||
- store the side lemmas as well (but only those that justify a constraint in the final lemma, recursively)
|
||||
- consider case if v is both in vars and bail_vars (do we need to keep it in bail_vars even if we can eliminate it from vars?)
|
||||
- Find a way to use resolve_value with forbidden interval lemmas.
|
||||
Then get rid of conflict_kind_t::backtrack and m_relevant_vars.
|
||||
|
|
@ -88,9 +89,9 @@ TODO:
|
|||
- or try to find an L(x,y) such that C1 -> L, ..., Cn -> L, and L -> y != b (under x := a); worst case y != b can work as L
|
||||
- minimize_vars... is it sound to do for each constraint separately, like we are doing now?
|
||||
|
||||
|
||||
--*/
|
||||
#pragma once
|
||||
#include "math/polysat/types.h"
|
||||
#include "math/polysat/constraint.h"
|
||||
#include "math/polysat/inference_logger.h"
|
||||
#include <optional>
|
||||
|
|
@ -128,12 +129,12 @@ namespace polysat {
|
|||
|
||||
unsigned_vector m_var_occurrences; // for each variable, the number of constraints in m_literals that contain it
|
||||
|
||||
// additional lemmas generated during conflict resolution
|
||||
// TODO: we might not need all of these in the end. add only the side lemmas which justify a constraint in the final lemma (recursively)?
|
||||
vector<clause_ref> m_lemmas;
|
||||
// Additional lemmas that justify new constraints generated during conflict resolution
|
||||
u_map<clause_ref> m_lemmas;
|
||||
|
||||
conflict_kind_t m_kind = conflict_kind_t::ok;
|
||||
|
||||
void set_impl(signed_constraint c);
|
||||
bool minimize_vars(signed_constraint c);
|
||||
|
||||
public:
|
||||
|
|
@ -169,11 +170,17 @@ namespace polysat {
|
|||
/** conflict because there is no viable value for the variable v */
|
||||
void init(pvar v, bool by_viable_fallback);
|
||||
|
||||
/** replace the current conflict by a single constraint */
|
||||
void set(signed_constraint c);
|
||||
|
||||
bool contains(signed_constraint c) const { SASSERT(c); return contains(c.blit()); }
|
||||
bool contains(sat::literal lit) const;
|
||||
bool contains_pvar(pvar v) const { return m_vars.contains(v) || m_bail_vars.contains(v); }
|
||||
bool pvar_occurs_in_constraints(pvar v) const { return v < m_var_occurrences.size() && m_var_occurrences[v] > 0; }
|
||||
|
||||
clause* side_lemma(signed_constraint c) const { SASSERT(c); return side_lemma(c.blit()); }
|
||||
clause* side_lemma(sat::literal lit) const;
|
||||
|
||||
/**
|
||||
* Insert constraint c into conflict state.
|
||||
*
|
||||
|
|
@ -182,6 +189,11 @@ namespace polysat {
|
|||
*/
|
||||
void insert(signed_constraint c);
|
||||
|
||||
/**
|
||||
* Insert constraint c that is justified by the given lemma.
|
||||
*/
|
||||
void insert(signed_constraint c, clause_ref lemma);
|
||||
|
||||
/** Insert assigned variables of c */
|
||||
void insert_vars(signed_constraint c);
|
||||
|
||||
|
|
|
|||
|
|
@ -1,3 +1,4 @@
|
|||
#if 0
|
||||
/*++
|
||||
Copyright (c) 2021 Microsoft Corporation
|
||||
|
||||
|
|
@ -601,3 +602,4 @@ namespace polysat {
|
|||
return m_bvar2mark.get(b, false);
|
||||
}
|
||||
}
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -1,3 +1,4 @@
|
|||
#if 0
|
||||
/*++
|
||||
Copyright (c) 2021 Microsoft Corporation
|
||||
|
||||
|
|
@ -249,3 +250,4 @@ namespace polysat {
|
|||
inline conflict::const_iterator conflict::begin() const { return conflict_iterator::begin(cm(), m_literals); }
|
||||
inline conflict::const_iterator conflict::end() const { return conflict_iterator::end(cm(), m_literals); }
|
||||
}
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -1,3 +1,4 @@
|
|||
#if 0
|
||||
/*++
|
||||
Copyright (c) 2021 Microsoft Corporation
|
||||
|
||||
|
|
@ -69,3 +70,4 @@ namespace polysat {
|
|||
}
|
||||
|
||||
}
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -1,3 +1,4 @@
|
|||
#if 0
|
||||
/*++
|
||||
Copyright (c) 2021 Microsoft Corporation
|
||||
|
||||
|
|
@ -28,3 +29,4 @@ namespace polysat {
|
|||
};
|
||||
|
||||
}
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -1,3 +1,4 @@
|
|||
#if 0
|
||||
/*++
|
||||
Copyright (c) 2021 Microsoft Corporation
|
||||
|
||||
|
|
@ -101,6 +102,14 @@ namespace polysat {
|
|||
core.log_inference(inference_sup("1", v, c2, c1));
|
||||
return l_true;
|
||||
case l_undef:
|
||||
#if 0
|
||||
core.reset();
|
||||
core.insert(c1);
|
||||
core.insert(c2);
|
||||
core.insert(~c);
|
||||
core.log_inference(inference_sup("1b", v, c2, c1));
|
||||
return l_true;
|
||||
#else
|
||||
SASSERT(premises.empty());
|
||||
// Ensure that c is assigned and justified
|
||||
premises.push_back(c1);
|
||||
|
|
@ -115,6 +124,7 @@ namespace polysat {
|
|||
SASSERT_EQ(l_true, c.bvalue(s));
|
||||
SASSERT(c.is_currently_false(s));
|
||||
break;
|
||||
#endif
|
||||
default:
|
||||
break;
|
||||
}
|
||||
|
|
@ -235,3 +245,4 @@ namespace polysat {
|
|||
}
|
||||
|
||||
}
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -1,3 +1,4 @@
|
|||
#if 0
|
||||
/*++
|
||||
Copyright (c) 2021 Microsoft Corporation
|
||||
|
||||
|
|
@ -44,3 +45,4 @@ namespace polysat {
|
|||
};
|
||||
|
||||
}
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -60,8 +60,9 @@ namespace polysat {
|
|||
for (auto const& c : core) {
|
||||
sat::literal const lit = c.blit();
|
||||
out_indent() << lit << ": " << c << '\n';
|
||||
// TODO: if justified by a side lemma, print it here
|
||||
// out_indent() << " justified by: " << lemma << '\n';
|
||||
clause* lemma = core.side_lemma(lit);
|
||||
if (lemma)
|
||||
out_indent() << " justified by: " << lemma << '\n';
|
||||
m_used_constraints.insert(lit.index());
|
||||
for (pvar v : c->vars())
|
||||
m_used_vars.insert(v);
|
||||
|
|
|
|||
|
|
@ -109,7 +109,7 @@ namespace polysat {
|
|||
// hi < lo <= lo' <= hi'
|
||||
if (lo_val() <= other.lo_val() && other.lo_val() <= other.hi_val())
|
||||
return true;
|
||||
// lo' <= hi' <= hi < lo
|
||||
// lo' <= hi' <= hi < lo
|
||||
if (other.lo_val() <= other.hi_val() && other.hi_val() <= hi_val())
|
||||
return true;
|
||||
// hi' <= hi < lo <= lo'
|
||||
|
|
|
|||
|
|
@ -1,3 +1,4 @@
|
|||
#if 0
|
||||
/*++
|
||||
Copyright (c) 2021 Microsoft Corporation
|
||||
|
||||
|
|
@ -486,3 +487,4 @@ namespace polysat {
|
|||
}
|
||||
|
||||
}
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -1,3 +1,4 @@
|
|||
#if 0
|
||||
/*++
|
||||
Copyright (c) 2021 Microsoft Corporation
|
||||
|
||||
|
|
@ -110,3 +111,4 @@ namespace polysat {
|
|||
*/
|
||||
|
||||
}
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -17,9 +17,7 @@ Author:
|
|||
--*/
|
||||
|
||||
#include "math/polysat/solver.h"
|
||||
#include "math/polysat/explain.h"
|
||||
#include "math/polysat/log.h"
|
||||
#include "math/polysat/variable_elimination.h"
|
||||
#include "math/polysat/polysat_params.hpp"
|
||||
|
||||
// For development; to be removed once the linear solver works well enough
|
||||
|
|
|
|||
|
|
@ -22,9 +22,8 @@ namespace polysat {
|
|||
// and kick out all other constraints.
|
||||
for (signed_constraint c : core) {
|
||||
if (!c->contains_var(v) && c.is_currently_false(s)) {
|
||||
core.reset();
|
||||
core.set(c);
|
||||
core.log_inference("ve_reduction");
|
||||
core.logger().log("ve_reduction");
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -635,7 +635,6 @@ namespace polysat {
|
|||
auto* e = m_units[v];
|
||||
entry* first = e;
|
||||
SASSERT(e);
|
||||
core.reset();
|
||||
do {
|
||||
// Build constraint: upper bound of each interval is not contained in the next interval,
|
||||
// using the equivalence: t \in [l;h[ <=> t-l < h-l
|
||||
|
|
@ -670,16 +669,13 @@ namespace polysat {
|
|||
core.logger().log(inf_fi(*this, v));
|
||||
|
||||
// TODO: should not be here, too general
|
||||
/*
|
||||
for (auto c : core) {
|
||||
if (c.bvalue(s) == l_false) {
|
||||
core.reset();
|
||||
core.set(~c);
|
||||
core.logger().log("");
|
||||
break;
|
||||
}
|
||||
}
|
||||
*/
|
||||
|
||||
return true;
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue