mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-23 06:13:40 +00:00
Code Activity

cleanup front end parameters to datalog engine

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-04-16 13:54:41 -07:00
parent a054b099c1
commit de5f1ebe9f
3 changed files with 2 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

19
src/shell/datalog_frontend.cpp
View file

@ -43,17 +43,7 @@ static datalog::context * g_ctx = 0;
static datalog::rule_set * g_orig_rules; static datalog::rule_set * g_orig_rules;
static datalog::instruction_block * g_code; static datalog::instruction_block * g_code;
static datalog::execution_context * g_ectx; static datalog::execution_context * g_ectx;
static smt_params * g_params;
datalog_params::datalog_params():
m_default_table("sparse"),
m_default_table_checked(false)
{}
// void datalog_params::register_params(ini_params& p) {
// p.register_symbol_param("DEFAULT_TABLE", m_default_table, "Datalog engine: default table (sparse)");
// p.register_bool_param("DEFAULT_TABLE_CHECKED", m_default_table_checked, "Wrap default table with a sanity checker");
// }
static void display_statistics( static void display_statistics(
std::ostream& out, std::ostream& out,
@ -61,7 +51,6 @@ static void display_statistics(
datalog::rule_set& orig_rules, datalog::rule_set& orig_rules,
datalog::instruction_block& code, datalog::instruction_block& code,
datalog::execution_context& ex_ctx, datalog::execution_context& ex_ctx,
smt_params& params,
bool verbose bool verbose
) )
{ {
@ -109,7 +98,7 @@ static void display_statistics(
static void display_statistics() { static void display_statistics() {
if (g_ctx) { if (g_ctx) {
display_statistics(std::cout, *g_ctx, *g_orig_rules, *g_code, *g_ectx, *g_params, true); display_statistics(std::cout, *g_ctx, *g_orig_rules, *g_code, *g_ectx, true);
} }
} }
@ -127,7 +116,6 @@ static void on_ctrl_c(int) {
unsigned read_datalog(char const * file) { unsigned read_datalog(char const * file) {
IF_VERBOSE(1, verbose_stream() << "Z3 Datalog Engine\n";); IF_VERBOSE(1, verbose_stream() << "Z3 Datalog Engine\n";);
datalog_params dl_params;
smt_params s_params; smt_params s_params;
ast_manager m; ast_manager m;
g_overall_time.start(); g_overall_time.start();
@ -135,8 +123,6 @@ unsigned read_datalog(char const * file) {
signal(SIGINT, on_ctrl_c); signal(SIGINT, on_ctrl_c);
params_ref params; params_ref params;
params.set_sym("engine", symbol("datalog")); params.set_sym("engine", symbol("datalog"));
params.set_sym("default_table", dl_params.m_default_table);
params.set_bool("default_table_checked", dl_params.m_default_table_checked);
datalog::context ctx(m, s_params, params); datalog::context ctx(m, s_params, params);
datalog::relation_manager & rmgr = ctx.get_rel_context().get_rmanager(); datalog::relation_manager & rmgr = ctx.get_rel_context().get_rmanager();
@ -186,7 +172,6 @@ unsigned read_datalog(char const * file) {
g_orig_rules = &original_rules; g_orig_rules = &original_rules;
g_code = &rules_code; g_code = &rules_code;
g_ectx = &ex_ctx; g_ectx = &ex_ctx;
g_params = &s_params;
try { try {
g_piece_timer.reset(); g_piece_timer.reset();
@ -254,7 +239,6 @@ unsigned read_datalog(char const * file) {
original_rules, original_rules,
rules_code, rules_code,
ex_ctx, ex_ctx,
s_params,
false); false);
} }
@ -266,7 +250,6 @@ unsigned read_datalog(char const * file) {
original_rules, original_rules,
rules_code, rules_code,
ex_ctx, ex_ctx,
s_params,
true); true);
return ERR_MEMOUT; return ERR_MEMOUT;
} }

5
src/shell/datalog_frontend.h
View file

@ -19,11 +19,6 @@ Revision History:
#ifndef _DATALOG_FRONTEND_H_ #ifndef _DATALOG_FRONTEND_H_
#define _DATALOG_FRONTEND_H_ #define _DATALOG_FRONTEND_H_
struct datalog_params {
symbol m_default_table;
bool m_default_table_checked;
datalog_params();
};
unsigned read_datalog(char const * file); unsigned read_datalog(char const * file);

2
src/shell/main.cpp
View file

@ -27,8 +27,8 @@ Revision History:
#include"z3_log_frontend.h" #include"z3_log_frontend.h"
#include"warning.h" #include"warning.h"
#include"version.h" #include"version.h"
#include"datalog_frontend.h"
#include"dimacs_frontend.h" #include"dimacs_frontend.h"
#include"datalog_frontend.h"
#include"timeout.h" #include"timeout.h"
#include"z3_exception.h" #include"z3_exception.h"
#include"error_codes.h" #include"error_codes.h"