mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-31 00:13:16 +00:00
Code Activity

outline of signature for assignment based conflict generation

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-07-11 18:36:28 +02:00
parent 0995928f6e
commit 46284c434a
2 changed files with 19 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/nlsat/nlsat_solver.cpp
View file

@ -2034,6 +2034,10 @@ namespace nlsat {
m_assignment.reset();
}
lbool check(literal_vector& assumptions, assignment const& rvalues, polynomial_ref_vector& core) {
return l_undef;
}
lbool check(literal_vector& assumptions) {
literal_vector result;
unsigned sz = assumptions.size();
@ -4104,6 +4108,10 @@ namespace nlsat {
return m_imp->check(assumptions);
}
lbool solver::check(literal_vector& assumptions, assignment const& rvalues, polynomial_ref_vector& core) {
return m_imp->check(assumptions, rvalues, core);
}
void solver::get_core(vector<assumption, false>& assumptions) {
return m_imp->get_core(assumptions);
}

11
src/nlsat/nlsat_solver.h
View file

@ -218,6 +218,17 @@ namespace nlsat {
lbool check(literal_vector& assumptions);
// check satisfiability of asserted formulas relative to assumptions.
// produce either,
// l_true - a model is availabe (rvalues can be ignored) or,
// l_false - update the list of assumptions (possibly reset it to empty), and a set of polynomials in core,
// such that the conjunction of the assumptions and the polynomials in core is unsatisfiable.
// l_undef - if the search was interrupted by a resource limit.
// We associate literals with the polynomials in the core based on their sign with respect to rvalues.
// If p(rvalues) > 0, then the literal is p <= 0, p(rvalues) < 0, then p(rvalues) >= 0, and p(rvalues) = 0, then p != 0.
//
lbool check(literal_vector& assumptions, assignment const& rvalues, polynomial_ref_vector& core);
// -----------------------
//
// Model