mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 01:24:08 +00:00
Code Activity

enable logging nla lemmas

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-04-25 10:29:34 -04:00
parent 2a4f0e785b
commit bebcd94703
5 changed files with 37 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/ast/sls/bv_sls_eval.h
View file

@ -25,6 +25,12 @@ namespace bv {
class sls_fixed;
class sls_eval_plugin {
public:
virtual ~sls_eval_plugin() {}
};
class sls_eval {
struct config {
unsigned m_prob_randomize_extract = 50;
@ -40,6 +46,8 @@ namespace bv {
random_gen m_rand;
config m_config;
scoped_ptr_vector<sls_eval_plugin> m_plugins;
scoped_ptr_vector<sls_valuation> m_values; // expr-id -> bv valuation

22
src/math/lp/nra_solver.cpp
View file

@ -3,6 +3,10 @@
Author: Nikolaj Bjorner, Lev Nachmanson
*/
#ifndef SINGLE_THREAD
#include <thread>
#endif
#include <fstream>
#include "math/lp/lar_solver.h"
#include "math/lp/nra_solver.h"
#include "nlsat/nlsat_solver.h"
@ -11,6 +15,7 @@
#include "util/map.h"
#include "util/uint_set.h"
#include "math/lp/nla_core.h"
#include "smt/params/smt_params_helper.hpp"
namespace nra {
@ -157,6 +162,23 @@ struct solver::imp {
TRACE("nra", m_nlsat->display(tout));
smt_params_helper p(m_params);
if (p.arith_nl_log()) {
static unsigned id = 0;
std::stringstream strm;
#ifndef SINGLE_THREAD
std::thread::id this_id = std::this_thread::get_id();
strm << "nla_" << this_id << "." << (++id) << ".smt2";
#else
strm << "nla_" << (++id) << ".smt2";
#endif
std::ofstream out(strm.str());
m_nlsat->display_smt2(out);
out << "(check-sat)\n";
out.close();
}
lbool r = l_undef;
try {
r = m_nlsat->check();

4
src/nlsat/nlsat_solver.cpp
View file

@ -3863,6 +3863,10 @@ namespace nlsat {
return out;
}
std::ostream& solver::display_smt2(std::ostream & out) const {
return m_imp->display_smt2(out);
}
std::ostream& solver::display_smt2(std::ostream & out, literal_vector const& ls) const {
return display_smt2(out, ls.size(), ls.data());
}

2
src/nlsat/nlsat_solver.h
View file

@ -254,6 +254,8 @@ namespace nlsat {
std::ostream& display_smt2(std::ostream & out, literal_vector const& ls) const;
std::ostream& display_smt2(std::ostream & out) const;
/**
\brief Display variable

1
src/smt/params/smt_params_helper.pyg
View file

@ -83,6 +83,7 @@ def_module_params(module_name='smt',
('arith.nl.propagate_linear_monomials', BOOL, True, 'propagate linear monomials'),
('arith.nl.optimize_bounds', BOOL, True, 'enable bounds optimization'),
('arith.nl.cross_nested', BOOL, True, 'enable cross-nested consistency checking'),
('arith.nl.log', BOOL, False, 'Log lemmas sent to nra solver'),
('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'),
('arith.propagation_mode', UINT, 1, '0 - no propagation, 1 - propagate existing literals, 2 - refine finite bounds'),
('arith.branch_cut_ratio', UINT, 2, 'branch/cut ratio for linear integer arithmetic'),