From 6145ccc077464698235f2c01cbdde1513377b2dd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 12 Oct 2012 17:34:23 -0700 Subject: [PATCH 1/2] Added tactic for qfnra purely based on nlsat Signed-off-by: Leonardo de Moura --- lib/install_tactics.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/lib/install_tactics.cpp b/lib/install_tactics.cpp index 629e25389..36de7be76 100644 --- a/lib/install_tactics.cpp +++ b/lib/install_tactics.cpp @@ -70,6 +70,7 @@ Notes: #include"qfbv_tactic.h" #include"subpaving_tactic.h" #include"unit_subsumption_tactic.h" +#include"qfnra_nlsat_tactic.h" MK_SIMPLE_TACTIC_FACTORY(simplifier_fct, mk_simplify_tactic(m, p)); MK_SIMPLE_TACTIC_FACTORY(split_clause_fct, mk_split_clause_tactic(p)); @@ -193,6 +194,7 @@ void install_tactics(tactic_manager & ctx) { ADD_TACTIC_CMD("qflra", "builtin strategy for solving QF_LRA problems.", qflra_fct); ADD_TACTIC_CMD("qfnia", "builtin strategy for solving QF_NIA problems.", qfnia_fct); ADD_TACTIC_CMD("qfnra", "builtin strategy for solving QF_NRA problems.", qfnra_fct); + ADD_TACTIC_CMD("qfnra-nlsat", "builtin strategy for solving QF_NRA problems using only nlsat.", qfnra_nlsat_fct); ADD_TACTIC_CMD("qfbv", "builtin strategy for solving QF_BV problems.", qfbv_fct); #ifndef _EXTERNAL_RELEASE ADD_TACTIC_CMD("subpaving", "tactic for testing subpaving module.", subpaving_fct); From bccf07be0b4b8b2610b1128b5c2456bcfbea2e0e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 13 Oct 2012 09:11:54 -0700 Subject: [PATCH 2/2] fixed bug in unsat core generation Signed-off-by: Leonardo de Moura --- lib/asserted_formulas.cpp | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/lib/asserted_formulas.cpp b/lib/asserted_formulas.cpp index 86907adb3..6f7d8827e 100644 --- a/lib/asserted_formulas.cpp +++ b/lib/asserted_formulas.cpp @@ -873,11 +873,18 @@ bool asserted_formulas::solve_core() { } void asserted_formulas::solve() { + // This method is buggy when unsatisfiable cores are enabled. + // It may eliminate answer literals. + // Since I will remove asserted_formulas.cpp in the future, I just disabled it. + // Note: asserted_formulas.cpp is based on the obsolete preprocessing stack. + // Users should the solve-eqs tactic if they want to eliminate variables. +#if 0 while (solve_core()) { IF_IVERBOSE(10, verbose_stream() << "reducing...\n";); flush_cache(); // collect garbage reduce_asserted_formulas(); } +#endif } void asserted_formulas::reduce_asserted_formulas() {