mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 12:53:38 +00:00
Code Activity

improve clp solver

Browse source 
- run default rule transformations
 - sort a predicate's rules by number of queries in the body to bias search

Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
This commit is contained in:
Nuno Lopes 2013-05-21 10:48:55 -07:00
parent 56dedec740
commit dc91a754dd
1 changed files with 12 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/muz_qe/clp_context.cpp
View file

@ -66,9 +66,10 @@ namespace datalog {
m_ctx.ensure_opened(); m_ctx.ensure_opened();
m_solver.reset(); m_solver.reset();
m_goals.reset(); m_goals.reset();
rm.mk_query(query, m_ctx.get_rules()); func_decl *head_decl = rm.mk_query(query, m_ctx.get_rules());
expr_ref head(m); m_ctx.apply_default_transformation();
head = m_ctx.get_rules().last()->get_head();
expr_ref head(m_ctx.get_rules().get_predicate_rules(head_decl)[0]->get_head(), m);
ground(head); ground(head);
m_goals.push_back(to_app(head)); m_goals.push_back(to_app(head));
return search(20, 0); return search(20, 0);
@ -125,6 +126,10 @@ namespace datalog {
m_var_subst(e, m_ground.size(), m_ground.c_ptr(), e); m_var_subst(e, m_ground.size(), m_ground.c_ptr(), e);
} }
static bool rule_sort_fn(const rule *r1, const rule *r2) {
return r1->get_uninterpreted_tail_size() < r2->get_uninterpreted_tail_size();
}
lbool search(unsigned depth, unsigned index) { lbool search(unsigned depth, unsigned index) {
if (index == m_goals.size()) { if (index == m_goals.size()) {
return l_true; return l_true;
@ -135,7 +140,10 @@ namespace datalog {
IF_VERBOSE(1, verbose_stream() << "search " << depth << " " << index << "\n";); IF_VERBOSE(1, verbose_stream() << "search " << depth << " " << index << "\n";);
unsigned num_goals = m_goals.size(); unsigned num_goals = m_goals.size();
app* head = m_goals[index].get(); app* head = m_goals[index].get();
rule_vector const& rules = m_ctx.get_rules().get_predicate_rules(head->get_decl());
rule_vector rules(m_ctx.get_rules().get_predicate_rules(head->get_decl()));
std::stable_sort(rules.begin(), rules.end(), rule_sort_fn);
lbool status = l_false; lbool status = l_false;
for (unsigned i = 0; i < rules.size(); ++i) { for (unsigned i = 0; i < rules.size(); ++i) {
rule* r = rules[i]; rule* r = rules[i];