From fd6fe87c5d9cd059c33a847274aef42af552730b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 22 Mar 2016 15:41:21 -0700
Subject: [PATCH] enable qe-lite for UFNIA benchmarks
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/qe/qsat.cpp | 93 ++++++++++++++++----------
src/qe/qsat.h | 2 +-
src/smt/theory_arith_int.h | 2 +-
src/tactic/smtlogics/quant_tactics.cpp | 2 +
4 files changed, 62 insertions(+), 37 deletions(-)
diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp
index 0a5c40dbd..1b0555b22 100644
--- a/src/qe/qsat.cpp
+++ b/src/qe/qsat.cpp
@@ -500,40 +500,40 @@ namespace qe {
}
}
- class kernel {
- ast_manager& m;
- smt_params m_smtp;
- smt::kernel m_kernel;
-
- public:
- kernel(ast_manager& m):
- m(m),
- m_kernel(m, m_smtp)
- {
- m_smtp.m_model = true;
- m_smtp.m_relevancy_lvl = 0;
- m_smtp.m_case_split_strategy = CS_ACTIVITY_WITH_CACHE;
+ class kernel {
+ ast_manager& m;
+ smt_params m_smtp;
+ smt::kernel m_kernel;
+
+ public:
+ kernel(ast_manager& m):
+ m(m),
+ m_kernel(m, m_smtp)
+ {
+ m_smtp.m_model = true;
+ m_smtp.m_relevancy_lvl = 0;
+ m_smtp.m_case_split_strategy = CS_ACTIVITY_WITH_CACHE;
+ }
+
+ smt::kernel& k() { return m_kernel; }
+ smt::kernel const& k() const { return m_kernel; }
+
+ void assert_expr(expr* e) {
+ m_kernel.assert_expr(e);
+ }
+
+ void get_core(expr_ref_vector& core) {
+ unsigned sz = m_kernel.get_unsat_core_size();
+ core.reset();
+ for (unsigned i = 0; i < sz; ++i) {
+ core.push_back(m_kernel.get_unsat_core_expr(i));
}
-
- smt::kernel& k() { return m_kernel; }
- smt::kernel const& k() const { return m_kernel; }
-
- void assert_expr(expr* e) {
- m_kernel.assert_expr(e);
- }
-
- void get_core(expr_ref_vector& core) {
- unsigned sz = m_kernel.get_unsat_core_size();
- core.reset();
- for (unsigned i = 0; i < sz; ++i) {
- core.push_back(m_kernel.get_unsat_core_expr(i));
- }
- TRACE("qe", tout << "core: " << core << "\n";
- m_kernel.display(tout);
- tout << "\n";
- );
- }
- };
+ TRACE("qe", tout << "core: " << core << "\n";
+ m_kernel.display(tout);
+ tout << "\n";
+ );
+ }
+ };
class qsat : public tactic {
@@ -1168,6 +1168,7 @@ namespace qe {
pred_abs m_pred_abs;
qe::mbp m_mbp;
kernel m_kernel;
+ vector<app_ref_vector> m_vars;
imp(ast_manager& m):
m(m),
@@ -1180,14 +1181,36 @@ namespace qe {
m_fmls.push_back(e);
}
- lbool check(svector<bool> const& is_max, func_decl_ref_vector const& vars, app* t) {
+ lbool check(svector<bool> const& is_max, app_ref_vector const& vars, app* t) {
// Assume this is the only call to check.
expr_ref_vector defs(m);
+ app_ref_vector free_vars(m), vars1(m);
expr_ref fml = mk_and(m_fmls);
+ m_pred_abs.get_free_vars(fml, free_vars);
m_pred_abs.abstract_atoms(fml, defs);
fml = m_pred_abs.mk_abstract(fml);
m_kernel.assert_expr(mk_and(defs));
m_kernel.assert_expr(fml);
+ obj_hashtable<app> var_set;
+ for (unsigned i = 0; i < vars.size(); ++i) {
+ var_set.insert(vars[i]);
+ }
+ for (unsigned i = 0; i < free_vars.size(); ++i) {
+ app* v = free_vars[i].get();
+ if (!var_set.contains(v)) {
+ vars1.push_back(v);
+ }
+ }
+ bool is_m = is_max[0];
+ for (unsigned i = 0; i < vars.size(); ++i) {
+ if (is_m != is_max[i]) {
+ m_vars.push_back(vars1);
+ vars1.reset();
+ is_m = is_max[i];
+ }
+ vars1.push_back(vars[i]);
+ }
+
// TBD
return l_undef;
@@ -1212,7 +1235,7 @@ namespace qe {
}
}
- lbool min_max_opt::check(svector<bool> const& is_max, func_decl_ref_vector const& vars, app* t) {
+ lbool min_max_opt::check(svector<bool> const& is_max, app_ref_vector const& vars, app* t) {
return m_imp->check(is_max, vars, t);
}
diff --git a/src/qe/qsat.h b/src/qe/qsat.h
index 91b370294..5c6b80a04 100644
--- a/src/qe/qsat.h
+++ b/src/qe/qsat.h
@@ -121,7 +121,7 @@ namespace qe {
~min_max_opt();
void add(expr* e);
void add(expr_ref_vector const& fmls);
- lbool check(svector<bool> const& is_max, func_decl_ref_vector const& vars, app* t);
+ lbool check(svector<bool> const& is_max, app_ref_vector const& vars, app* t);
};
diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h
index 72e1f1bc2..8f209b96b 100644
--- a/src/smt/theory_arith_int.h
+++ b/src/smt/theory_arith_int.h
@@ -1308,7 +1308,7 @@ namespace smt {
if (!gcd_test())
return FC_CONTINUE;
- if (m_params.m_arith_euclidean_solver)
+ if (m_params.m_arith_euclidean_solver || (0 == (1 + m_branch_cut_counter) % 80))
apply_euclidean_solver();
if (get_context().inconsistent())
diff --git a/src/tactic/smtlogics/quant_tactics.cpp b/src/tactic/smtlogics/quant_tactics.cpp
index 13a790e93..f501ed75a 100644
--- a/src/tactic/smtlogics/quant_tactics.cpp
+++ b/src/tactic/smtlogics/quant_tactics.cpp
@@ -22,6 +22,7 @@ Revision History:
#include"solve_eqs_tactic.h"
#include"elim_uncnstr_tactic.h"
#include"qe_tactic.h"
+#include"qe_lite.h"
#include"qsat.h"
#include"nlqsat.h"
#include"ctx_simplify_tactic.h"
@@ -61,6 +62,7 @@ static tactic * mk_no_solve_eq_preprocessor(ast_manager & m) {
tactic * mk_ufnia_tactic(ast_manager & m, params_ref const & p) {
tactic * st = and_then(mk_no_solve_eq_preprocessor(m),
+ mk_qe_lite_tactic(m, p),
mk_smt_tactic());
st->updt_params(p);
return st;