mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

add simple bounded CLP backend

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-04-26 16:10:46 -07:00
parent 8038c719fb
commit 65b52ba3e9
3 changed files with 41 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

34
src/muz_qe/dl_context.cpp
View file

@ -547,6 +547,8 @@ namespace datalog {
throw default_exception("get_num_levels is not supported for bmc");
case TAB_ENGINE:
throw default_exception("get_num_levels is not supported for tab");
case CLP_ENGINE:
throw default_exception("get_num_levels is not supported for clp");
default:
throw default_exception("unknown engine");
}
@ -565,6 +567,8 @@ namespace datalog {
throw default_exception("operation is not supported for BMC engine");
case TAB_ENGINE:
throw default_exception("operation is not supported for TAB engine");
case CLP_ENGINE:
throw default_exception("operation is not supported for CLP engine");
default:
throw default_exception("unknown engine");
}
@ -584,6 +588,8 @@ namespace datalog {
throw default_exception("operation is not supported for BMC engine");
case TAB_ENGINE:
throw default_exception("operation is not supported for TAB engine");
case CLP_ENGINE:
throw default_exception("operation is not supported for CLP engine");
default:
throw default_exception("unknown engine");
}
@ -711,6 +717,10 @@ namespace datalog {
check_existential_tail(r);
check_positive_predicates(r);
break;
case CLP_ENGINE:
check_existential_tail(r);
check_positive_predicates(r);
break;
default:
UNREACHABLE();
break;
@ -984,6 +994,9 @@ namespace datalog {
else if (e == symbol("tab")) {
m_engine = TAB_ENGINE;
}
else if (e == symbol("clp")) {
m_engine = CLP_ENGINE;
}
if (m_engine == LAST_ENGINE) {
expr_fast_mark1 mark;
@ -1019,6 +1032,8 @@ namespace datalog {
return bmc_query(query);
case TAB_ENGINE:
return tab_query(query);
case CLP_ENGINE:
return clp_query(query);
default:
UNREACHABLE();
return rel_query(query);
@ -1083,11 +1098,22 @@ namespace datalog {
}
}
void context::ensure_clp() {
if (!m_clp.get()) {
m_clp = alloc(clp, *this);
}
}
lbool context::tab_query(expr* query) {
ensure_tab();
return m_tab->query(query);
}
lbool context::clp_query(expr* query) {
ensure_clp();
return m_clp->query(query);
}
void context::ensure_rel() {
if (!m_rel.get()) {
m_rel = alloc(rel_context, *this);
@ -1128,6 +1154,10 @@ namespace datalog {
ensure_tab();
m_last_answer = m_tab->get_answer();
return m_last_answer.get();
case CLP_ENGINE:
ensure_clp();
m_last_answer = m_clp->get_answer();
return m_last_answer.get();
default:
UNREACHABLE();
}
@ -1153,6 +1183,10 @@ namespace datalog {
ensure_tab();
m_tab->display_certificate(out);
return true;
case CLP_ENGINE:
ensure_clp();
m_clp->display_certificate(out);
return true;
default:
return false;
}

7
src/muz_qe/dl_context.h
View file

@ -47,7 +47,7 @@ Revision History:
#include"dl_rule_transformer.h"
#include"expr_abstract.h"
#include"expr_functors.h"
#include"clp_context.h"
namespace datalog {
@ -124,6 +124,7 @@ namespace datalog {
scoped_ptr<bmc> m_bmc;
scoped_ptr<rel_context> m_rel;
scoped_ptr<tab> m_tab;
scoped_ptr<clp> m_clp;
bool m_closed;
bool m_saturation_was_run;
@ -477,6 +478,8 @@ namespace datalog {
void ensure_tab();
void ensure_clp();
void ensure_rel();
void new_query();
@ -489,6 +492,8 @@ namespace datalog {
lbool tab_query(expr* query);
lbool clp_query(expr* query);
void check_quantifier_free(rule_ref& r);
void check_uninterpreted_free(rule_ref& r);
void check_existential_tail(rule_ref& r);

1
src/muz_qe/dl_util.h
View file

@ -54,6 +54,7 @@ namespace datalog {
BMC_ENGINE,
QBMC_ENGINE,
TAB_ENGINE,
CLP_ENGINE,
LAST_ENGINE
};