mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-09 02:25:38 +00:00
Code Activity

remove references to linear propagate

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-03-20 09:20:00 +01:00
parent 3dbca1042c
commit da782a9dc7
2 changed files with 1 additions and 35 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -29,7 +29,6 @@ Author:
#include "math/polysat/restart.h"
#include "math/polysat/ule_constraint.h"
#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"
@ -149,7 +148,6 @@ namespace polysat {
mutable scoped_ptr_vector<dd::pdd_manager> m_pdd;
viable m_viable; // viable sets per variable
viable_fallback m_viable_fallback; // fallback for viable, using bitblasting over univariate constraints
linear_solver m_linear_solver;
conflict m_conflict;
simplify_clause m_simplify_clause;
simplify m_simplify;
@ -295,7 +293,6 @@ namespace polysat {
void bdecide();
void pdecide(pvar v);
void linear_propagate();
bool is_conflict() const { return !m_conflict.empty(); }
bool at_base_level() const;