mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 03:45:51 +00:00
Code Activity

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

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-01-28 11:14:11 +00:00
commit 20df9e1cd1
13 changed files with 579 additions and 325 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/api/api_context.cpp
View file

@ -76,7 +76,6 @@ namespace api {
m_sutil(m()),
m_last_result(m()),
m_ast_trail(m()),
m_replay_stack(),
m_pmanager(m_limit) {
m_error_code = Z3_OK;
@ -100,23 +99,12 @@ namespace api {
m_fpa_fid = m().mk_family_id("fpa");
m_seq_fid = m().mk_family_id("seq");
m_dt_plugin = static_cast<datatype_decl_plugin*>(m().get_plugin(m_dt_fid));
if (!m_user_ref_count) {
m_replay_stack.push_back(0);
}
install_tactics(*this);
}
context::~context() {
m_last_obj = 0;
if (!m_user_ref_count) {
for (unsigned i = 0; i < m_replay_stack.size(); ++i) {
dealloc(m_replay_stack[i]);
}
m_ast_trail.reset();
}
reset_parser();
}

8
src/api/api_context.h
View file

@ -58,7 +58,7 @@ namespace api {
bv_util m_bv_util;
datalog::dl_decl_util m_datalog_util;
fpa_util m_fpa_util;
datatype_util m_dtutil;
datatype_util m_dtutil;
seq_util m_sutil;
// Support for old solver API
@ -67,8 +67,6 @@ namespace api {
ast_ref_vector m_last_result; //!< used when m_user_ref_count == true
ast_ref_vector m_ast_trail; //!< used when m_user_ref_count == false
unsigned_vector m_ast_lim;
ptr_vector<ast_ref_vector> m_replay_stack;
ref<api::object> m_last_obj; //!< reference to the last API object returned by the APIs
@ -123,7 +121,7 @@ namespace api {
bv_util & bvutil() { return m_bv_util; }
datalog::dl_decl_util & datalog_util() { return m_datalog_util; }
fpa_util & fpautil() { return m_fpa_util; }
datatype_util& dtutil() { return m_dtutil; }
datatype_util& dtutil() { return m_dtutil; }
seq_util& sutil() { return m_sutil; }
family_id get_basic_fid() const { return m_basic_fid; }
family_id get_array_fid() const { return m_array_fid; }
@ -181,8 +179,6 @@ namespace api {
void interrupt();
void invoke_error_handler(Z3_error_code c);
static void out_of_memory_handler(void * _ctx);
void check_sorts(ast * n);

3
src/api/z3_api.h
View file

@ -4419,6 +4419,9 @@ extern "C" {
\brief Interface to simplifier.
Provides an interface to the AST simplifier used by Z3.
It returns an AST object which is equal to the argument.
The returned AST is simplified using algebraic simplificaiton rules,
such as constant propagation (propagating true/false over logical connectives).
def_API('Z3_simplify', AST, (_in(CONTEXT), _in(AST)))
*/

63
src/ast/rewriter/seq_rewriter.cpp
View file

@ -36,6 +36,7 @@ expr_ref sym_expr::accept(expr* e) {
break;
}
case t_char:
SASSERT(m.get_sort(e) == m.get_sort(m_t));
result = m.mk_eq(e, m_t);
break;
case t_range: {
@ -374,7 +375,7 @@ br_status seq_rewriter::mk_seq_length(expr* a, expr_ref& result) {
es.push_back(m_autil.mk_numeral(rational(len, rational::ui64()), true));
}
result = m_autil.mk_add(es.size(), es.c_ptr());
return BR_DONE;
return BR_REWRITE2;
}
return BR_FAILED;
}
@ -383,7 +384,7 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
zstring s;
rational pos, len;
if (m_util.str.is_string(a, s) && m_autil.is_numeral(b, pos) && m_autil.is_numeral(c, len) &&
pos.is_unsigned() && len.is_unsigned() && pos.get_unsigned() <= s.length()) {
pos.is_unsigned() && len.is_unsigned() && pos.get_unsigned() + len.get_unsigned() <= s.length()) {
unsigned _pos = pos.get_unsigned();
unsigned _len = len.get_unsigned();
result = m_util.str.mk_string(s.extract(_pos, _len));
@ -538,34 +539,40 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
}
}
}
if (a1 != b1) {
return BR_FAILED;
}
m_util.str.get_concat(a, as);
m_util.str.get_concat(b, bs);
unsigned i = 0;
bool all_values = true;
expr_ref_vector eqs(m());
for (; i < as.size() && i < bs.size(); ++i) {
all_values &= m().is_value(as[i].get()) && m().is_value(bs[i].get());
if (as[i].get() != bs[i].get()) {
if (all_values) {
result = m().mk_false();
return BR_DONE;
}
break;
expr* a = as[i].get(), *b = bs[i].get();
if (a == b) {
continue;
}
};
all_values &= m().is_value(a) && m().is_value(b);
if (all_values) {
result = m().mk_false();
return BR_DONE;
}
if (m_util.str.is_unit(a) && m_util.str.is_unit(b)) {
eqs.push_back(m().mk_eq(a, b));
continue;
}
break;
}
if (i == as.size()) {
result = m().mk_true();
return BR_DONE;
result = mk_and(eqs);
if (m().is_true(result)) {
return BR_DONE;
}
return BR_REWRITE3;
}
SASSERT(i < as.size());
if (i == bs.size()) {
expr_ref_vector es(m());
for (unsigned j = i; j < as.size(); ++j) {
es.push_back(m().mk_eq(m_util.str.mk_empty(m().get_sort(a)), as[j].get()));
eqs.push_back(m().mk_eq(m_util.str.mk_empty(m().get_sort(a)), as[j].get()));
}
result = mk_and(es);
result = mk_and(eqs);
return BR_REWRITE3;
}
if (i > 0) {
@ -575,8 +582,9 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
result = m_util.str.mk_prefix(a, b);
return BR_DONE;
}
UNREACHABLE();
return BR_FAILED;
else {
return BR_FAILED;
}
}
br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) {
@ -785,8 +793,8 @@ bool seq_rewriter::is_sequence(expr* e, expr_ref_vector& seq) {
else if (m_util.str.is_empty(e)) {
continue;
}
else if (m_util.str.is_unit(e)) {
seq.push_back(e);
else if (m_util.str.is_unit(e, e1)) {
seq.push_back(e1);
}
else if (m_util.str.is_concat(e, e1, e2)) {
todo.push_back(e1);
@ -1170,14 +1178,13 @@ bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_
rs.pop_back();
}
else {
expr_ref s2(m_util.str.mk_string(s.extract(0, s.length()-2)), m());
expr_ref s2(m_util.str.mk_string(s.extract(0, s.length()-1)), m());
rs[rs.size()-1] = s2;
}
}
else {
break;
}
TRACE("seq", tout << "change back\n";);
change = true;
lchange = true;
}
@ -1222,19 +1229,19 @@ bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_
SASSERT(m().get_sort(ch) == m().get_sort(a));
lhs.push_back(ch);
rhs.push_back(a);
ls.pop_back();
++head1;
if (s.length() == 1) {
rs.pop_back();
++head2;
}
else {
expr_ref s2(m_util.str.mk_string(s.extract(1, s.length()-1)), m());
rs[rs.size()-1] = s2;
rs[head2] = s2;
}
}
else {
break;
}
TRACE("seq", tout << "change front\n";);
TRACE("seq", tout << ls << " == " << rs << "\n";);
change = true;
lchange = true;

28
src/ast/seq_decl_plugin.cpp
View file

@ -31,6 +31,10 @@ static bool is_hex_digit(char ch, unsigned& d) {
d = 10 + ch - 'A';
return true;
}
if ('a' <= ch && ch <= 'f') {
d = 10 + ch - 'a';
return true;
}
return false;
}
@ -85,6 +89,7 @@ static bool is_escape_char(char const *& s, unsigned& result) {
s += 2;
return true;
}
return false;
}
zstring::zstring(encoding enc): m_encoding(enc) {}
@ -143,11 +148,15 @@ zstring zstring::replace(zstring const& src, zstring const& dst) const {
if (eq) {
result.m_buffer.append(dst.m_buffer);
found = true;
i += src.length() - 1;
}
else {
result.m_buffer.push_back(m_buffer[i]);
}
}
for (unsigned i = length() - src.length() + 1; i < length(); ++i) {
result.m_buffer.push_back(m_buffer[i]);
}
return result;
}
@ -554,7 +563,11 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
parameter param(symbol(""));
return mk_func_decl(OP_STRING_CONST, 1, &param, 0, 0, m_string);
}
return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));
else {
parameter param(rng.get());
func_decl_info info(m_family_id, k, 1, &param);
return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, info);
}
case OP_SEQ_UNIT:
case OP_RE_PLUS:
@ -736,6 +749,19 @@ bool seq_decl_plugin::is_value(app* e) const {
m_manager->is_value(e->get_arg(0)));
}
expr* seq_decl_plugin::get_some_value(sort* s) {
seq_util util(*m_manager);
if (util.is_seq(s)) {
return util.str.mk_empty(s);
}
sort* seq;
if (util.is_re(s, seq)) {
return util.re.mk_to_re(util.str.mk_empty(seq));
}
UNREACHABLE();
return 0;
}
app* seq_util::mk_skolem(symbol const& name, unsigned n, expr* const* args, sort* range) {
SASSERT(range);
parameter param(name);

4
src/ast/seq_decl_plugin.h
View file

@ -177,10 +177,13 @@ public:
virtual bool is_unique_value(app * e) const { return is_value(e); }
virtual expr * get_some_value(sort * s);
bool is_char(ast* a) const { return a == m_char; }
app* mk_string(symbol const& s);
app* mk_string(zstring const& s);
};
class seq_util {
@ -268,6 +271,7 @@ public:
MATCH_TERNARY(is_extract);
MATCH_BINARY(is_contains);
MATCH_BINARY(is_at);
MATCH_BINARY(is_index);
MATCH_TERNARY(is_index);
MATCH_TERNARY(is_replace);
MATCH_BINARY(is_prefix);

1
src/cmd_context/cmd_context.cpp
View file

@ -1638,6 +1638,7 @@ void cmd_context::validate_model() {
catch (contains_array_op_proc::found) {
continue;
}
TRACE("model_validate", model_smt2_pp(tout, *this, *(md.get()), 0););
throw cmd_exception("an invalid model was generated");
}
}

