mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
Merge branch 'master' of https://github.com/Z3Prover/z3
This commit is contained in:
commit
aab63dc126
|
@ -50,7 +50,7 @@ def add_missing_cr(dir):
|
|||
if f.endswith('.cpp') or f.endswith('.h') or f.endswith('.c') or f.endswith('.cs'):
|
||||
path = "%s\\%s" % (root, f)
|
||||
if not has_cr(path):
|
||||
print "Missing CR for %s" % path
|
||||
print("Missing CR for %s" % path)
|
||||
add_cr(path)
|
||||
|
||||
add_missing_cr('src')
|
||||
|
|
|
@ -42,16 +42,16 @@ def set_build_dir(path):
|
|||
mk_dir(BUILD_DIR)
|
||||
|
||||
def display_help():
|
||||
print "mk_unix_dist.py: Z3 Linux/OSX/BSD distribution generator\n"
|
||||
print "This script generates the zip files containing executables, shared objects, header files for Linux/OSX/BSD."
|
||||
print "It must be executed from the Z3 root directory."
|
||||
print "\nOptions:"
|
||||
print " -h, --help display this message."
|
||||
print " -s, --silent do not print verbose messages."
|
||||
print " -b <sudir>, --build=<subdir> subdirectory where x86 and x64 Z3 versions will be built (default: build-dist)."
|
||||
print " -f, --force force script to regenerate Makefiles."
|
||||
print " --nojava do not include Java bindings in the binary distribution files."
|
||||
print " --githash include git hash in the Zip file."
|
||||
print("mk_unix_dist.py: Z3 Linux/OSX/BSD distribution generator\n")
|
||||
print("This script generates the zip files containing executables, shared objects, header files for Linux/OSX/BSD.")
|
||||
print("It must be executed from the Z3 root directory.")
|
||||
print("\nOptions:")
|
||||
print(" -h, --help display this message.")
|
||||
print(" -s, --silent do not print verbose messages.")
|
||||
print(" -b <sudir>, --build=<subdir> subdirectory where x86 and x64 Z3 versions will be built (default: build-dist).")
|
||||
print(" -f, --force force script to regenerate Makefiles.")
|
||||
print(" --nojava do not include Java bindings in the binary distribution files.")
|
||||
print(" --githash include git hash in the Zip file.")
|
||||
exit(0)
|
||||
|
||||
# Parse configuration option for mk_make script
|
||||
|
@ -169,7 +169,7 @@ def mk_dist_dir():
|
|||
mk_util.JAVA_ENABLED = JAVA_ENABLED
|
||||
mk_unix_dist(build_path, dist_path)
|
||||
if is_verbose():
|
||||
print "Generated distribution folder at '%s'" % dist_path
|
||||
print("Generated distribution folder at '%s'" % dist_path)
|
||||
|
||||
ZIPOUT = None
|
||||
|
||||
|
@ -193,7 +193,7 @@ def mk_zip():
|
|||
ZIPOUT = zipfile.ZipFile(zfname, 'w', zipfile.ZIP_DEFLATED)
|
||||
os.path.walk(dist_path, mk_zip_visitor, '*')
|
||||
if is_verbose():
|
||||
print "Generated '%s'" % zfname
|
||||
print("Generated '%s'" % zfname)
|
||||
except:
|
||||
pass
|
||||
ZIPOUT = None
|
||||
|
|
|
@ -10,7 +10,7 @@ endif = re.compile("#endif /\* \_(.*)\_H\_")
|
|||
|
||||
|
||||
def fix_hdr(file):
|
||||
print file
|
||||
print(file)
|
||||
tmp = "%s.tmp" % file
|
||||
ins = open(file)
|
||||
ous = open(tmp,'w')
|
||||
|
@ -29,7 +29,7 @@ def fix_hdr(file):
|
|||
continue
|
||||
m = ifndef.search(line)
|
||||
if m:
|
||||
print m.group(1)
|
||||
print(m.group(1))
|
||||
ous.write("#ifndef ")
|
||||
ous.write(m.group(1))
|
||||
ous.write("_H_\n")
|
||||
|
|
File diff suppressed because it is too large
Load diff
|
@ -2563,7 +2563,7 @@ public class Context extends IDisposable
|
|||
}
|
||||
|
||||
/**
|
||||
* Create a tactic that applies the given tactics in parallel.
|
||||
* Create a tactic that applies the given tactics in parallel until one of them succeeds (i.e., the first that doesn't fail).
|
||||
**/
|
||||
public Tactic parOr(Tactic... t)
|
||||
{
|
||||
|
|
|
@ -2941,7 +2941,7 @@ sig
|
|||
Alias for [UsingParams]*)
|
||||
val with_ : context -> tactic -> Params.params -> tactic
|
||||
|
||||
(** Create a tactic that applies the given tactics in parallel. *)
|
||||
(** Create a tactic that applies the given tactics in parallel until one of them succeeds (i.e., the first that doesn't fail). *)
|
||||
val par_or : context -> tactic list -> tactic
|
||||
|
||||
(** Create a tactic that applies a tactic to a given goal and then another tactic
|
||||
|
|
|
@ -37,7 +37,7 @@ tactic_cmd::~tactic_cmd() {
|
|||
}
|
||||
|
||||
tactic * tactic_cmd::mk(ast_manager & m) {
|
||||
return (*m_factory)(m, params_ref());
|
||||
return (*m_factory)(m, params_ref());
|
||||
}
|
||||
|
||||
probe_info::probe_info(symbol const & n, char const * d, probe * p):
|
||||
|
@ -62,12 +62,12 @@ public:
|
|||
virtual char const * get_descr(cmd_context & ctx) const { return "declare a new tactic, use (help-tactic) for the tactic language syntax."; }
|
||||
virtual unsigned get_arity() const { return 2; }
|
||||
virtual void prepare(cmd_context & ctx) { m_name = symbol::null; m_decl = 0; }
|
||||
virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const {
|
||||
virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const {
|
||||
if (m_name == symbol::null) return CPK_SYMBOL;
|
||||
return CPK_SEXPR;
|
||||
}
|
||||
virtual void set_next_arg(cmd_context & ctx, symbol const & s) { m_name = s; }
|
||||
virtual void set_next_arg(cmd_context & ctx, sexpr * n) { m_decl = n; }
|
||||
virtual void set_next_arg(cmd_context & ctx, sexpr * n) { m_decl = n; }
|
||||
virtual void execute(cmd_context & ctx) {
|
||||
tactic_ref t = sexpr2tactic(ctx, m_decl); // make sure the tactic is well formed.
|
||||
ctx.insert_user_tactic(m_name, m_decl);
|
||||
|
@ -82,7 +82,7 @@ ATOMIC_CMD(get_user_tactics_cmd, "get-user-tactics", "display tactics defined us
|
|||
for (bool first = true; it != end; ++it) {
|
||||
if (first) first = false; else buf << "\n ";
|
||||
buf << "(declare-tactic " << it->m_key << " ";
|
||||
it->m_value->display(buf);
|
||||
it->m_value->display(buf);
|
||||
buf << ")";
|
||||
}
|
||||
std::string r = buf.str();
|
||||
|
@ -94,8 +94,8 @@ void help_tactic(cmd_context & ctx) {
|
|||
std::ostringstream buf;
|
||||
buf << "combinators:\n";
|
||||
buf << "- (and-then <tactic>+) executes the given tactics sequencially.\n";
|
||||
buf << "- (or-else <tactic>+) tries the given tactics in sequence until one of them succeeds.\n";
|
||||
buf << "- (par-or <tactic>+) executes the given tactics in parallel until one of them succeeds.\n";
|
||||
buf << "- (or-else <tactic>+) tries the given tactics in sequence until one of them succeeds (i.e., the first that doesn't fail).\n";
|
||||
buf << "- (par-or <tactic>+) executes the given tactics in parallel until one of them succeeds (i.e., the first that doesn't fail).\n";
|
||||
buf << "- (par-then <tactic1> <tactic2>) executes tactic1 and then tactic2 to every subgoal produced by tactic1. All subgoals are processed in parallel.\n";
|
||||
buf << "- (try-for <tactic> <num>) excutes the given tactic for at most <num> milliseconds, it fails if the execution takes more than <num> milliseconds.\n";
|
||||
buf << "- (if <probe> <tactic> <tactic>) if <probe> evaluates to true, then execute the first tactic. Otherwise execute the second.\n";
|
||||
|
@ -134,8 +134,8 @@ public:
|
|||
}
|
||||
|
||||
virtual char const * get_usage() const { return "<tactic> (<keyword> <value>)*"; }
|
||||
|
||||
virtual void prepare(cmd_context & ctx) {
|
||||
|
||||
virtual void prepare(cmd_context & ctx) {
|
||||
parametric_cmd::prepare(ctx);
|
||||
m_tactic = 0;
|
||||
}
|
||||
|
@ -144,17 +144,17 @@ public:
|
|||
if (m_tactic == 0) return CPK_SEXPR;
|
||||
return parametric_cmd::next_arg_kind(ctx);
|
||||
}
|
||||
|
||||
|
||||
virtual void set_next_arg(cmd_context & ctx, sexpr * arg) {
|
||||
m_tactic = arg;
|
||||
}
|
||||
|
||||
|
||||
virtual void init_pdescrs(cmd_context & ctx, param_descrs & p) {
|
||||
insert_timeout(p);
|
||||
insert_max_memory(p);
|
||||
p.insert("print_statistics", CPK_BOOL, "(default: false) print statistics.");
|
||||
}
|
||||
|
||||
|
||||
void display_statistics(cmd_context & ctx, tactic * t) {
|
||||
statistics stats;
|
||||
get_memory_statistics(stats);
|
||||
|
@ -181,7 +181,7 @@ public:
|
|||
p.insert("print_proof", CPK_BOOL, "(default: false) print proof.");
|
||||
p.insert("print_model", CPK_BOOL, "(default: false) print model.");
|
||||
}
|
||||
|
||||
|
||||
virtual void execute(cmd_context & ctx) {
|
||||
params_ref p = ctx.params().merge_default_params(ps());
|
||||
tactic_ref tref = using_params(sexpr2tactic(ctx, m_tactic), p);
|
||||
|
@ -200,7 +200,7 @@ public:
|
|||
{
|
||||
tactic & t = *tref;
|
||||
cancel_eh<tactic> eh(t);
|
||||
{
|
||||
{
|
||||
scoped_ctrl_c ctrlc(eh);
|
||||
scoped_timer timer(timeout, &eh);
|
||||
cmd_context::scoped_watch sw(ctx);
|
||||
|
@ -212,7 +212,7 @@ public:
|
|||
if (r == l_undef) {
|
||||
if (reason_unknown != "") {
|
||||
result->m_unknown = reason_unknown;
|
||||
// ctx.diagnostic_stream() << "\"" << escaped(reason_unknown.c_str(), true) << "\"" << std::endl;
|
||||
// ctx.diagnostic_stream() << "\"" << escaped(reason_unknown.c_str(), true) << "\"" << std::endl;
|
||||
}
|
||||
else {
|
||||
result->m_unknown = "unknown";
|
||||
|
@ -231,7 +231,7 @@ public:
|
|||
}
|
||||
t.collect_statistics(result->m_stats);
|
||||
}
|
||||
|
||||
|
||||
if (ctx.produce_unsat_cores()) {
|
||||
ptr_vector<expr> core_elems;
|
||||
m.linearize(core, core_elems);
|
||||
|
@ -247,7 +247,7 @@ public:
|
|||
ctx.regular_stream() << ")" << std::endl;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
if (ctx.produce_models() && md) {
|
||||
result->m_model = md;
|
||||
if (p.get_bool("print_model", false)) {
|
||||
|
@ -291,7 +291,7 @@ public:
|
|||
#endif
|
||||
exec_given_tactic_cmd::init_pdescrs(ctx, p);
|
||||
}
|
||||
|
||||
|
||||
virtual void execute(cmd_context & ctx) {
|
||||
params_ref p = ctx.params().merge_default_params(ps());
|
||||
tactic_ref tref = using_params(sexpr2tactic(ctx, m_tactic), p);
|
||||
|
@ -300,9 +300,9 @@ public:
|
|||
ast_manager & m = ctx.m();
|
||||
goal_ref g = alloc(goal, m, ctx.produce_proofs(), ctx.produce_models(), ctx.produce_unsat_cores());
|
||||
assert_exprs_from(ctx, *g);
|
||||
|
||||
unsigned timeout = p.get_uint("timeout", UINT_MAX);
|
||||
|
||||
|
||||
unsigned timeout = p.get_uint("timeout", UINT_MAX);
|
||||
|
||||
goal_ref_buffer result_goals;
|
||||
model_converter_ref mc;
|
||||
proof_converter_ref pc;
|
||||
|
@ -311,7 +311,7 @@ public:
|
|||
std::string reason_unknown;
|
||||
bool failed = false;
|
||||
cancel_eh<tactic> eh(t);
|
||||
{
|
||||
{
|
||||
scoped_ctrl_c ctrlc(eh);
|
||||
scoped_timer timer(timeout, &eh);
|
||||
cmd_context::scoped_watch sw(ctx);
|
||||
|
@ -323,7 +323,7 @@ public:
|
|||
failed = true;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
if (!failed && p.get_bool("print", true)) {
|
||||
bool print_dependencies = p.get_bool("print_dependencies", false);
|
||||
ctx.regular_stream() << "(goals\n";
|
||||
|
@ -343,7 +343,7 @@ public:
|
|||
}
|
||||
#endif
|
||||
|
||||
if (!failed && p.get_bool("print_benchmark", false)) {
|
||||
if (!failed && p.get_bool("print_benchmark", false)) {
|
||||
unsigned num_goals = result_goals.size();
|
||||
SASSERT(num_goals > 0);
|
||||
if (num_goals == 1) {
|
||||
|
@ -374,10 +374,10 @@ public:
|
|||
ctx.display_smt2_benchmark(ctx.regular_stream(), 1, assertions);
|
||||
}
|
||||
}
|
||||
|
||||
if (!failed && mc && p.get_bool("print_model_converter", false))
|
||||
|
||||
if (!failed && mc && p.get_bool("print_model_converter", false))
|
||||
mc->display(ctx.regular_stream());
|
||||
|
||||
|
||||
if (p.get_bool("print_statistics", false))
|
||||
display_statistics(ctx, tref.get());
|
||||
}
|
||||
|
@ -573,7 +573,7 @@ static tactic * mk_echo(cmd_context & ctx, sexpr * n) {
|
|||
sexpr * curr = n->get_child(i);
|
||||
bool last = (i == num_children - 1);
|
||||
tactic * t;
|
||||
if (curr->is_string())
|
||||
if (curr->is_string())
|
||||
t = mk_echo_tactic(ctx, curr->get_string().c_str(), last);
|
||||
else
|
||||
t = mk_probe_value_tactic(ctx, 0, sexpr2probe(ctx, curr), last);
|
||||
|
@ -701,11 +701,11 @@ tactic * sexpr2tactic(cmd_context & ctx, sexpr * n) {
|
|||
}
|
||||
}
|
||||
|
||||
static probe * mk_not_probe (cmd_context & ctx, sexpr * n) {
|
||||
SASSERT(n->is_composite());
|
||||
unsigned num_children = n->get_num_children();
|
||||
if (num_children != 2)
|
||||
throw cmd_exception("invalid probe expression, one argument expected", n->get_line(), n->get_pos());
|
||||
static probe * mk_not_probe (cmd_context & ctx, sexpr * n) {
|
||||
SASSERT(n->is_composite());
|
||||
unsigned num_children = n->get_num_children();
|
||||
if (num_children != 2)
|
||||
throw cmd_exception("invalid probe expression, one argument expected", n->get_line(), n->get_pos());
|
||||
return mk_not(sexpr2probe(ctx, n->get_child(1)));
|
||||
}
|
||||
|
||||
|
@ -775,7 +775,7 @@ probe * sexpr2probe(cmd_context & ctx, sexpr * n) {
|
|||
if (!head->is_symbol())
|
||||
throw cmd_exception("invalid probe, symbol expected", n->get_line(), n->get_pos());
|
||||
symbol const & p_name = head->get_symbol();
|
||||
|
||||
|
||||
if (p_name == "=")
|
||||
return mk_eq_probe(ctx, n);
|
||||
else if (p_name == "<=")
|
||||
|
@ -792,13 +792,13 @@ probe * sexpr2probe(cmd_context & ctx, sexpr * n) {
|
|||
return mk_or_probe(ctx, n);
|
||||
else if (p_name == "=>" || p_name == "implies")
|
||||
return mk_implies_probe(ctx, n);
|
||||
else if (p_name == "not")
|
||||
else if (p_name == "not")
|
||||
return mk_not_probe(ctx, n);
|
||||
else if (p_name == "*")
|
||||
return mk_mul_probe(ctx, n);
|
||||
else if (p_name == "+")
|
||||
else if (p_name == "+")
|
||||
return mk_add_probe(ctx, n);
|
||||
else if (p_name == "-")
|
||||
else if (p_name == "-")
|
||||
return mk_sub_probe(ctx, n);
|
||||
else if (p_name == "/")
|
||||
return mk_div_probe(ctx, n);
|
||||
|
|
File diff suppressed because it is too large
Load diff
Loading…
Reference in a new issue