From 680c28d083e46425ef5603214ece86529487cac1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 20 Mar 2016 16:34:04 -0700 Subject: [PATCH] remove nnf conversion which breaks NRA property Signed-off-by: Nikolaj Bjorner --- src/nlsat/nlsat_solver.cpp | 2 +- src/tactic/smtlogics/nra_tactic.cpp | 27 +++++++++++---------------- 2 files changed, 12 insertions(+), 17 deletions(-) diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 40177bb08..ae3f1252b 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -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; diff --git a/src/tactic/smtlogics/nra_tactic.cpp b/src/tactic/smtlogics/nra_tactic.cpp index 4098cd6c1..063e0775a 100644 --- a/src/tactic/smtlogics/nra_tactic.cpp +++ b/src/tactic/smtlogics/nra_tactic.cpp @@ -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)) + )); }