mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 20:33:38 +00:00
Code Activity

apply

Browse source
This commit is contained in:
Jakob Rath 2022-08-22 12:44:56 +02:00
parent bf1a7914cd
commit 53f276d225
4 changed files with 13 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/math/polysat/simplify_clause.cpp
View file

@ -21,4 +21,9 @@ namespace polysat {
s(s) s(s)
{} {}
bool simplify_clause::apply(clause& cl)
{
(void)s;
return false;
}
} }

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

@ -22,6 +22,8 @@ namespace polysat {
public: public:
simplify_clause(solver& s); simplify_clause(solver& s);
bool apply(clause& cl);
}; };
} }

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

@ -12,7 +12,7 @@ Abstract:
Author: Author:
Nikolaj Bjorner (nbjorner) 2021-03-19 Nikolaj Bjorner (nbjorner) 2021-03-19
Jakob Rath 2021-04-6 Jakob Rath 2021-04-06
--*/ --*/
@ -33,6 +33,7 @@ namespace polysat {
m_viable_fallback(*this), m_viable_fallback(*this),
m_linear_solver(*this), m_linear_solver(*this),
m_conflict(*this), m_conflict(*this),
m_simplify_clause(*this),
m_simplify(*this), m_simplify(*this),
m_restart(*this), m_restart(*this),
m_bvars(), m_bvars(),
@ -825,6 +826,7 @@ namespace polysat {
void solver::learn_lemma(clause& lemma) { void solver::learn_lemma(clause& lemma) {
LOG("Learning: "<< lemma); LOG("Learning: "<< lemma);
SASSERT(!lemma.empty()); SASSERT(!lemma.empty());
m_simplify_clause.apply(lemma);
add_clause(lemma); add_clause(lemma);
// TODO: add pwatch? // TODO: add pwatch?
} }

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

@ -24,6 +24,7 @@ Author:
#include "math/polysat/conflict.h" #include "math/polysat/conflict.h"
#include "math/polysat/constraint.h" #include "math/polysat/constraint.h"
#include "math/polysat/clause_builder.h" #include "math/polysat/clause_builder.h"
#include "math/polysat/simplify_clause.h"
#include "math/polysat/simplify.h" #include "math/polysat/simplify.h"
#include "math/polysat/restart.h" #include "math/polysat/restart.h"
#include "math/polysat/explain.h" #include "math/polysat/explain.h"
@ -69,6 +70,7 @@ namespace polysat {
friend class clause_builder; friend class clause_builder;
friend class conflict; friend class conflict;
friend class conflict_explainer; friend class conflict_explainer;
friend class simplify_clause;
friend class simplify; friend class simplify;
friend class restart; friend class restart;
friend class explainer; friend class explainer;
@ -99,6 +101,7 @@ namespace polysat {
viable_fallback m_viable_fallback; // fallback for viable, using bitblasting over univariate constraints viable_fallback m_viable_fallback; // fallback for viable, using bitblasting over univariate constraints
linear_solver m_linear_solver; linear_solver m_linear_solver;
conflict m_conflict; conflict m_conflict;
simplify_clause m_simplify_clause;
simplify m_simplify; simplify m_simplify;
restart m_restart; restart m_restart;
bool_var_manager m_bvars; // Map boolean variables to constraints bool_var_manager m_bvars; // Map boolean variables to constraints