mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

fixing python build errors

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-11-01 09:34:42 -05:00
parent 2a6fa4af39
commit b02fec91cc
7 changed files with 76 additions and 35 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/api/api_ast.cpp
View file

@ -33,6 +33,7 @@ Revision History:
#include "ast/rewriter/th_rewriter.h"
#include "ast/rewriter/var_subst.h"
#include "ast/rewriter/expr_safe_replace.h"
#include "ast/rewriter/recfun_replace.h"
#include "ast/pp.h"
#include "util/scoped_ctrl_c.h"
#include "util/cancel_eh.h"
@ -156,7 +157,8 @@ extern "C" {
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
return;
}
p.set_definition(pd, n, _vars.c_ptr(), abs_body);
recfun_replace replace(m);
p.set_definition(replace, pd, n, _vars.c_ptr(), abs_body);
Z3_CATCH;
}

40
src/ast/recfun_decl_plugin.cpp
View file

@ -21,7 +21,6 @@ Revision History:
#include <functional>
#include <sstream>
#include "ast/expr_functors.h"
#include "ast/expr_substitution.h"
#include "ast/recfun_decl_plugin.h"
#include "ast/ast_pp.h"
#include "util/scoped_ptr_vector.h"
@ -162,7 +161,7 @@ namespace recfun {
static void convert_path(ast_manager & m,
choice_lst const * choices,
expr_ref_vector & conditions /* out */,
expr_substitution & subst /* out */)
replace & subst /* out */)
{
for (; choices != nullptr; choices = choices->next) {
app * ite = choices->ite;
@ -177,15 +176,6 @@ namespace recfun {
}
}
// substitute `subst` in `e`
static expr_ref replace_subst(th_rewriter & th_rw, ast_manager & m,
expr_substitution & subst, expr * e) {
th_rw.reset();
th_rw.set_substitution(&subst);
expr_ref res(m);
th_rw(e, res);
return res;
}
void def::add_case(std::string & name, unsigned case_index, expr_ref_vector const& conditions, expr * rhs, bool is_imm) {
case_def c(m, m_fid, this, name, case_index, get_domain(), conditions, rhs);
@ -198,7 +188,8 @@ namespace recfun {
// Compute a set of cases, given the RHS
void def::compute_cases(is_immediate_pred & is_i, th_rewriter & th_rw,
void def::compute_cases(replace& subst,
is_immediate_pred & is_i,
unsigned n_vars, var *const * vars, expr* rhs)
{
VERIFY(m_cases.empty() && "cases cannot already be computed");
@ -291,13 +282,13 @@ namespace recfun {
// leaf of the search tree
conditions.reset();
expr_substitution subst(m);
subst.reset();
convert_path(m, b.path, conditions, subst);
// substitute, to get rid of `ite` terms
expr_ref case_rhs = replace_subst(th_rw, m, subst, rhs);
expr_ref case_rhs = subst(rhs);
for (unsigned i = 0; i < conditions.size(); ++i) {
conditions[i] = replace_subst(th_rw, m, subst, conditions.get(i));
conditions[i] = subst(conditions.get(i));
}
// yield new case
@ -314,7 +305,7 @@ namespace recfun {
*/
util::util(ast_manager & m)
: m_manager(m), m_fid(m.get_family_id("recfun")), m_th_rw(m),
: m_manager(m), m_fid(m.get_family_id("recfun")),
m_plugin(dynamic_cast<decl::plugin*>(m.get_plugin(m_fid))) {
}
@ -325,8 +316,8 @@ namespace recfun {
return alloc(def, m(), m_fid, name, n, domain, range);
}
void util::set_definition(promise_def & d, unsigned n_vars, var * const * vars, expr * rhs) {
d.set_definition(n_vars, vars, rhs);
void util::set_definition(replace& subst, promise_def & d, unsigned n_vars, var * const * vars, expr * rhs) {
d.set_definition(subst, n_vars, vars, rhs);
}
app_ref util::mk_depth_limit_pred(unsigned d) {
@ -361,11 +352,11 @@ namespace recfun {
};
// set definition
void promise_def::set_definition(unsigned n_vars, var * const * vars, expr * rhs) {
void promise_def::set_definition(replace& r, unsigned n_vars, var * const * vars, expr * rhs) {
SASSERT(n_vars == d->get_arity());
is_imm_pred is_i(*u);
d->compute_cases(is_i, u->get_th_rewriter(), n_vars, vars, rhs);
d->compute_cases(r, is_i, n_vars, vars, rhs);
}
namespace decl {
@ -398,8 +389,8 @@ namespace recfun {
return promise_def(&u(), d);
}
void plugin::set_definition(promise_def & d, unsigned n_vars, var * const * vars, expr * rhs) {
u().set_definition(d, n_vars, vars, rhs);
void plugin::set_definition(replace& r, promise_def & d, unsigned n_vars, var * const * vars, expr * rhs) {
u().set_definition(r, d, n_vars, vars, rhs);
for (case_def & c : d.get_def()->get_cases()) {
m_case_defs.insert(c.get_decl(), &c);
}
@ -409,11 +400,12 @@ namespace recfun {
return !m_case_defs.empty();
}
def* plugin::mk_def(symbol const& name, unsigned n, sort ** params, sort * range,
def* plugin::mk_def(replace& subst,
symbol const& name, unsigned n, sort ** params, sort * range,
unsigned n_vars, var ** vars, expr * rhs) {
promise_def d = mk_def(name, n, params, range);
SASSERT(! m_defs.contains(d.get_def()->get_decl()));
set_definition(d, n_vars, vars, rhs);
set_definition(subst, d, n_vars, vars, rhs);
return d.get_def();
}

20
src/ast/recfun_decl_plugin.h
View file

@ -20,7 +20,6 @@ Revision History:
#pragma once
#include "ast/ast.h"
#include "ast/rewriter/th_rewriter.h"
#include "util/obj_hashtable.h"
namespace recfun {
@ -46,6 +45,13 @@ namespace recfun {
typedef var_ref_vector vars;
class replace {
public:
virtual void reset() = 0;
virtual void insert(expr* d, expr* r) = 0;
virtual expr_ref operator()(expr* e) = 0;
};
class case_def {
friend class def;
func_decl_ref m_pred; //<! predicate used for this case
@ -105,7 +111,7 @@ namespace recfun {
def(ast_manager &m, family_id fid, symbol const & s, unsigned arity, sort *const * domain, sort* range);
// compute cases for a function, given its RHS (possibly containing `ite`).
void compute_cases(is_immediate_pred &, th_rewriter & th_rw,
void compute_cases(replace& subst, is_immediate_pred &,
unsigned n_vars, var *const * vars, expr* rhs);
void add_case(std::string & name, unsigned case_index, expr_ref_vector const& conditions, expr* rhs, bool is_imm = false);
bool contains_ite(expr* e); // expression contains a test?
@ -129,7 +135,7 @@ namespace recfun {
friend class util;
util * u;
def * d;
void set_definition(unsigned n_vars, var * const * vars, expr * rhs); // call only once
void set_definition(replace& r, unsigned n_vars, var * const * vars, expr * rhs); // call only once
public:
promise_def(util * u, def * d) : u(u), d(d) {}
promise_def(promise_def const & from) : u(from.u), d(from.d) {}
@ -167,9 +173,9 @@ namespace recfun {
promise_def mk_def(symbol const& name, unsigned n, sort *const * params, sort * range);
void set_definition(promise_def & d, unsigned n_vars, var * const * vars, expr * rhs);
void set_definition(replace& r, promise_def & d, unsigned n_vars, var * const * vars, expr * rhs);
def* mk_def(symbol const& name, unsigned n, sort ** params, sort * range, unsigned n_vars, var ** vars, expr * rhs);
def* mk_def(replace& subst, symbol const& name, unsigned n, sort ** params, sort * range, unsigned n_vars, var ** vars, expr * rhs);
bool has_def(func_decl* f) const { return m_defs.contains(f); }
bool has_defs() const;
@ -193,18 +199,16 @@ namespace recfun {
ast_manager & m_manager;
family_id m_fid;
th_rewriter m_th_rw;
decl::plugin * m_plugin;
bool compute_is_immediate(expr * rhs);
void set_definition(promise_def & d, unsigned n_vars, var * const * vars, expr * rhs);
void set_definition(replace& r, promise_def & d, unsigned n_vars, var * const * vars, expr * rhs);
public:
util(ast_manager &m);
~util();
ast_manager & m() { return m_manager; }
th_rewriter & get_th_rewriter() { return m_th_rw; }
decl::plugin& get_plugin() { return *m_plugin; }
bool is_case_pred(expr * e) const { return is_app_of(e, m_fid, OP_FUN_CASE_PRED); }

1
src/ast/rewriter/expr_safe_replace.cpp
View file

@ -19,7 +19,6 @@ Revision History:
--*/
#include "ast/rewriter/expr_safe_replace.h"
#include "ast/rewriter/rewriter.h"
#include "ast/ast_pp.h"

1
src/ast/rewriter/expr_safe_replace.h
View file

@ -23,6 +23,7 @@ Revision History:
#define EXPR_SAFE_REPLACE_H_
#include "ast/ast.h"
#include "ast/rewriter/var_subst.h"
class expr_safe_replace {
ast_manager& m;

41
src/ast/rewriter/recfun_replace.h Normal file
View file

@ -0,0 +1,41 @@
/*++
Copyright (c) 2018 Microsoft Corporation
Module Name:
recfun_replace.h
Abstract:
replace function for recfun.
recfun_decl_plugin relies on being able to do expression replacement.
It uses expr_safe_replace from ast/rewriter, which depends on ast.
To break the dependency cycle we hoist the relevant functionality into
an argument to functionality exposed by recfun::set_definition
Author:
Nikolaj Bjorner (nbjorner) 2018-11-01
Revision History:
--*/
#ifndef RECFUN_REPLACE_H_
#define RECFUN_REPLACE_H_
#include "ast/recfun_decl_plugin.h"
#include "ast/rewriter/expr_safe_replace.h"
class recfun_replace : public recfun::replace {
ast_manager& m;
expr_safe_replace m_replace;
public:
recfun_replace(ast_manager& m): m(m), m_replace(m) {}
void reset() override { m_replace.reset(); }
void insert(expr* s, expr* t) { m_replace.insert(s, t); }
expr_ref operator()(expr* e) { expr_ref r(m); m_replace(e, r); return r; }
};
#endif /* RECFUN_REPLACE_H_ */

4
src/cmd_context/cmd_context.cpp
View file

@ -39,6 +39,7 @@ Notes:
#include "ast/well_sorted.h"
#include "ast/for_each_expr.h"
#include "ast/rewriter/th_rewriter.h"
#include "ast/rewriter/recfun_replace.h"
#include "model/model_evaluator.h"
#include "model/model_smt2_pp.h"
#include "model/model_v2_pp.h"
@ -953,7 +954,8 @@ void cmd_context::insert_rec_fun(func_decl* f, expr_ref_vector const& binding, s
}
recfun::promise_def d = p.get_promise_def(f);
p.set_definition(d, vars.size(), vars.c_ptr(), rhs);
recfun_replace replace(m());
p.set_definition(replace, d, vars.size(), vars.c_ptr(), rhs);
}
func_decl * cmd_context::find_func_decl(symbol const & s) const {