mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
remove nnf conversion which breaks NRA property
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
1a5449c3d4
commit
680c28d083
|
@ -460,7 +460,7 @@ namespace nlsat {
|
|||
|
||||
void del(bool_var b) {
|
||||
SASSERT(m_bwatches[b].empty());
|
||||
SASSERT(m_bvalues[b] == l_undef);
|
||||
//SASSERT(m_bvalues[b] == l_undef);
|
||||
m_num_bool_vars--;
|
||||
m_dead[b] = true;
|
||||
m_atoms[b] = 0;
|
||||
|
|
|
@ -35,22 +35,17 @@ tactic * mk_nra_tactic(ast_manager & m, params_ref const& p) {
|
|||
p2.set_uint("seed", 13);
|
||||
p2.set_bool("factor", false);
|
||||
|
||||
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_tactic(m, p),
|
||||
cond(mk_is_qfnra_probe(),
|
||||
or_else(try_for(mk_qfnra_nlsat_tactic(m, p), 5000),
|
||||
try_for(mk_qfnra_nlsat_tactic(m, p1), 10000),
|
||||
mk_qfnra_nlsat_tactic(m, p2)),
|
||||
#if 1
|
||||
or_else(mk_nlqsat_tactic(m, p),
|
||||
mk_smt_tactic(p))
|
||||
#else
|
||||
mk_smt_tactic(p)
|
||||
#endif
|
||||
));
|
||||
return and_then(
|
||||
mk_simplify_tactic(m, p),
|
||||
mk_propagate_values_tactic(m, p),
|
||||
mk_qe_lite_tactic(m),
|
||||
cond(mk_is_qfnra_probe(),
|
||||
or_else(try_for(mk_qfnra_nlsat_tactic(m, p), 5000),
|
||||
try_for(mk_qfnra_nlsat_tactic(m, p1), 10000),
|
||||
mk_qfnra_nlsat_tactic(m, p2)),
|
||||
or_else(mk_nlqsat_tactic(m, p),
|
||||
mk_smt_tactic(p))
|
||||
));
|
||||
}
|
||||
|
||||
|
||||
|
|
Loading…
Reference in a new issue