mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

cleanning

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-12-01 18:50:26 -08:00
parent 29ec68284b
commit 9bd4fd969a
6 changed files with 10 additions and 33 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/front_end_params/front_end_params.cpp
View file

@ -36,7 +36,6 @@ void front_end_params::register_params(ini_params & p) {
p.register_int_param("proof_mode", 0, 2, reinterpret_cast<int&>(m_proof_mode), "select proof generation mode: 0 - disabled, 1 - coarse grain, 2 - fine grain");
p.register_bool_param("trace", m_trace, "enable tracing for the Axiom Profiler tool");
p.register_string_param("trace_file_name", m_trace_file_name, "tracing file name");
p.register_bool_param("display_config", m_display_config, "display configuration used by Z3");
#ifdef _WINDOWS
// The non-windows memory manager does not have access to memory sizes.

6
src/front_end_params/front_end_params.h
View file

@ -33,8 +33,6 @@ struct front_end_params : public smt_params {
bool m_trace;
std::string m_trace_file_name;
std::fstream* m_trace_stream;
bool m_display_config;
bool m_dump_goal_as_smt;
front_end_params():
m_well_sorted_check(true),
@ -45,9 +43,7 @@ struct front_end_params : public smt_params {
m_debug_ref_count(false),
m_trace(false),
m_trace_file_name("z3.log"),
m_trace_stream(NULL),
m_display_config(false),
m_dump_goal_as_smt(false) {
m_trace_stream(NULL) {
}
void open_trace_file();

6
src/front_end_params/smt_params.h
View file

@ -204,6 +204,7 @@ struct smt_params : public preprocessor_params,
unsigned m_soft_timeout;
bool m_at_labels_cex; // only use labels which contains the @ symbol when building multiple counterexamples.
bool m_check_at_labels; // check that @ labels are inserted to generate unique counter-examples.
bool m_dump_goal_as_smt;
smt_params():
m_display_proof(false),
@ -270,9 +271,8 @@ struct smt_params : public preprocessor_params,
m_user_theory_persist_axioms(false),
m_soft_timeout(0),
m_at_labels_cex(false),
m_check_at_labels(false)
{
m_check_at_labels(false),
m_dump_goal_as_smt(false) {
}
};

8
src/shell/dimacs_frontend.cpp
View file

@ -22,7 +22,6 @@ Revision History:
#include"timeout.h"
#include"dimacs.h"
#include"sat_solver.h"
#include"front_end_params.h"
extern bool g_display_statistics;
static sat::solver * g_solver = 0;
@ -64,12 +63,12 @@ static void display_model(sat::solver const & s) {
std::cout << "\n";
}
unsigned read_dimacs(char const * file_name, front_end_params & front_end_params) {
unsigned read_dimacs(char const * file_name) {
g_start_time = clock();
register_on_timeout_proc(on_timeout);
signal(SIGINT, on_ctrl_c);
params_ref p;
p.set_bool("produce_models", front_end_params.m_model);
p.set_bool("produce_models", true);
sat::solver solver(p, 0);
g_solver = &solver;
@ -90,8 +89,7 @@ unsigned read_dimacs(char const * file_name, front_end_params & front_end_params
switch (r) {
case l_true:
std::cout << "sat\n";
if (front_end_params.m_model)
display_model(solver);
display_model(solver);
break;
case l_undef:
std::cout << "unknown\n";

2
src/shell/dimacs_frontend.h
View file

@ -19,7 +19,7 @@ Revision History:
#ifndef _DIMACS_FRONTEND_H_
#define _DIMACS_FRONTEND_H_
unsigned read_dimacs(char const * benchmark_file, front_end_params & front_end_params);
unsigned read_dimacs(char const * benchmark_file);
#endif /* _DATALOG_FRONTEND_H_ */

20
src/shell/main.cpp
View file

@ -77,7 +77,7 @@ void display_usage() {
std::cout << " " << OPT << "version prints version number of Z3.\n";
std::cout << " " << OPT << "v:level be verbose, where <level> is the verbosity level.\n";
std::cout << " " << OPT << "nw disable warning messages.\n";
std::cout << " " << OPT << "ps display all available parameters.\n";
std::cout << " " << OPT << "ps display Z3 global (and module) parameters.\n";
std::cout << " --" << " all remaining arguments are assumed to be part of the input file name. This option allows Z3 to read files with strange names such as: -foo.smt2.\n";
std::cout << "\nResources:\n";
// timeout and memout are now available on Linux and OSX too.
@ -87,8 +87,6 @@ void display_usage() {
//
std::cout << "\nOutput:\n";
std::cout << " " << OPT << "st display statistics.\n";
std::cout << "\nSearch heuristics:\n";
std::cout << " " << OPT << "rs:num random seed.\n";
#if defined(Z3DEBUG) || defined(_TRACE)
std::cout << "\nDebugging support:\n";
#endif
@ -226,20 +224,6 @@ void parse_cmd_line_args(int argc, char ** argv) {
}
g_front_end_params->m_relevancy_lvl = strtol(opt_arg, 0, 10);
}
else if (strcmp(opt_name, "rd") == 0) {
if (!opt_arg) {
error("optional argument (/rd:num) is missing.");
}
g_front_end_params->m_random_var_freq = static_cast<double>(strtol(opt_arg, 0, 10)) / 100.0;
}
else if (strcmp(opt_name, "rs") == 0) {
if (!opt_arg) {
error("optional argument (/rs:num) is missing.");
}
long seed = strtol(opt_arg, 0, 10);
g_front_end_params->m_random_seed = seed;
g_front_end_params->m_arith_random_seed = seed;
}
else if (strcmp(opt_name, "T") == 0) {
if (!opt_arg)
error("option argument (/T:timeout) is missing.");
@ -382,7 +366,7 @@ int main(int argc, char ** argv) {
return_value = read_smtlib2_commands(g_input_file, *g_front_end_params);
break;
case IN_DIMACS:
return_value = read_dimacs(g_input_file, *g_front_end_params);
return_value = read_dimacs(g_input_file);
break;
case IN_DATALOG:
read_datalog(g_input_file, *g_extra_params, *g_front_end_params);