43
src/parsers/smt2/smt2parser.cpp
View file

@ -432,8 +432,10 @@ namespace smt2 {
}
}
void unknown_sort(symbol id) {
std::string msg = "unknown sort '";
void unknown_sort(symbol id, char const* context = "") {
std::string msg = context;
if (context[0]) msg += ": ";
msg += "unknown sort '";
msg += id.str() + "'";
throw parser_exception(msg.c_str());
}
@ -528,12 +530,12 @@ namespace smt2 {
SASSERT(sexpr_stack().size() == stack_pos + 1);
}
sort * parse_sort_name() {
sort * parse_sort_name(char const* context = "") {
SASSERT(curr_is_identifier());
symbol id = curr_id();
psort_decl * d = m_ctx.find_psort_decl(id);
if (d == 0)
unknown_sort(id);
unknown_sort(id, context);
if (!d->has_var_params() && d->get_num_params() != 0)
throw parser_exception("sort constructor expects parameters");
sort * r = d->instantiate(pm());
@ -689,23 +691,24 @@ namespace smt2 {
next();
}
void parse_sort() {
void parse_sort(char const* context) {
unsigned stack_pos = sort_stack().size();
unsigned num_frames = 0;
do {
if (curr_is_identifier()) {
sort_stack().push_back(parse_sort_name());
sort_stack().push_back(parse_sort_name(context));
}
else if (curr_is_rparen()) {
if (num_frames == 0)
throw parser_exception("invalid sort, unexpected ')'");
if (num_frames == 0) {
throw parser_exception(std::string(context) + " invalid sort, unexpected ')'");
}
pop_sort_app_frame();
num_frames--;
}
else {
check_lparen_next("invalid sort, symbol, '_' or '(' expected");
if (!curr_is_identifier())
throw parser_exception("invalid sort, symbol or '_' expected");
throw parser_exception(std::string(context) + " invalid sort, symbol or '_' expected");
if (curr_id_is_underscore()) {
sort_stack().push_back(parse_indexed_sort());
}
@ -723,7 +726,7 @@ namespace smt2 {
unsigned sz = 0;
check_lparen_next(context);
while (!curr_is_rparen()) {
parse_sort();
parse_sort(context);
sz++;
}
next();
@ -1151,7 +1154,7 @@ namespace smt2 {
symbol_stack().push_back(curr_id());
TRACE("parse_sorted_vars", tout << "push_back curr_id(): " << curr_id() << "\n";);
next();
parse_sort();
parse_sort("invalid sorted variables");
check_rparen_next("invalid sorted variable, ')' expected");
num++;
}
@ -1243,7 +1246,7 @@ namespace smt2 {
has_as = true;
next();
symbol r = parse_indexed_identifier();
parse_sort();
parse_sort("Invalid qualified identifier");
check_rparen_next("invalid qualified identifier, ')' expected");
return r;
}
@ -1848,7 +1851,7 @@ namespace smt2 {
unsigned sort_spos = sort_stack().size();
unsigned expr_spos = expr_stack().size();
unsigned num_vars = parse_sorted_vars();
parse_sort();
parse_sort("Invalid function definition");
parse_expr();
if (m().get_sort(expr_stack().back()) != sort_stack().back())
throw parser_exception("invalid function/constant definition, sort mismatch");
@ -1936,7 +1939,7 @@ namespace smt2 {
unsigned expr_spos = expr_stack().size();
unsigned num_vars = parse_sorted_vars();
SASSERT(num_vars == m_num_bindings);
parse_sort();
parse_sort("Invalid recursive function definition");
f = m().mk_func_decl(id, num_vars, sort_stack().c_ptr() + sort_spos, sort_stack().back());
bindings.append(num_vars, expr_stack().c_ptr() + expr_spos);
ids.append(num_vars, symbol_stack().c_ptr() + sym_spos);
@ -1999,7 +2002,7 @@ namespace smt2 {
check_identifier("invalid constant definition, symbol expected");
symbol id = curr_id();
next();
parse_sort();
parse_sort("Invalid constant definition");
parse_expr();
if (m().get_sort(expr_stack().back()) != sort_stack().back())
throw parser_exception("invalid constant definition, sort mismatch");
@ -2020,7 +2023,7 @@ namespace smt2 {
next();
unsigned spos = sort_stack().size();
unsigned num_params = parse_sorts("Parsing function declaration. Expecting sort list '('");
parse_sort();
parse_sort("Invalid function declaration");
func_decl_ref f(m());
f = m().mk_func_decl(id, num_params, sort_stack().c_ptr() + spos, sort_stack().back());
sort_stack().shrink(spos);
@ -2037,7 +2040,7 @@ namespace smt2 {
check_identifier("invalid constant declaration, symbol expected");
symbol id = curr_id();
next();
parse_sort();
parse_sort("Invalid constant declaration");
SASSERT(!sort_stack().empty());
func_decl_ref c(m());
c = m().mk_const_decl(id, sort_stack().back());
@ -2300,9 +2303,9 @@ namespace smt2 {
next();
}
unsigned spos = sort_stack().size();
parse_sorts("Parsing function name. Expecting sort list startig with '(' to disambiguate function name");
parse_sorts("Invalid function name. Expecting sort list startig with '(' to disambiguate function name");
unsigned domain_size = sort_stack().size() - spos;
parse_sort();
parse_sort("Invalid function name");
func_decl * d = m_ctx.find_func_decl(id, indices.size(), indices.c_ptr(), domain_size, sort_stack().c_ptr() + spos, sort_stack().back());
sort_stack().shrink(spos);
check_rparen_next("invalid function declaration reference, ')' expected");
@ -2375,7 +2378,7 @@ namespace smt2 {
break;
}
case CPK_SORT:
parse_sort();
parse_sort("invalid command argument, sort expected");
m_curr_cmd->set_next_arg(m_ctx, sort_stack().back());
return;
case CPK_SORT_LIST: {

3
src/smt/smt_setup.cpp
View file

@ -847,6 +847,9 @@ namespace smt {
setup_AUFLIA(false);
setup_datatypes();
setup_bv();
setup_dl();
setup_seq();
setup_card();
setup_fpa();
return;
}

692
src/smt/theory_seq.cpp
View file

File diff suppressed because it is too large Load diff

29
src/smt/theory_seq.h
View file

@ -45,6 +45,8 @@ namespace smt {
typedef std::pair<expr*, dependency*> expr_dep;
typedef obj_map<expr, expr_dep> eqdep_map_t;
class seq_value_proc;
// cache to track evaluations under equalities
class eval_cache {
eqdep_map_t m_map;
@ -138,8 +140,7 @@ namespace smt {
m_util.str.get_concat(l, ls);
m_util.str.get_concat(r, rs);
return eq(m_eq_id++, ls, rs, dep);
}
}
class ne {
vector<expr_ref_vector> m_lhs;
@ -192,6 +193,7 @@ namespace smt {
expr_ref m_e;
public:
replay_length_coherence(ast_manager& m, expr* e) : m_e(e, m) {}
virtual ~replay_length_coherence() {}
virtual void operator()(theory_seq& th) {
th.check_length_coherence(m_e);
m_e.reset();
@ -202,6 +204,7 @@ namespace smt {
expr_ref m_e;
public:
replay_axiom(ast_manager& m, expr* e) : m_e(e, m) {}
virtual ~replay_axiom() {}
virtual void operator()(theory_seq& th) {
th.enque_axiom(m_e);
m_e.reset();
@ -336,7 +339,7 @@ namespace smt {
void propagate_lit(dependency* dep, literal lit) { propagate_lit(dep, 0, 0, lit); }
void propagate_lit(dependency* dep, unsigned n, literal const* lits, literal lit);
void propagate_eq(dependency* dep, enode* n1, enode* n2);
void propagate_eq(literal lit, expr* e1, expr* e2, bool add_to_eqs = false);
void propagate_eq(literal lit, expr* e1, expr* e2, bool add_to_eqs);
void set_conflict(dependency* dep, literal_vector const& lits = literal_vector());
u_map<unsigned> m_branch_start;
@ -353,8 +356,10 @@ namespace smt {
bool add_solution(expr* l, expr* r, dependency* dep);
bool is_nth(expr* a) const;
bool is_tail(expr* a, expr*& s, unsigned& idx) const;
bool is_eq(expr* e, expr*& a, expr*& b) const;
expr_ref mk_nth(expr* s, expr* idx);
expr_ref mk_last(expr* e);
expr_ref mk_first(expr* e);
expr_ref canonize(expr* e, dependency*& eqs);
bool canonize(expr* e, expr_ref_vector& es, dependency*& eqs);
bool canonize(expr_ref_vector const& es, expr_ref_vector& result, dependency*& eqs);
@ -366,7 +371,7 @@ namespace smt {
// terms whose meaning are encoded using axioms.
void enque_axiom(expr* e);
void deque_axiom(expr* e);
void add_axiom(literal l1, literal l2 = null_literal, literal l3 = null_literal, literal l4 = null_literal);
void add_axiom(literal l1, literal l2 = null_literal, literal l3 = null_literal, literal l4 = null_literal, literal l5 = null_literal);
void add_indexof_axiom(expr* e);
void add_replace_axiom(expr* e);
void add_extract_axiom(expr* e);
@ -382,7 +387,7 @@ namespace smt {
void add_in_re_axiom(expr* n);
literal mk_literal(expr* n);
literal mk_eq_empty(expr* n);
literal mk_equals(expr* a, expr* b);
literal mk_seq_eq(expr* a, expr* b);
void tightest_prefix(expr* s, expr* x, literal lit, literal lit2 = null_literal);
expr_ref mk_sub(expr* a, expr* b);
enode* ensure_enode(expr* a);
@ -418,12 +423,14 @@ namespace smt {
bool is_step(expr* e, expr*& s, expr*& tail, expr*& re, expr*& i, expr*& j, expr*& t) const;
bool is_step(expr* e) const;
void propagate_step(literal lit, expr* n);
bool add_reject2reject(expr* rej);
bool add_accept2step(expr* acc);
bool add_step2accept(expr* step);
bool add_prefix2prefix(expr* e);
bool add_suffix2suffix(expr* e);
bool add_contains2contains(expr* e);
bool add_reject2reject(expr* rej, bool& change);
bool add_accept2step(expr* acc, bool& change);
bool add_step2accept(expr* step, bool& change);
bool add_prefix2prefix(expr* e, bool& change);
bool add_suffix2suffix(expr* e, bool& change);
bool add_contains2contains(expr* e, bool& change);
void propagate_not_prefix(expr* e);
void propagate_not_suffix(expr* e);
void ensure_nth(literal lit, expr* s, expr* idx);
bool canonizes(bool sign, expr* e);
void propagate_non_empty(literal lit, expr* s);

13
src/tactic/smtlogics/quant_tactics.h
View file

@ -32,4 +32,17 @@ tactic * mk_lra_tactic(ast_manager & m, params_ref const & p);
tactic * mk_lia_tactic(ast_manager & m, params_ref const & p);
tactic * mk_lira_tactic(ast_manager & m, params_ref const & p);
/*
ADD_TACTIC("ufnia", "builtin strategy for solving UFNIA problems.", "mk_ufnia_tactic(m, p)")
ADD_TACTIC("uflra", "builtin strategy for solving UFLRA problems.", "mk_uflra_tactic(m, p)")
ADD_TACTIC("auflia", "builtin strategy for solving AUFLIA problems.", "mk_auflia_tactic(m, p)")
ADD_TACTIC("auflira", "builtin strategy for solving AUFLIRA problems.", "mk_auflira_tactic(m, p)")
ADD_TACTIC("aufnira", "builtin strategy for solving AUFNIRA problems.", "mk_aufnira_tactic(m, p)")
ADD_TACTIC("lra", "builtin strategy for solving LRA problems.", "mk_lra_tactic(m, p)")
ADD_TACTIC("lia", "builtin strategy for solving LIA problems.", "mk_lia_tactic(m, p)")
ADD_TACTIC("lira", "builtin strategy for solving LIRA problems.", "mk_lira_tactic(m, p)")
*/
#endif

5
src/util/memory_manager.h
View file

@ -46,11 +46,6 @@ public:
out_of_memory_error();
};
class exceeded_memory_allocations : public z3_error {
public:
exceeded_memory_allocations();
};
class memory {
public:
static bool is_out_of_memory();