mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

remove another cm

Browse source
This commit is contained in:
Jakob Rath 2021-09-12 16:08:24 +02:00
parent a8c132f769
commit 00cc81d1a4
3 changed files with 2 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/polysat/explain.cpp
View file

@ -17,8 +17,6 @@ Author:
namespace polysat {
constraint_manager& explainer::cm() { return s().m_constraints; }
signed_constraint ex_polynomial_superposition::resolve1(pvar v, signed_constraint c1, signed_constraint c2) {
// c1 is true, c2 is false
SASSERT(c1.is_currently_true(s()));
@ -35,7 +33,7 @@ namespace polysat {
// (this condition might be too strict, but we use it for now to prevent looping)
if (b.degree(v) <= r.degree(v))
return {};
signed_constraint c = cm().eq(r);
signed_constraint c = s().eq(r);
LOG("resolved: " << c << " currently false? " << c.is_currently_false(s()));
if (!c.is_currently_false(s()))
return {};

2
src/math/polysat/explain.h
View file

@ -20,7 +20,6 @@ Author:
namespace polysat {
class solver;
class constraint_manager;
class explainer {
friend class conflict_core;
@ -28,7 +27,6 @@ namespace polysat {
void set_solver(solver& s) { m_solver = &s; }
protected:
solver& s() { return *m_solver; }
constraint_manager& cm();
public:
virtual ~explainer() {}
virtual bool try_explain(pvar v, /* vector<signed_constraint> const& cjust_v, */ conflict_core& core) = 0;

1
src/math/polysat/solver.h
View file

@ -62,6 +62,7 @@ namespace polysat {
friend class viable;
friend class assignment_pp;
friend class assignments_pp;
friend class ex_polynomial_superposition;
friend class inf_saturate;
friend class constraint_manager;