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

Merge branch 'master' of https://github.com/z3prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-12-14 16:46:25 -08:00
commit f01d9d29d2
13 changed files with 85 additions and 59 deletions
Download patch file Download diff file Expand all files Collapse all files

31
src/api/c++/z3++.h
View file

@ -366,8 +366,14 @@ namespace z3 {
void recdef(func_decl, expr_vector const& args, expr const& body);
func_decl user_propagate_function(symbol const& name, sort_vector const& domain, sort const& range);
/**
\brief create an uninterpreted constant.
*/
expr constant(symbol const & name, sort const & s);
expr constant(char const * name, sort const & s);
/**
\brief create uninterpreted constants of a given sort.
*/
expr bool_const(char const * name);
expr int_const(char const * name);
expr real_const(char const * name);
@ -378,6 +384,12 @@ namespace z3 {
template<size_t precision>
expr fpa_const(char const * name);
/**
\brief create a de-Bruijn variable.
*/
expr variable(unsigned index, sort const& s);
expr fpa_rounding_mode();
expr bool_val(bool b);
@ -1907,21 +1919,21 @@ namespace z3 {
inline expr operator>(expr const & a, int b) { return a > a.ctx().num_val(b, a.get_sort()); }
inline expr operator>(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) > b; }
inline expr operator&(expr const & a, expr const & b) { if (a.is_bool()) return a && b; check_context(a, b); Z3_ast r = Z3_mk_bvand(a.ctx(), a, b); return expr(a.ctx(), r); }
inline expr operator&(expr const & a, expr const & b) { if (a.is_bool()) return a && b; check_context(a, b); Z3_ast r = Z3_mk_bvand(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); }
inline expr operator&(expr const & a, int b) { return a & a.ctx().num_val(b, a.get_sort()); }
inline expr operator&(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) & b; }
inline expr operator^(expr const & a, expr const & b) { check_context(a, b); Z3_ast r = a.is_bool() ? Z3_mk_xor(a.ctx(), a, b) : Z3_mk_bvxor(a.ctx(), a, b); return expr(a.ctx(), r); }
inline expr operator^(expr const & a, expr const & b) { check_context(a, b); Z3_ast r = a.is_bool() ? Z3_mk_xor(a.ctx(), a, b) : Z3_mk_bvxor(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); }
inline expr operator^(expr const & a, int b) { return a ^ a.ctx().num_val(b, a.get_sort()); }
inline expr operator^(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) ^ b; }
inline expr operator|(expr const & a, expr const & b) { if (a.is_bool()) return a || b; check_context(a, b); Z3_ast r = Z3_mk_bvor(a.ctx(), a, b); return expr(a.ctx(), r); }
inline expr operator|(expr const & a, expr const & b) { if (a.is_bool()) return a || b; check_context(a, b); Z3_ast r = Z3_mk_bvor(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); }
inline expr operator|(expr const & a, int b) { return a | a.ctx().num_val(b, a.get_sort()); }
inline expr operator|(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) | b; }
inline expr nand(expr const& a, expr const& b) { if (a.is_bool()) return !(a && b); check_context(a, b); Z3_ast r = Z3_mk_bvnand(a.ctx(), a, b); return expr(a.ctx(), r); }
inline expr nor(expr const& a, expr const& b) { if (a.is_bool()) return !(a || b); check_context(a, b); Z3_ast r = Z3_mk_bvnor(a.ctx(), a, b); return expr(a.ctx(), r); }
inline expr xnor(expr const& a, expr const& b) { if (a.is_bool()) return !(a ^ b); check_context(a, b); Z3_ast r = Z3_mk_bvxnor(a.ctx(), a, b); return expr(a.ctx(), r); }
inline expr nand(expr const& a, expr const& b) { if (a.is_bool()) return !(a && b); check_context(a, b); Z3_ast r = Z3_mk_bvnand(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); }
inline expr nor(expr const& a, expr const& b) { if (a.is_bool()) return !(a || b); check_context(a, b); Z3_ast r = Z3_mk_bvnor(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); }
inline expr xnor(expr const& a, expr const& b) { if (a.is_bool()) return !(a ^ b); check_context(a, b); Z3_ast r = Z3_mk_bvxnor(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); }
inline expr min(expr const& a, expr const& b) {
check_context(a, b);
Z3_ast r;
@ -1935,6 +1947,7 @@ namespace z3 {
assert(a.is_fpa());
r = Z3_mk_fpa_min(a.ctx(), a, b);
}
a.check_error();
return expr(a.ctx(), r);
}
inline expr max(expr const& a, expr const& b) {
@ -1950,6 +1963,7 @@ namespace z3 {
assert(a.is_fpa());
r = Z3_mk_fpa_max(a.ctx(), a, b);
}
a.check_error();
return expr(a.ctx(), r);
}
inline expr bvredor(expr const & a) {
@ -3580,6 +3594,11 @@ namespace z3 {
return expr(*this, r);
}
inline expr context::constant(char const * name, sort const & s) { return constant(str_symbol(name), s); }
inline expr context::variable(unsigned idx, sort const& s) {
Z3_ast r = Z3_mk_bound(m_ctx, idx, s);
check_error();
return expr(*this, r);
}
inline expr context::bool_const(char const * name) { return constant(name, bool_sort()); }
inline expr context::int_const(char const * name) { return constant(name, int_sort()); }
inline expr context::real_const(char const * name) { return constant(name, real_sort()); }

4
src/api/python/z3/z3.py
View file

@ -1469,7 +1469,9 @@ def FreshConst(sort, prefix="c"):
def Var(idx, s):
"""Create a Z3 free variable. Free variables are used to create quantified formulas.
A free variable with index n is bound when it occurs within the scope of n+1 quantified
declarations.
>>> Var(0, IntSort())
Var(0)
>>> eq(Var(0, IntSort()), Var(0, BoolSort()))

8
src/api/z3_api.h
View file

@ -4051,7 +4051,10 @@ extern "C" {
Z3_pattern Z3_API Z3_mk_pattern(Z3_context c, unsigned num_patterns, Z3_ast const terms[]);
/**
\brief Create a bound variable.
\brief Create a variable.
Variables are intended to be bound by a scope created by a quantifier. So we call them bound variables
even if they appear as free variables in the expression produced by \c Z3_mk_bound.
Bound variables are indexed by de-Bruijn indices. It is perhaps easiest to explain
the meaning of de-Bruijn indices by indicating the compilation process from
@ -5318,8 +5321,9 @@ extern "C" {
Z3_ast const to[]);
/**
\brief Substitute the free variables in \c a with the expressions in \c to.
\brief Substitute the variables in \c a with the expressions in \c to.
For every \c i smaller than \c num_exprs, the variable with de-Bruijn index \c i is replaced with term \ccode{to[i]}.
Note that a variable is created using the function \ref Z3_mk_bound.
def_API('Z3_substitute_vars', AST, (_in(CONTEXT), _in(AST), _in(UINT), _in_array(2, AST)))
*/

8
src/ast/simplifiers/elim_unconstrained.cpp
View file

@ -65,7 +65,6 @@ void elim_unconstrained::eliminate() {
expr_ref r(m), side_cond(m);
int v = m_heap.erase_min();
node& n = get_node(v);
IF_VERBOSE(11, verbose_stream() << mk_bounded_pp(n.m_orig, m) << " @ " << n.m_refcount << "\n");
if (n.m_refcount == 0)
continue;
if (n.m_refcount > 1)
@ -203,10 +202,11 @@ void elim_unconstrained::freeze(expr* t) {
return;
node& n = get_node(t);
if (!n.m_term)
return;
n.m_refcount = UINT_MAX / 2;
if (m_heap.contains(root(t)))
return;
if (m_heap.contains(root(t))) {
n.m_refcount = UINT_MAX / 2;
m_heap.increased(root(t));
}
}
void elim_unconstrained::gc(expr* t) {

25
src/muz/base/dl_rule.cpp
View file

@ -1013,28 +1013,31 @@ namespace datalog {
}
}
void rule::display(context & ctx, std::ostream & out) const {
void rule::display(context & ctx, std::ostream & out, bool compact) const {
ast_manager & m = ctx.get_manager();
out << m_name.str () << ":\n";
if (!compact)
out << m_name.str () << ":\n";
output_predicate(ctx, m_head, out);
if (m_tail_size == 0) {
out << ".\n";
out << ".";
if (!compact)
out << "\n";
return;
}
out << " :- ";
for (unsigned i = 0; i < m_tail_size; i++) {
if (i > 0)
out << ",";
out << "\n ";
if (!compact)
out << "\n";
out << " ";
if (is_neg_tail(i))
out << "not ";
app * t = get_tail(i);
if (ctx.is_predicate(t)) {
if (ctx.is_predicate(t))
output_predicate(ctx, t, out);
}
else {
else
out << mk_pp(t, m);
}
}
out << '.';
if (ctx.output_profile()) {
@ -1042,10 +1045,10 @@ namespace datalog {
output_profile(out);
out << '}';
}
out << '\n';
if (m_proof) {
if (!compact)
out << '\n';
if (m_proof)
out << mk_pp(m_proof, m) << '\n';
}
}

2
src/muz/base/dl_rule.h
View file

@ -365,7 +365,7 @@ namespace datalog {
void get_vars(ast_manager& m, ptr_vector<sort>& sorts) const;
void display(context & ctx, std::ostream & out) const;
void display(context & ctx, std::ostream & out, bool compact = false) const;
/**
\brief Return the name(s) associated with this rule. Plural for preprocessed (e.g. obtained by inlining) rules.

23
src/muz/base/dl_util.h
View file

@ -320,32 +320,31 @@ namespace datalog {
unsigned_vector & res, bool & identity);
template<class T>
void permutate_by_cycle(T & container, unsigned cycle_len, const unsigned * permutation_cycle) {
if (cycle_len<2) {
void permute_by_cycle(T& container, unsigned cycle_len, const unsigned * permutation_cycle) {
if (cycle_len < 2)
return;
}
auto aux = container[permutation_cycle[0]];
for (unsigned i=1; i<cycle_len; i++) {
container[permutation_cycle[i-1]]=container[permutation_cycle[i]];
}
container[permutation_cycle[cycle_len-1]]=aux;
verbose_stream() << "xx " << cycle_len << "\n";
for (unsigned i = 1; i < cycle_len; i++)
container[permutation_cycle[i-1]] = container[permutation_cycle[i]];
container[permutation_cycle[cycle_len-1]] = aux;
}
template<class T, class M>
void permutate_by_cycle(ref_vector<T,M> & container, unsigned cycle_len, const unsigned * permutation_cycle) {
void permute_by_cycle(ref_vector<T,M> & container, unsigned cycle_len, const unsigned * permutation_cycle) {
if (cycle_len<2) {
return;
}
verbose_stream() << "ptr\n";
T * aux = container.get(permutation_cycle[0]);
for (unsigned i=1; i<cycle_len; i++) {
for (unsigned i=1; i < cycle_len; i++) {
container.set(permutation_cycle[i-1], container.get(permutation_cycle[i]));
}
container.set(permutation_cycle[cycle_len-1], aux);
}
template<class T>
void permutate_by_cycle(T & container, const unsigned_vector & permutation_cycle) {
permutate_by_cycle(container, permutation_cycle.size(), permutation_cycle.data());
void permute_by_cycle(T & container, const unsigned_vector & permutation_cycle) {
permute_by_cycle(container, permutation_cycle.size(), permutation_cycle.data());
}

2
src/muz/rel/dl_base.h
View file

@ -160,7 +160,7 @@ namespace datalog {
SASSERT(cycle_len>=2);
result=src;
permutate_by_cycle(result, cycle_len, permutation_cycle);
permute_by_cycle(result, cycle_len, permutation_cycle);
}
/**

2
src/muz/rel/dl_finite_product_relation.cpp
View file

@ -674,7 +674,7 @@ namespace datalog {
unsigned sig_sz = r.get_signature().size();
unsigned_vector permutation;
add_sequence(0, sig_sz, permutation);
permutate_by_cycle(permutation, cycle_len, permutation_cycle);
permute_by_cycle(permutation, cycle_len, permutation_cycle);
unsigned_vector table_permutation;

32
src/muz/rel/dl_mk_explanations.cpp
View file

@ -70,20 +70,16 @@ namespace datalog {
m_union_decl(mk_explanations::get_union_decl(get_context()), get_ast_manager()) {}
~explanation_relation_plugin() override {
for (unsigned i = 0; i < m_pool.size(); ++i) {
for (unsigned j = 0; j < m_pool[i].size(); ++j) {
for (unsigned i = 0; i < m_pool.size(); ++i)
for (unsigned j = 0; j < m_pool[i].size(); ++j)
dealloc(m_pool[i][j]);
}
}
}
bool can_handle_signature(const relation_signature & s) override {
unsigned n=s.size();
for (unsigned i=0; i<n; i++) {
if (!get_context().get_decl_util().is_rule_sort(s[i])) {
for (unsigned i=0; i<n; i++)
if (!get_context().get_decl_util().is_rule_sort(s[i]))
return false;
}
}
return true;
}
@ -105,9 +101,10 @@ namespace datalog {
relation_intersection_filter_fn * mk_filter_by_negation_fn(const relation_base & t,
const relation_base & negated_obj, unsigned joined_col_cnt,
const unsigned * t_cols, const unsigned * negated_cols) override;
relation_intersection_filter_fn * mk_filter_by_intersection_fn(const relation_base & t,
const relation_base & src, unsigned joined_col_cnt,
const unsigned * t_cols, const unsigned * src_cols) override;
relation_intersection_filter_fn * mk_filter_by_intersection_fn(
const relation_base & t,
const relation_base & src, unsigned joined_col_cnt,
const unsigned * t_cols, const unsigned * src_cols) override;
};
@ -150,7 +147,7 @@ namespace datalog {
void assign_data(const relation_fact & f) {
m_empty = false;
unsigned n=get_signature().size();
unsigned n = get_signature().size();
SASSERT(f.size()==n);
m_data.reset();
m_data.append(n, f.data());
@ -161,11 +158,12 @@ namespace datalog {
m_data.resize(get_signature().size());
}
void unite_with_data(const relation_fact & f) {
if (empty()) {
assign_data(f);
return;
}
unsigned n=get_signature().size();
unsigned n = get_signature().size();
SASSERT(f.size()==n);
for (unsigned i=0; i<n; i++) {
SASSERT(!is_undefined(i));
@ -365,9 +363,9 @@ namespace datalog {
explanation_relation * res = static_cast<explanation_relation *>(plugin.mk_empty(get_result_signature()));
if (!r.empty()) {
relation_fact permutated_data = r.m_data;
permutate_by_cycle(permutated_data, m_cycle);
res->assign_data(permutated_data);
relation_fact permuted_data = r.m_data;
permute_by_cycle(dynamic_cast<app_ref_vector&>(permuted_data), m_cycle);
res->assign_data(permuted_data);
}
return res;
}
@ -704,7 +702,7 @@ namespace datalog {
symbol mk_explanations::get_rule_symbol(rule * r) {
if (r->name() == symbol::null) {
std::stringstream sstm;
r->display(m_context, sstm);
r->display(m_context, sstm, true);
std::string res = sstm.str();
res = res.substr(0, res.find_last_not_of('\n')+1);
return symbol(res.c_str());

2
src/muz/rel/dl_relation_manager.cpp
View file

@ -1149,7 +1149,7 @@ namespace datalog {
}
void modify_fact(table_fact & f) const override {
permutate_by_cycle(f, m_cycle);
permute_by_cycle(f, m_cycle);
}
table_base * operator()(const table_base & t) override {

4
src/muz/rel/dl_sieve_relation.cpp
View file

@ -413,14 +413,14 @@ namespace datalog {
unsigned sig_sz = r.get_signature().size();
unsigned_vector permutation;
add_sequence(0, sig_sz, permutation);
permutate_by_cycle(permutation, cycle_len, permutation_cycle);
permute_by_cycle(permutation, cycle_len, permutation_cycle);
bool inner_identity;
unsigned_vector inner_permutation;
collect_sub_permutation(permutation, r.m_sig2inner, inner_permutation, inner_identity);
bool_vector result_inner_cols = r.m_inner_cols;
permutate_by_cycle(result_inner_cols, cycle_len, permutation_cycle);
permute_by_cycle(result_inner_cols, cycle_len, permutation_cycle);
relation_signature result_sig;
relation_signature::from_rename(r.get_signature(), cycle_len, permutation_cycle, result_sig);

1
src/params/context_params.cpp
View file

@ -109,6 +109,7 @@ void context_params::set(char const * param, char const * value) {
else if (p == "encoding") {
if (strcmp(value, "unicode") == 0 || strcmp(value, "bmp") == 0 || strcmp(value, "ascii") == 0) {
m_encoding = value;
gparams::set("encoding", value);
}
else {
std::stringstream strm;