mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-06 11:02:44 +00:00
Code Activity

add trace tag for levelwise

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-08-14 17:12:09 -07:00
parent 1066f3ea3b
commit f46cc6814a
5 changed files with 23 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/nlsat/nlsat_solver.cpp
View file

@ -39,6 +39,7 @@ Revision History:
#include "nlsat/nlsat_simplify.h"
#include "nlsat/nlsat_simple_checker.h"
#include "nlsat/nlsat_variable_ordering_strategy.h"
#include "nlsat_solver.h"
#define NLSAT_EXTRA_VERBOSE
@ -4347,10 +4348,14 @@ namespace nlsat {
nlsat_params::collect_param_descrs(d);
}
unsynch_mpq_manager & solver::qm() {
const assignment &solver::get_assignment() const {
return m_imp->m_assignment;
}
unsynch_mpq_manager &solver::qm()
{
return m_imp->m_qm;
}
anum_manager & solver::am() {
return m_imp->m_am;
}