mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-22 11:07:51 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-12-12 15:42:39 -08:00
parent e0effa3775
commit c663d28201
4 changed files with 13 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/sat/smt/polysat/core.cpp
View file

@ -149,13 +149,14 @@ namespace polysat {
m_var = m_var_queue.next_var();
s.trail().push(mk_dqueue_var(m_var, *this));
switch (m_viable.find_viable(m_var, m_value)) {
case find_t::empty:
s.set_lemma(m_viable.get_core(), 0, m_viable.explain());
// propagate_unsat_core();
case find_t::empty:
s.set_lemma(m_viable.get_core(), m_viable.explain());
// propagate_unsat_core();
return sat::check_result::CR_CONTINUE;
case find_t::singleton:
case find_t::singleton: {
s.propagate(m_constraints.eq(var2pdd(m_var), m_value), m_viable.explain());
return sat::check_result::CR_CONTINUE;
}
case find_t::multiple:
s.add_eq_literal(m_var, m_value);
return sat::check_result::CR_CONTINUE;

2
src/sat/smt/polysat/types.h
View file

@ -107,7 +107,7 @@ namespace polysat {
virtual ~solver_interface() {}
virtual void add_eq_literal(pvar v, rational const& val) = 0;
virtual void set_conflict(dependency_vector const& core) = 0;
virtual void set_lemma(core_vector const& aux_core, unsigned level, dependency_vector const& core) = 0;
virtual void set_lemma(core_vector const& aux_core, dependency_vector const& core) = 0;
virtual void add_polysat_clause(char const* name, core_vector cs, bool redundant) = 0;
virtual dependency propagate(signed_constraint sc, dependency_vector const& deps) = 0;
virtual void propagate(dependency const& d, bool sign, dependency_vector const& deps) = 0;