mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-14 21:05:39 +00:00
Code Activity

clean up (#7844)

Browse source
This commit is contained in:
ValentinPromies 2025-09-03 18:52:51 +02:00 • committed by GitHub
parent 187f013224
commit 4fec287107
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 22 additions and 37 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/nlsat/nlsat_solver.cpp
View file

@ -2034,7 +2034,7 @@ namespace nlsat {
m_assignment.reset();
}
lbool check(assignment const& rvalues, atom_vector& core, literal_vector& cell) {
lbool check(assignment const& rvalues, literal_vector& clause) {
// temporarily set m_assignment to the given one
assignment tmp = m_assignment;
m_assignment.reset();
@ -2076,21 +2076,16 @@ namespace nlsat {
// assignment does not satisfy the constraints -> create lemma
SASSERT(best_literal != null_literal);
cell.reset();
clause.reset();
m_lazy_clause.reset();
m_explain.set_linear_project(true);
m_explain.main_operator(1, &best_literal, m_lazy_clause);
m_explain.set_linear_project(false);
for (auto l : m_lazy_clause) {
cell.push_back(l);
clause.push_back(l);
}
m_lemma_assumptions = nullptr;
core.clear();
SASSERT(!best_literal.sign());
core.push_back(m_atoms[best_literal.var()]);
clause.push_back(~best_literal);
m_assignment.reset();
m_assignment.copy(tmp);
@ -4167,8 +4162,8 @@ namespace nlsat {
return m_imp->check(assumptions);
}
lbool solver::check(assignment const& rvalues, atom_vector& clause, literal_vector& cell) {
return m_imp->check(rvalues, clause, cell);
lbool solver::check(assignment const& rvalues, literal_vector& clause) {
return m_imp->check(rvalues, clause);
}
void solver::get_core(vector<assumption, false>& assumptions) {

11
src/nlsat/nlsat_solver.h
View file

@ -222,15 +222,14 @@ namespace nlsat {
// check satisfiability of asserted formulas relative to state of the nlsat solver.
// produce either,
// l_true - a model is available (rvalues can be ignored) or,
// l_false - the conjunction of literals from get_core, and negations of atoms in clause,
// such that the conjunction of the assumptions and the polynomials in core is unsatisfiable.
// l_false - a clause (not core v not cell) excluding a cell around rvalues if core (consisting of atoms
// passed to nlsat) is asserted.
// l_undef - if the search was interrupted by a resource limit.
// clause is a list of atoms. Their negations conjoined with core literals are unsatisfiable.
// Different implementations of check are possible. One where core comprises of linear polynomials could
// clause is a list of literals. Their disjunction is valid.
// Different implementations of check are possible. One where cell comprises of linear polynomials could
// produce lemmas that are friendly to linear arithmetic solvers.
// TODO: update
//
lbool check(assignment const& rvalues, atom_vector& clause, literal_vector& cell);
lbool check(assignment const& rvalues, literal_vector& clause);
// -----------------------
//