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

adjusting new tactics

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-03-20 10:13:23 -07:00
parent f0bdcbb3db
commit 92b5aac12a
4 changed files with 13 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/nlsat/nlsat_types.h
View file

@ -115,12 +115,13 @@ namespace nlsat {
switch (k) {
case atom::kind::EQ: return out << "=";
case atom::kind::LT: return out << "<";
case atom::kind::GT: return out << ">";
case atom::kind::ROOT_EQ: return out << "= root";
case atom::kind::ROOT_LT: return out << "< root";
case atom::kind::ROOT_LE: return out << "<= root";
case atom::kind::ROOT_GT: return out << "> root";
case atom::kind::ROOT_GE: return out << ">= root";
default: UNREACHABLE();
default: return out << (int)k;
}
return out;
}

6
src/nlsat/tactic/goal2nlsat.cpp
View file

@ -29,7 +29,7 @@ Notes:
#include"expr2var.h"
#include"arith_decl_plugin.h"
#include"tactic.h"
#include"ast_smt2_pp.h"
#include"ast_pp.h"
#include"polynomial.h"
#include"algebraic_numbers.h"
@ -126,7 +126,7 @@ struct goal2nlsat::imp {
m_qm.neg(d2);
polynomial_ref p(m_pm);
p = m_pm.addmul(d1, m_pm.mk_unit(), p1, d2, m_pm.mk_unit(), p2);
TRACE("goal2nlsat_bug", tout << "p: " << p << "\nk: " << k << "\n";);
TRACE("goal2nlsat_bug", tout << mk_pp(f, m) << " p: " << p << "\nk: " << k << "\n";);
if (is_const(p)) {
int sign;
if (is_zero(p))
@ -194,7 +194,7 @@ struct goal2nlsat::imp {
switch (to_app(f)->get_decl_kind()) {
case OP_TRUE:
case OP_FALSE:
TRACE("goal2nlsat", tout << "f: " << mk_ismt2_pp(f, m) << "\n";);
TRACE("goal2nlsat", tout << "f: " << mk_pp(f, m) << "\n";);
throw tactic_exception("apply simplify before applying nlsat");
case OP_AND:
case OP_OR:

7
src/qe/nlqsat.cpp
View file

@ -30,6 +30,7 @@ Revision History:
#include "ast_util.h"
#include "tseitin_cnf_tactic.h"
#include "expr_safe_replace.h"
#include "ast_pp.h"
namespace qe {
@ -285,6 +286,7 @@ namespace qe {
}
nlsat::var_vector vs;
m_solver.vars(l, vs);
TRACE("qe", m_solver.display(tout, l); tout << "\n";);
for (unsigned i = 0; i < vs.size(); ++i) {
level.merge(m_rvar2level[vs[i]]);
}
@ -542,15 +544,20 @@ namespace qe {
}
else if (m_t2x.is_var(v)) {
nlsat::var w = m_t2x.to_var(v);
TRACE("qe", tout << mk_pp(v, m) << " |-> " << w << "\n";);
m_bound_rvars.back().push_back(w);
m_rvar2level.setx(w, lvl, max_level());
}
else {
TRACE("qe", tout << mk_pp(v, m) << " not found\n";);
}
}
}
init_var2expr();
m_is_true = nlsat::literal(m_a2b.to_var(is_true), false);
// insert literals from arithmetical sub-formulas
nlsat::atom_vector const& atoms = m_solver.get_atoms();
TRACE("qe", m_solver.display(tout); );
for (unsigned i = 0; i < atoms.size(); ++i) {
if (atoms[i]) {
get_level(nlsat::literal(i, false));

2
src/tactic/smtlogics/nra_tactic.cpp
View file

@ -38,7 +38,7 @@ tactic * mk_nra_tactic(ast_manager & m, params_ref const& p) {
return and_then(mk_simplify_tactic(m, p),
mk_nnf_tactic(m, p),
mk_propagate_values_tactic(m, p),
mk_qe_lite_tactic(m),
//mk_qe_lite_tactic(m),
mk_qe_tactic(m, p),
cond(mk_is_qfnra_probe(),
or_else(try_for(mk_qfnra_nlsat_tactic(m, p), 5000),