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

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

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2017-11-17 21:15:36 +00:00
parent f5ff9fae34 d380db8068
commit 0194df611c
21 changed files with 204 additions and 101 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
scripts/update_api.py
View file

@ -240,7 +240,7 @@ def param2javaw(p):
if k == OUT:
return "jobject"
elif k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY:
if param_type(p) == INT or param_type(p) == UINT:
if param_type(p) == INT or param_type(p) == UINT or param_type(p) == BOOL:
return "jintArray"
else:
return "jlongArray"
@ -258,7 +258,7 @@ def param2pystr(p):
def param2ml(p):
k = param_kind(p)
if k == OUT:
if param_type(p) == INT or param_type(p) == UINT or param_type(p) == INT64 or param_type(p) == UINT64:
if param_type(p) == INT or param_type(p) == UINT or param_type(p) == BOOL or param_type(p) == INT64 or param_type(p) == UINT64:
return "int"
elif param_type(p) == STRING:
return "string"
@ -491,7 +491,7 @@ def java_method_name(name):
# Return the type of the java array elements
def java_array_element_type(p):
if param_type(p) == INT or param_type(p) == UINT:
if param_type(p) == INT or param_type(p) == UINT or param_type(p) == BOOL:
return 'jint'
else:
return 'jlong'
@ -653,7 +653,7 @@ def mk_java(java_dir, package_name):
if k == OUT or k == INOUT:
java_wrapper.write(' %s _a%s;\n' % (type2str(param_type(param)), i))
elif k == IN_ARRAY or k == INOUT_ARRAY:
if param_type(param) == INT or param_type(param) == UINT:
if param_type(param) == INT or param_type(param) == UINT or param_type(param) == BOOL:
java_wrapper.write(' %s * _a%s = (%s*) jenv->GetIntArrayElements(a%s, NULL);\n' % (type2str(param_type(param)), i, type2str(param_type(param)), i))
else:
java_wrapper.write(' GETLONGAELEMS(%s, a%s, _a%s);\n' % (type2str(param_type(param)), i, i))
@ -663,7 +663,7 @@ def mk_java(java_dir, package_name):
type2str(param_type(param)),
param_array_capacity_pos(param),
type2str(param_type(param))))
if param_type(param) == INT or param_type(param) == UINT:
if param_type(param) == INT or param_type(param) == UINT or param_type(param) == BOOL:
java_wrapper.write(' jenv->GetIntArrayRegion(a%s, 0, (jsize)a%s, (jint*)_a%s);\n' % (i, param_array_capacity_pos(param), i))
else:
java_wrapper.write(' GETLONGAREGION(%s, a%s, 0, a%s, _a%s);\n' % (type2str(param_type(param)), i, param_array_capacity_pos(param), i))
@ -702,19 +702,19 @@ def mk_java(java_dir, package_name):
for param in params:
k = param_kind(param)
if k == OUT_ARRAY:
if param_type(param) == INT or param_type(param) == UINT:
if param_type(param) == INT or param_type(param) == UINT or param_type(param) == BOOL:
java_wrapper.write(' jenv->SetIntArrayRegion(a%s, 0, (jsize)a%s, (jint*)_a%s);\n' % (i, param_array_capacity_pos(param), i))
else:
java_wrapper.write(' SETLONGAREGION(a%s, 0, a%s, _a%s);\n' % (i, param_array_capacity_pos(param), i))
java_wrapper.write(' free(_a%s);\n' % i)
elif k == IN_ARRAY or k == OUT_ARRAY:
if param_type(param) == INT or param_type(param) == UINT:
if param_type(param) == INT or param_type(param) == UINT or param_type(param) == BOOL:
java_wrapper.write(' jenv->ReleaseIntArrayElements(a%s, (jint*)_a%s, JNI_ABORT);\n' % (i, i))
else:
java_wrapper.write(' RELEASELONGAELEMS(a%s, _a%s);\n' % (i, i))
elif k == OUT or k == INOUT:
if param_type(param) == INT or param_type(param) == UINT:
if param_type(param) == INT or param_type(param) == UINT or param_type(param) == BOOL:
java_wrapper.write(' {\n')
java_wrapper.write(' jclass mc = jenv->GetObjectClass(a%s);\n' % i)
java_wrapper.write(' jfieldID fid = jenv->GetFieldID(mc, "value", "I");\n')
@ -957,7 +957,7 @@ def def_API(name, result, params):
log_c.write(" }\n")
log_c.write(" Au(a%s);\n" % sz)
exe_c.write("in.get_uint_array(%s)" % i)
elif ty == INT:
elif ty == INT or ty == BOOL:
log_c.write("U(a%s[i]);" % i)
log_c.write(" }\n")
log_c.write(" Au(a%s);\n" % sz)

