mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 05:48:44 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
Nuno Lopes 2013-04-16 15:14:28 -07:00
parent 0b0e5b6912 7e4c9a7f75
commit ec2726ac66
3 changed files with 2 additions and 24 deletions
Show stats 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::instruction_block * g_code;
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(
std::ostream& out,
@ -61,7 +51,6 @@ static void display_statistics(
datalog::rule_set& orig_rules,
datalog::instruction_block& code,
datalog::execution_context& ex_ctx,
smt_params& params,
bool verbose
)
{
@ -109,7 +98,7 @@ static void display_statistics(
static void display_statistics() {
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) {
IF_VERBOSE(1, verbose_stream() << "Z3 Datalog Engine\n";);
datalog_params dl_params;
smt_params s_params;
ast_manager m;
g_overall_time.start();
@ -135,8 +123,6 @@ unsigned read_datalog(char const * file) {
signal(SIGINT, on_ctrl_c);
params_ref params;
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::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_code = &rules_code;
g_ectx = &ex_ctx;
g_params = &s_params;
try {
g_piece_timer.reset();
@ -254,7 +239,6 @@ unsigned read_datalog(char const * file) {
original_rules,
rules_code,
ex_ctx,
s_params,
false);
}
@ -266,7 +250,6 @@ unsigned read_datalog(char const * file) {
original_rules,
rules_code,
ex_ctx,
s_params,
true);
return ERR_MEMOUT;
}

5
src/shell/datalog_frontend.h
View file

@ -19,11 +19,6 @@ Revision History:
#ifndef _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);

2
src/shell/main.cpp
View file

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