13
src/api/api_numeral.cpp
View file

@ -387,4 +387,17 @@ extern "C" {
Z3_CATCH_RETURN(Z3_FALSE);
}
Z3_ast Z3_API Z3_mk_bv_numeral(Z3_context c, unsigned sz, Z3_bool const* bits) {
Z3_TRY;
LOG_Z3_mk_bv_numeral(c, sz, bits);
RESET_ERROR_CODE();
rational r(0);
for (unsigned i = 0; i < sz; ++i) {
if (bits[i]) r += rational::power_of_two(i);
}
ast * a = mk_c(c)->mk_numeral_core(r, mk_c(c)->bvutil().mk_sort(sz));
RETURN_Z3(of_ast(a));
Z3_CATCH_RETURN(0);
}
};

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

@ -301,6 +301,7 @@ namespace z3 {
expr bv_val(__int64 n, unsigned sz);
expr bv_val(__uint64 n, unsigned sz);
expr bv_val(char const * n, unsigned sz);
expr bv_val(unsigned n, bool const* bits);
expr string_val(char const* s);
expr string_val(std::string const& s);
@ -964,6 +965,13 @@ namespace z3 {
friend expr operator|(expr const & a, expr const & b);
friend expr operator|(expr const & a, int b);
friend expr operator|(int a, expr const & b);
friend expr nand(expr const& a, expr const& b);
friend expr nor(expr const& a, expr const& b);
friend expr xnor(expr const& a, expr const& b);
expr rotate_left(unsigned i) { Z3_ast r = Z3_mk_rotate_left(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
expr rotate_right(unsigned i) { Z3_ast r = Z3_mk_rotate_right(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
expr repeat(unsigned i) { Z3_ast r = Z3_mk_repeat(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
friend expr operator~(expr const & a);
expr extract(unsigned hi, unsigned lo) const { Z3_ast r = Z3_mk_extract(ctx(), hi, lo, *this); ctx().check_error(); return expr(ctx(), r); }
@ -1332,6 +1340,10 @@ 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 nand(expr const& a, expr const& 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) { 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) { check_context(a, b); Z3_ast r = Z3_mk_bvxnor(a.ctx(), a, b); return expr(a.ctx(), r); }
inline expr operator~(expr const & a) { Z3_ast r = Z3_mk_bvnot(a.ctx(), a); return expr(a.ctx(), r); }
@ -1406,11 +1418,18 @@ namespace z3 {
inline expr udiv(int a, expr const & b) { return udiv(b.ctx().num_val(a, b.get_sort()), b); }
/**
\brief signed reminder operator for bitvectors
\brief signed remainder operator for bitvectors
*/
inline expr srem(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsrem(a.ctx(), a, b)); }
inline expr srem(expr const & a, int b) { return srem(a, a.ctx().num_val(b, a.get_sort())); }
inline expr srem(int a, expr const & b) { return srem(b.ctx().num_val(a, b.get_sort()), b); }
/**
\brief signed modulus operator for bitvectors
*/
inline expr smod(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsmod(a.ctx(), a, b)); }
inline expr smod(expr const & a, int b) { return smod(a, a.ctx().num_val(b, a.get_sort())); }
inline expr smod(int a, expr const & b) { return smod(b.ctx().num_val(a, b.get_sort()), b); }
/**
\brief unsigned reminder operator for bitvectors
@ -2455,6 +2474,11 @@ namespace z3 {
inline expr context::bv_val(__int64 n, unsigned sz) { Z3_ast r = Z3_mk_int64(m_ctx, n, bv_sort(sz)); check_error(); return expr(*this, r); }
inline expr context::bv_val(__uint64 n, unsigned sz) { Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, bv_sort(sz)); check_error(); return expr(*this, r); }
inline expr context::bv_val(char const * n, unsigned sz) { Z3_ast r = Z3_mk_numeral(m_ctx, n, bv_sort(sz)); check_error(); return expr(*this, r); }
inline expr context::bv_val(unsigned n, bool const* bits) {
array<Z3_bool> _bits(n);
for (unsigned i = 0; i < n; ++i) _bits[i] = bits[i] ? 1 : 0;
Z3_ast r = Z3_mk_bv_numeral(m_ctx, n, _bits.ptr()); check_error(); return expr(*this, r);
}
inline expr context::string_val(char const* s) { Z3_ast r = Z3_mk_string(m_ctx, s); check_error(); return expr(*this, r); }
inline expr context::string_val(std::string const& s) { Z3_ast r = Z3_mk_string(m_ctx, s.c_str()); check_error(); return expr(*this, r); }

14
src/api/dotnet/Context.cs
View file

@ -3127,6 +3127,20 @@ namespace Microsoft.Z3
return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
}
/// <summary>
/// Create a bit-vector numeral.
/// </summary>
/// <param name="bits">An array of bits representing the bit-vector. Least signficant bit is at position 0.</param>
public BitVecNum MkBV(bool[] bits)
{
Contract.Ensures(Contract.Result<BitVecNum>() != null);
int[] _bits = new int[bits.Length];
for (int i = 0; i < bits.Length; ++i) _bits[i] = bits[i] ? 1 : 0;
return (BitVecNum)Expr.Create(this, Native.Z3_mk_bv_numeral(nCtx, (uint)bits.Length, _bits));
}
#endregion
#endregion // Numerals

8
src/api/z3_api.h
View file

@ -3248,6 +3248,14 @@ extern "C" {
*/
Z3_ast Z3_API Z3_mk_unsigned_int64(Z3_context c, __uint64 v, Z3_sort ty);
/**
\brief create a bit-vector numeral from a vector of Booleans.
\sa Z3_mk_numeral
def_API('Z3_mk_bv_numeral', AST, (_in(CONTEXT), _in(UINT), _in_array(1, BOOL)))
*/
Z3_ast Z3_API Z3_mk_bv_numeral(Z3_context c, unsigned sz, Z3_bool const* bits);
/*@}*/
/** @name Sequences and regular expressions */

13
src/ast/ast.cpp
View file

@ -1684,22 +1684,9 @@ ast * ast_manager::register_node_core(ast * n) {
CASSERT("nondet_bug", contains || slow_not_contains(n));
#endif
#if 0
static unsigned counter = 0;
counter++;
if (counter % 100000 == 0)
verbose_stream() << "[ast-table] counter: " << counter << " collisions: " << m_ast_table.collisions() << " capacity: " << m_ast_table.capacity() << " size: " << m_ast_table.size() << "\n";
#endif
ast * r = m_ast_table.insert_if_not_there(n);
SASSERT(r->m_hash == h);
if (r != n) {
#if 0
static unsigned reused = 0;
reused++;
if (reused % 100000 == 0)
verbose_stream() << "[ast-table] reused: " << reused << "\n";
#endif
SASSERT(contains);
SASSERT(m_ast_table.contains(n));
if (is_func_decl(r) && to_func_decl(r)->get_range() != to_func_decl(n)->get_range()) {

2
src/ast/rewriter/poly_rewriter_def.h
View file

@ -687,7 +687,7 @@ br_status poly_rewriter<Config>::mk_sub(unsigned num_args, expr * const * args,
}
set_curr_sort(m().get_sort(args[0]));
expr_ref minus_one(mk_numeral(numeral(-1)), m());
ptr_buffer<expr> new_args;
expr_ref_buffer new_args(m());
new_args.push_back(args[0]);
for (unsigned i = 1; i < num_args; i++) {
if (is_zero(args[i])) continue;

19
src/muz/base/dl_util.cpp
View file

@ -277,16 +277,21 @@ namespace datalog {
return get_max_var(has_var);
}
void del_rule(horn_subsume_model_converter* mc, rule& r) {
void del_rule(horn_subsume_model_converter* mc, rule& r, bool unreachable) {
if (mc) {
ast_manager& m = mc->get_manager();
expr_ref_vector body(m);
for (unsigned i = 0; i < r.get_tail_size(); ++i) {
if (r.is_neg_tail(i)) {
body.push_back(m.mk_not(r.get_tail(i)));
}
else {
body.push_back(r.get_tail(i));
if (unreachable) {
body.push_back(m.mk_false());
}
else {
for (unsigned i = 0; i < r.get_tail_size(); ++i) {
if (r.is_neg_tail(i)) {
body.push_back(m.mk_not(r.get_tail(i)));
}
else {
body.push_back(r.get_tail(i));
}
}
}
TRACE("dl_dr",

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

@ -354,7 +354,7 @@ namespace datalog {
unsigned get_max_rule_var(const rule& r);
};
void del_rule(horn_subsume_model_converter* mc, rule& r);
void del_rule(horn_subsume_model_converter* mc, rule& r, bool unreachable);
void resolve_rule(rule_manager& rm,
replace_proof_converter* pc, rule const& r1, rule const& r2, unsigned idx,

3
src/muz/transforms/dl_mk_interp_tail_simplifier.cpp
View file

@ -607,6 +607,9 @@ namespace datalog {
rule_set * res = alloc(rule_set, m_context);
if (transform_rules(source, *res)) {
res->inherit_predicates(source);
TRACE("dl",
source.display(tout);
res->display(tout););
} else {
dealloc(res);
res = 0;

16
src/muz/transforms/dl_mk_rule_inliner.cpp
View file

@ -426,7 +426,7 @@ namespace datalog {
for (unsigned i = 0; i < m_inlined_rules.get_num_rules(); ++i) {
rule* r = m_inlined_rules.get_rule(i);
datalog::del_rule(m_mc, *r);
datalog::del_rule(m_mc, *r, true);
}
}
@ -465,7 +465,7 @@ namespace datalog {
}
}
if (modified) {
datalog::del_rule(m_mc, *r0);
datalog::del_rule(m_mc, *r0, true);
}
return modified;
@ -488,9 +488,9 @@ namespace datalog {
}
if (something_done && m_mc) {
for (rule_set::iterator rit = orig.begin(); rit!=rend; ++rit) {
if (inlining_allowed(orig, (*rit)->get_decl())) {
datalog::del_rule(m_mc, **rit);
for (rule* r : orig) {
if (inlining_allowed(orig, r->get_decl())) {
datalog::del_rule(m_mc, *r, true);
}
}
}
@ -580,7 +580,7 @@ namespace datalog {
// nothing unifies with the tail atom, therefore the rule is unsatisfiable
// (we can say this because relation pred doesn't have any ground facts either)
res = 0;
datalog::del_rule(m_mc, *r);
datalog::del_rule(m_mc, *r, false);
return true;
}
if (!is_oriented_rewriter(inlining_candidate, strat)) {
@ -590,7 +590,7 @@ namespace datalog {
goto process_next_tail;
}
if (!try_to_inline_rule(*r, *inlining_candidate, ti, res)) {
datalog::del_rule(m_mc, *r);
datalog::del_rule(m_mc, *r, false);
res = 0;
}
return true;
@ -823,7 +823,7 @@ namespace datalog {
if (num_tail_unifiers == 1) {
TRACE("dl", tout << "setting invalid: " << j << "\n";);
valid.set(j, false);
datalog::del_rule(m_mc, *r2);
datalog::del_rule(m_mc, *r2, true);
del_rule(r2, j);
}

27
src/muz/transforms/dl_mk_slice.cpp
View file

@ -426,8 +426,8 @@ namespace datalog {
bool change = true;
while (change) {
change = false;
for (unsigned i = 0; i < src.get_num_rules(); ++i) {
change = prune_rule(*src.get_rule(i)) || change;
for (rule* r : src) {
change = prune_rule(*r) || change;
}
}
}
@ -457,18 +457,19 @@ namespace datalog {
void mk_slice::solve_vars(rule& r, uint_set& used_vars, uint_set& parameter_vars) {
expr_ref_vector conjs = get_tail_conjs(r);
for (unsigned j = 0; j < conjs.size(); ++j) {
expr* e = conjs[j].get();
for (expr * e : conjs) {
expr_ref r(m);
unsigned v;
if (is_eq(e, v, r) && is_output(v) && m_var_is_sliceable[v]) {
TRACE("dl", tout << "is_eq: " << mk_pp(e, m) << " " << (m_solved_vars[v].get()?"solved":"new") << "\n";);
add_var(v);
if (!m_solved_vars[v].get()) {
TRACE("dl", tout << v << " is solved\n";);
add_free_vars(parameter_vars, r);
m_solved_vars[v] = r;
}
else {
TRACE("dl", tout << v << " is used\n";);
// variables can only be solved once.
add_free_vars(used_vars, e);
add_free_vars(used_vars, m_solved_vars[v].get());
@ -508,10 +509,9 @@ namespace datalog {
//
uint_set used_vars, parameter_vars;
solve_vars(r, used_vars, parameter_vars);
uint_set::iterator it = used_vars.begin(), end = used_vars.end();
for (; it != end; ++it) {
if (*it < m_var_is_sliceable.size()) {
m_var_is_sliceable[*it] = false;
for (unsigned uv : used_vars) {
if (uv < m_var_is_sliceable.size()) {
m_var_is_sliceable[uv] = false;
}
}
//
@ -533,6 +533,9 @@ namespace datalog {
if (m_solved_vars[i].get()) {
m_var_is_sliceable[i] = false;
}
if (parameter_vars.contains(i)) {
m_var_is_sliceable[i] = false;
}
}
else if (is_output) {
if (parameter_vars.contains(i)) {
@ -687,11 +690,9 @@ namespace datalog {
}
void mk_slice::display(std::ostream& out) {
obj_map<func_decl, bit_vector>::iterator it = m_sliceable.begin();
obj_map<func_decl, bit_vector>::iterator end = m_sliceable.end();
for (; it != end; ++it) {
out << it->m_key->get_name() << " ";
bit_vector const& bv = it->m_value;
for (auto const& kv : m_sliceable) {
out << kv.m_key->get_name() << " ";
bit_vector const& bv = kv.m_value;
for (unsigned i = 0; i < bv.size(); ++i) {
out << (bv.get(i)?"1":"0");
}

53
src/muz/transforms/dl_mk_subsumption_checker.cpp
View file

@ -24,8 +24,10 @@ Revision History:
#include "ast/rewriter/rewriter.h"
#include "ast/rewriter/rewriter_def.h"
#include "muz/transforms/dl_mk_subsumption_checker.h"
#include "muz/base/fixedpoint_params.hpp"
#include "tactic/extension_model_converter.h"
namespace datalog {
@ -37,26 +39,28 @@ namespace datalog {
bool mk_subsumption_checker::is_total_rule(const rule * r) {
if(r->get_tail_size()!=0) { return false; }
if (r->get_tail_size() != 0) {
return false;
}
unsigned pt_len = r->get_positive_tail_size();
if(pt_len!=r->get_uninterpreted_tail_size()) {
//we dont' expect rules with negative tails to be total
if(pt_len != r->get_uninterpreted_tail_size()) {
// we dont' expect rules with negative tails to be total
return false;
}
for(unsigned i=0; i<pt_len; i++) {
for (unsigned i = 0; i < pt_len; i++) {
func_decl * tail_pred = r->get_tail(i)->get_decl();
if(!m_total_relations.contains(tail_pred)) {
//this rule has a non-total predicate in the tail
if (!m_total_relations.contains(tail_pred)) {
// this rule has a non-total predicate in the tail
return false;
}
}
unsigned t_len = r->get_positive_tail_size();
for(unsigned i=pt_len; i<t_len; i++) {
for(unsigned i = pt_len; i < t_len; i++) {
SASSERT(!r->is_neg_tail(i)); //we assume interpreted tail not to be negated
if(!m.is_true(r->get_tail(i))) {
if (!m.is_true(r->get_tail(i))) {
//this rule has an interpreted tail which is not constant true
return false;
}
@ -183,20 +187,15 @@ namespace datalog {
rule_ref_vector orig_rules(m_context.get_rule_manager());
orig_rules.append(orig.get_num_rules(), orig.begin());
rule * * rbegin = orig_rules.c_ptr();
rule * * rend = rbegin + orig_rules.size();
//before traversing we sort rules so that the shortest are in the beginning.
//this will help make subsumption checks more efficient
std::sort(rbegin, rend, rule_size_comparator);
std::sort(orig_rules.c_ptr(), orig_rules.c_ptr() + orig_rules.size(), rule_size_comparator);
for(rule_set::iterator rit = rbegin; rit!=rend; ++rit) {
rule * r = *rit;
for (rule * r : orig_rules) {
func_decl * head_pred = r->get_decl();
if(m_total_relations.contains(head_pred)) {
if(!orig.is_output_predicate(head_pred) ||
if (m_total_relations.contains(head_pred)) {
if (!orig.is_output_predicate(head_pred) ||
total_relations_with_included_rules.contains(head_pred)) {
//We just skip definitions of total non-output relations as
//we'll eliminate them from the problem.
@ -205,8 +204,7 @@ namespace datalog {
modified = true;
continue;
}
rule * defining_rule;
VERIFY(m_total_relation_defining_rules.find(head_pred, defining_rule));
rule * defining_rule = m_total_relation_defining_rules.find(head_pred);
if (defining_rule) {
rule_ref totality_rule(m_context.get_rule_manager());
VERIFY(transform_rule(defining_rule, subs_index, totality_rule));
@ -224,24 +222,31 @@ namespace datalog {
}
rule_ref new_rule(m_context.get_rule_manager());
if(!transform_rule(r, subs_index, new_rule)) {
if (!transform_rule(r, subs_index, new_rule)) {
modified = true;
continue;
}
if(m_new_total_relation_discovery_during_transformation && is_total_rule(new_rule)) {
if (m_new_total_relation_discovery_during_transformation && is_total_rule(new_rule)) {
on_discovered_total_relation(head_pred, new_rule.get());
}
if(subs_index.is_subsumed(new_rule)) {
if (subs_index.is_subsumed(new_rule)) {
modified = true;
continue;
}
if(new_rule.get()!=r) {
if (new_rule.get()!=r) {
modified = true;
}
tgt.add_rule(new_rule);
subs_index.add(new_rule);
}
tgt.inherit_predicates(orig);
if (!m_total_relations.empty() && m_context.get_model_converter()) {
extension_model_converter* mc0 = alloc(extension_model_converter, m);
for (func_decl* p : m_total_relations) {
mc0->insert(p, m.mk_true());
}
m_context.add_model_converter(mc0);
}
TRACE("dl",
tout << "original set size: "<<orig.get_num_rules()<<"\n"
<< "reduced set size: "<<tgt.get_num_rules()<<"\n"; );

31
src/qe/qe_lite.cpp
View file

@ -20,7 +20,6 @@ Revision History:
#include "qe/qe_lite.h"
#include "ast/expr_abstract.h"
#include "ast/used_vars.h"
#include "ast/occurs.h"
#include "ast/rewriter/rewriter_def.h"
#include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h"
@ -39,6 +38,30 @@ Revision History:
#include "qe/qe_vartest.h"
namespace eq {
bool occurs_var(unsigned idx, expr* e) {
ptr_buffer<expr> todo;
todo.push_back(e);
ast_mark mark;
while (!todo.empty()) {
expr* e = todo.back();
todo.pop_back();
if (mark.is_marked(e)) continue;
mark.mark(e, true);
if (is_var(e)) {
if (to_var(e)->get_idx() == idx) return true;
}
else if (is_app(e)) {
todo.append(to_app(e)->get_num_args(), to_app(e)->get_args());
}
else if (is_quantifier(e)) {
quantifier* q = to_quantifier(e);
if (occurs_var(idx + q->get_num_decls(), q->get_expr())) return true;
}
}
return false;
}
class der {
ast_manager & m;
arith_util a;
@ -65,7 +88,7 @@ namespace eq {
for (unsigned i = 0; i < definitions.size(); i++) {
var * v = vars[i];
expr * t = definitions[i];
if (t == 0 || has_quantifiers(t) || occurs(v, t))
if (t == 0 || has_quantifiers(t) || occurs_var(v->get_idx(), t))
definitions[i] = 0;
else
found = true; // found at least one candidate
@ -679,9 +702,9 @@ namespace eq {
}
bool is_unconstrained(var* x, expr* t, unsigned i, expr_ref_vector const& conjs) {
bool occ = occurs(x, t);
bool occ = occurs_var(x->get_idx(), t);
for (unsigned j = 0; !occ && j < conjs.size(); ++j) {
occ = (i != j) && occurs(x, conjs[j]);
occ = (i != j) && occurs_var(x->get_idx(), conjs[j]);
}
return !occ;
}

2
src/smt/smt_context.cpp
View file

@ -4373,7 +4373,7 @@ namespace smt {
void context::add_rec_funs_to_model() {
ast_manager& m = m_manager;
SASSERT(m_model);
for (unsigned i = 0; i < m_asserted_formulas.get_num_formulas(); ++i) {
for (unsigned i = 0; !get_cancel_flag() && i < m_asserted_formulas.get_num_formulas(); ++i) {
expr* e = m_asserted_formulas.get_formula(i);
if (is_quantifier(e)) {
TRACE("context", tout << mk_pp(e, m) << "\n";);

7
src/smt/smt_context.h
View file

@ -209,7 +209,12 @@ namespace smt {
~scoped_mk_model() {
if (m_ctx.m_proto_model.get() != 0) {
m_ctx.m_model = m_ctx.m_proto_model->mk_model();
m_ctx.add_rec_funs_to_model();
try {
m_ctx.add_rec_funs_to_model();
}
catch (...) {
// no op
}
m_ctx.m_proto_model = 0; // proto_model is not needed anymore.
}
}

38
src/smt/theory_str.cpp
View file

@ -47,6 +47,8 @@ namespace smt {
sLevel(0),
finalCheckProgressIndicator(false),
m_trail(m),
m_factory(nullptr),
m_unused_id(0),
m_delayed_axiom_setup_terms(m),
tmpStringVarCount(0),
tmpXorVarCount(0),
@ -61,8 +63,8 @@ namespace smt {
cacheHitCount(0),
cacheMissCount(0),
m_fresh_id(0),
m_find(*this),
m_trail_stack(*this)
m_trail_stack(*this),
m_find(*this)
{
initialize_charset();
}
@ -279,7 +281,7 @@ namespace smt {
} else {
theory_var v = theory::mk_var(n);
m_find.mk_var();
TRACE("str", tout << "new theory var v#" << v << std::endl;);
TRACE("str", tout << "new theory var v#" << v << " find " << m_find.find(v) << std::endl;);
get_context().attach_th_var(n, this, v);
get_context().mark_as_relevant(n);
return v;
@ -1903,8 +1905,8 @@ namespace smt {
// support for user_smt_theory-style EQC handling
app * theory_str::get_ast(theory_var i) {
return get_enode(i)->get_owner();
app * theory_str::get_ast(theory_var v) {
return get_enode(v)->get_owner();
}
theory_var theory_str::get_var(expr * n) const {
@ -4648,14 +4650,20 @@ namespace smt {
// We only check m_find for a string constant.
expr * theory_str::z3str2_get_eqc_value(expr * n , bool & hasEqcValue) {
expr * curr = n;
do {
if (u.str.is_string(curr)) {
hasEqcValue = true;
return curr;
}
curr = get_eqc_next(curr);
} while (curr != n);
theory_var curr = get_var(n);
if (curr != null_theory_var) {
curr = m_find.find(curr);
theory_var first = curr;
do {
expr* a = get_ast(curr);
if (u.str.is_string(a)) {
hasEqcValue = true;
return a;
}
curr = m_find.next(curr);
}
while (curr != first && curr != null_theory_var);
}
hasEqcValue = false;
return n;
}
@ -10584,7 +10592,9 @@ namespace smt {
return alloc(expr_wrapper_proc, val);
} else {
TRACE("str", tout << "WARNING: failed to find a concrete value, falling back" << std::endl;);
return alloc(expr_wrapper_proc, to_app(mk_string("**UNUSED**")));
std::ostringstream unused;
unused << "**UNUSED**" << (m_unused_id++);
return alloc(expr_wrapper_proc, to_app(mk_string(unused.str().c_str())));
}
}

6
src/smt/theory_str.h
View file

@ -267,6 +267,10 @@ protected:
str_value_factory * m_factory;
// Unique identifier appended to unused variables to ensure that model construction
// does not introduce equalities when they weren't enforced.
unsigned m_unused_id;
// terms we couldn't go through set_up_axioms() with because they weren't internalized
expr_ref_vector m_delayed_axiom_setup_terms;
@ -358,8 +362,8 @@ protected:
// cache mapping each string S to Length(S)
obj_map<expr, app*> length_ast_map;
th_union_find m_find;
th_trail_stack m_trail_stack;
th_union_find m_find;
theory_var get_var(expr * n) const;
expr * get_eqc_next(expr * n);
app * get_ast(theory_var i);

4
src/tactic/arith/diff_neq_tactic.cpp
View file

@ -95,13 +95,13 @@ class diff_neq_tactic : public tactic {
if (is_uninterp_const(lhs) && u.is_numeral(rhs, k) && m_max_neg_k <= k && k <= m_max_k) {
var x = mk_var(lhs);
int _k = static_cast<int>(k.get_int64());
m_upper[x] = _k;
m_upper[x] = std::min(m_upper[x], _k);
}
else if (is_uninterp_const(rhs) && u.is_numeral(lhs, k) && m_max_neg_k <= k && k <= m_max_k) {
var x = mk_var(rhs);
int _k = static_cast<int>(k.get_int64());
m_lower[x] = _k;
m_lower[x] = std::max(m_lower[x], _k);
}
else {
throw_not_supported();

2
src/util/lp/lar_solver.h
View file

@ -1157,7 +1157,7 @@ public:
bool explanation_is_correct(const vector<std::pair<mpq, unsigned>>& explanation) const {
#ifdef Z3DEBUG
lconstraint_kind kind;
lconstraint_kind kind = EQ; // initialize it just to avoid a warning
SASSERT(the_relations_are_of_same_type(explanation, kind));
SASSERT(the_left_sides_sum_to_zero(explanation));
mpq rs = sum_of_right_sides_of_explanation(explanation);

1
src/util/union_find.h
View file

@ -102,6 +102,7 @@ public:
unsigned find(unsigned v) const {
while (true) {
SASSERT(v < m_find.size());
unsigned new_v = m_find[v];
if (new_v == v)
return v;