mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-20 02:00:22 +00:00
Code Activity

Merge branch 'develop' into regex-develop

Browse source
This commit is contained in:
Murphy Berzish 2018-04-03 12:31:27 -04:00
commit 41703a4254
40 changed files with 721 additions and 485 deletions
Download patch file Download diff file Expand all files Collapse all files

108
src/smt/smt_context_pp.cpp
View file

@ -19,7 +19,7 @@ Revision History:
#include "smt/smt_context.h"
#include "ast/ast_ll_pp.h"
#include "ast/ast_pp.h"
#include "ast/ast_smt_pp.h"
#include "ast/ast_pp_util.h"
#include "util/stats.h"
namespace smt {
@ -43,11 +43,10 @@ namespace smt {
return out << "RESOURCE_LIMIT";
case THEORY:
if (!m_incomplete_theories.empty()) {
ptr_vector<theory>::const_iterator it = m_incomplete_theories.begin();
ptr_vector<theory>::const_iterator end = m_incomplete_theories.end();
for (bool first = true; it != end; ++it) {
bool first = true;
for (theory* th : m_incomplete_theories) {
if (first) first = false; else out << " ";
out << (*it)->get_name();
out << th->get_name();
}
}
else {
@ -173,12 +172,10 @@ namespace smt {
void context::display_binary_clauses(std::ostream & out) const {
bool first = true;
vector<watch_list>::const_iterator it = m_watches.begin();
vector<watch_list>::const_iterator end = m_watches.end();
for (unsigned l_idx = 0; it != end; ++it, ++l_idx) {
literal l1 = to_literal(l_idx);
unsigned l_idx = 0;
for (watch_list const& wl : m_watches) {
literal l1 = to_literal(l_idx++);
literal neg_l1 = ~l1;
watch_list const & wl = *it;
literal const * it2 = wl.begin_literals();
literal const * end2 = wl.end_literals();
for (; it2 != end2; ++it2) {
@ -291,10 +288,7 @@ namespace smt {
}
void context::display_theories(std::ostream & out) const {
ptr_vector<theory>::const_iterator it = m_theory_set.begin();
ptr_vector<theory>::const_iterator end = m_theory_set.end();
for (; it != end; ++it) {
theory * th = *it;
for (theory* th : m_theory_set) {
th->display(out);
}
}
@ -393,10 +387,8 @@ namespace smt {
#endif
m_qmanager->collect_statistics(st);
m_asserted_formulas.collect_statistics(st);
ptr_vector<theory>::const_iterator it = m_theory_set.begin();
ptr_vector<theory>::const_iterator end = m_theory_set.end();
for (; it != end; ++it) {
(*it)->collect_statistics(st);
for (theory* th : m_theory_set) {
th->collect_statistics(st);
}
}
@ -413,19 +405,23 @@ namespace smt {
}
void context::display_lemma_as_smt_problem(std::ostream & out, unsigned num_antecedents, literal const * antecedents, literal consequent, symbol const& logic) const {
ast_smt_pp pp(m_manager);
pp.set_benchmark_name("lemma");
pp.set_status("unsat");
pp.set_logic(logic);
ast_pp_util visitor(m_manager);
expr_ref_vector fmls(m_manager);
visitor.collect(fmls);
expr_ref n(m_manager);
for (unsigned i = 0; i < num_antecedents; i++) {
literal l = antecedents[i];
expr_ref n(m_manager);
literal2expr(l, n);
pp.add_assumption(n);
fmls.push_back(n);
}
expr_ref n(m_manager);
literal2expr(~consequent, n);
pp.display_smt2(out, n);
if (consequent != false_literal) {
literal2expr(~consequent, n);
fmls.push_back(n);
}
if (logic != symbol::null) out << "(set-logic " << logic << ")\n";
visitor.collect(fmls);
visitor.display_decls(out);
visitor.display_asserts(out, fmls, true);
}
static unsigned g_lemma_id = 0;
@ -448,25 +444,29 @@ namespace smt {
void context::display_lemma_as_smt_problem(std::ostream & out, unsigned num_antecedents, literal const * antecedents,
unsigned num_eq_antecedents, enode_pair const * eq_antecedents,
literal consequent, symbol const& logic) const {
ast_smt_pp pp(m_manager);
pp.set_benchmark_name("lemma");
pp.set_status("unsat");
pp.set_logic(logic);
ast_pp_util visitor(m_manager);
expr_ref_vector fmls(m_manager);
visitor.collect(fmls);
expr_ref n(m_manager);
for (unsigned i = 0; i < num_antecedents; i++) {
literal l = antecedents[i];
expr_ref n(m_manager);
literal2expr(l, n);
pp.add_assumption(n);
fmls.push_back(n);
}
for (unsigned i = 0; i < num_eq_antecedents; i++) {
enode_pair const & p = eq_antecedents[i];
expr_ref eq(m_manager);
eq = m_manager.mk_eq(p.first->get_owner(), p.second->get_owner());
pp.add_assumption(eq);
n = m_manager.mk_eq(p.first->get_owner(), p.second->get_owner());
fmls.push_back(n);
}
expr_ref n(m_manager);
literal2expr(~consequent, n);
pp.display_smt2(out, n);
if (consequent != false_literal) {
literal2expr(~consequent, n);
fmls.push_back(n);
}
if (logic != symbol::null) out << "(set-logic " << logic << ")\n";
visitor.collect(fmls);
visitor.display_decls(out);
visitor.display_asserts(out, fmls, true);
}
void context::display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents,
@ -490,10 +490,7 @@ namespace smt {
*/
void context::display_normalized_enodes(std::ostream & out) const {
out << "normalized enodes:\n";
ptr_vector<enode>::const_iterator it = m_enodes.begin();
ptr_vector<enode>::const_iterator end = m_enodes.end();
for (; it != end; ++it) {
enode * n = *it;
for (enode * n : m_enodes) {
out << "#";
out.width(5);
out << std::left << n->get_owner_id() << " #";
@ -524,28 +521,23 @@ namespace smt {
}
void context::display_enodes_lbls(std::ostream & out) const {
ptr_vector<enode>::const_iterator it = m_enodes.begin();
ptr_vector<enode>::const_iterator end = m_enodes.end();
for (; it != end; ++it) {
enode * n = *it;
for (enode* n : m_enodes) {
n->display_lbls(out);
}
}
void context::display_decl2enodes(std::ostream & out) const {
out << "decl2enodes:\n";
vector<enode_vector>::const_iterator it1 = m_decl2enodes.begin();
vector<enode_vector>::const_iterator end1 = m_decl2enodes.end();
for (unsigned id = 0; it1 != end1; ++it1, ++id) {
enode_vector const & v = *it1;
unsigned id = 0;
for (enode_vector const& v : m_decl2enodes) {
if (!v.empty()) {
out << "id " << id << " ->";
enode_vector::const_iterator it2 = v.begin();
enode_vector::const_iterator end2 = v.end();
for (; it2 != end2; ++it2)
out << " #" << (*it2)->get_owner_id();
for (enode* n : v) {
out << " #" << n->get_owner_id();
}
out << "\n";
}
++id;
}
}
@ -588,20 +580,20 @@ namespace smt {
case b_justification::BIN_CLAUSE: {
literal l2 = j.get_literal();
out << "bin-clause ";
display_literal(out, l2);
display_literal_verbose(out, l2);
break;
}
case b_justification::CLAUSE: {
clause * cls = j.get_clause();
out << "clause ";
if (cls) display_literals(out, cls->get_num_literals(), cls->begin_literals());
if (cls) display_literals_verbose(out, cls->get_num_literals(), cls->begin_literals());
break;
}
case b_justification::JUSTIFICATION: {
out << "justification " << j.get_justification()->get_from_theory() << ": ";
literal_vector lits;
const_cast<conflict_resolution&>(*m_conflict_resolution).justification2literals(j.get_justification(), lits);
display_literals(out, lits);
display_literals_verbose(out, lits);
break;
}
default:

2
src/smt/smt_quantifier.cpp
View file

@ -222,7 +222,7 @@ namespace smt {
final_check_status final_check_eh(bool full) {
if (full) {
IF_VERBOSE(100, verbose_stream() << "(smt.final-check \"quantifiers\")\n";);
IF_VERBOSE(100, if (!m_quantifiers.empty()) verbose_stream() << "(smt.final-check \"quantifiers\")\n";);
final_check_status result = m_qi_queue.final_check_eh() ? FC_DONE : FC_CONTINUE;
final_check_status presult = m_plugin->final_check_eh(full);
if (presult != FC_DONE)

8
src/smt/theory_seq.cpp
View file

@ -2404,8 +2404,7 @@ bool theory_seq::add_stoi_val_axiom(expr* e) {
lits.push_back(~is_digit(ith_char));
nums.push_back(digit2int(ith_char));
}
for (unsigned i = sz-1, c = 1; i > 0; c *= 10) {
--i;
for (unsigned i = sz, c = 1; i-- > 0; c *= 10) {
coeff = m_autil.mk_int(c);
nums[i] = m_autil.mk_mul(coeff, nums[i].get());
}
@ -2414,9 +2413,10 @@ bool theory_seq::add_stoi_val_axiom(expr* e) {
lits.push_back(mk_eq(e, num, false));
++m_stats.m_add_axiom;
m_new_propagation = true;
for (unsigned i = 0; i < lits.size(); ++i) {
ctx.mark_as_relevant(lits[i]);
for (literal lit : lits) {
ctx.mark_as_relevant(lit);
}
TRACE("seq", ctx.display_literals_verbose(tout, lits); tout << "\n";);
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
m_stoi_axioms.insert(val);
m_trail_stack.push(insert_map<theory_seq, rational_set, rational>(m_stoi_axioms, val));

612
src/smt/theory_str.cpp
View file

File diff suppressed because it is too large Load diff

61
src/smt/theory_str.h
View file

@ -80,25 +80,8 @@ public:
void register_value(expr * n) override { /* Ignore */ }
};
// rather than modify obj_pair_map I inherit from it and add my own helper methods
class theory_str_contain_pair_bool_map_t : public obj_pair_map<expr, expr, expr*> {
public:
expr * operator[](std::pair<expr*, expr*> key) const {
expr * value;
bool found = this->find(key.first, key.second, value);
if (found) {
return value;
} else {
TRACE("t_str", tout << "WARNING: lookup miss in contain_pair_bool_map!" << std::endl;);
return nullptr;
}
}
bool contains(std::pair<expr*, expr*> key) const {
expr * unused;
return this->find(key.first, key.second, unused);
}
};
// NSB: added operator[] and contains to obj_pair_hashtable
class theory_str_contain_pair_bool_map_t : public obj_pair_map<expr, expr, expr*> {};
template<typename Ctx>
class binary_search_trail : public trail<Ctx> {
@ -236,7 +219,7 @@ class theory_str : public theory {
struct T_cut
{
int level;
std::map<expr*, int> vars;
obj_map<expr, int> vars;
T_cut() {
level = -100;
@ -348,6 +331,7 @@ protected:
ptr_vector<enode> m_concat_axiom_todo;
ptr_vector<enode> m_string_constant_length_todo;
ptr_vector<enode> m_concat_eval_todo;
expr_ref_vector m_delayed_assertions_todo;
// enode lists for library-aware/high-level string terms (e.g. substr, contains)
ptr_vector<enode> m_library_aware_axiom_todo;
@ -365,8 +349,8 @@ protected:
int tmpXorVarCount;
int tmpLenTestVarCount;
int tmpValTestVarCount;
std::map<std::pair<expr*, expr*>, std::map<int, expr*> > varForBreakConcat;
// obj_pair_map<expr, expr, std::map<int, expr*> > varForBreakConcat;
std::map<std::pair<expr*,expr*>, std::map<int, expr*> > varForBreakConcat;
bool avoidLoopCut;
bool loopDetected;
obj_map<expr, std::stack<T_cut*> > cut_var_map;
@ -376,7 +360,7 @@ protected:
obj_hashtable<expr> variable_set;
obj_hashtable<expr> internal_variable_set;
obj_hashtable<expr> regex_variable_set;
std::map<int, std::set<expr*> > internal_variable_scope_levels;
std::map<int, obj_hashtable<expr> > internal_variable_scope_levels;
obj_hashtable<expr> internal_lenTest_vars;
obj_hashtable<expr> internal_valTest_vars;
@ -385,28 +369,30 @@ protected:
obj_hashtable<expr> input_var_in_len;
obj_map<expr, unsigned int> fvar_len_count_map;
std::map<expr*, ptr_vector<expr> > fvar_lenTester_map;
obj_map<expr, ptr_vector<expr> > fvar_lenTester_map;
obj_map<expr, expr*> lenTester_fvar_map;
std::map<expr*, std::map<int, svector<std::pair<int, expr*> > > > fvar_valueTester_map;
std::map<expr*, expr*> valueTester_fvar_map;
std::map<expr*, int_vector> val_range_map;
obj_map<expr, std::map<int, svector<std::pair<int, expr*> > > > fvar_valueTester_map;
obj_map<expr, expr*> valueTester_fvar_map;
obj_map<expr, int_vector> val_range_map;
// This can't be an expr_ref_vector because the constructor is wrong,
// we would need to modify the allocator so we pass in ast_manager
std::map<expr*, std::map<std::set<expr*>, ptr_vector<expr> > > unroll_tries_map;
std::map<expr*, expr*> unroll_var_map;
std::map<std::pair<expr*, expr*>, expr*> concat_eq_unroll_ast_map;
obj_map<expr, std::map<std::set<expr*>, ptr_vector<expr> > > unroll_tries_map;
obj_map<expr, expr*> unroll_var_map;
obj_pair_map<expr, expr, expr*> concat_eq_unroll_ast_map;
expr_ref_vector contains_map;
theory_str_contain_pair_bool_map_t contain_pair_bool_map;
//obj_map<expr, obj_pair_set<expr, expr> > contain_pair_idx_map;
std::map<expr*, std::set<std::pair<expr*, expr*> > > contain_pair_idx_map;
obj_map<expr, std::set<std::pair<expr*, expr*> > > contain_pair_idx_map;
// TBD: do a curried map for determinism.
std::map<std::pair<expr*, zstring>, expr*> regex_in_bool_map;
std::map<expr*, std::set<zstring> > regex_in_var_reg_str_map;
obj_map<expr, std::set<zstring> > regex_in_var_reg_str_map;
// regex automata
ptr_vector<eautomaton> regex_automata;
@ -608,10 +594,11 @@ protected:
std::map<expr*, expr*> & concatAliasMap, std::map<expr*, expr *> & varConstMap,
std::map<expr*, expr*> & concatConstMap, std::map<expr*, std::map<expr*, int> > & varEqConcatMap);
expr * dealias_node(expr * node, std::map<expr*, expr*> & varAliasMap, std::map<expr*, expr*> & concatAliasMap);
void get_grounded_concats(expr* node, std::map<expr*, expr*> & varAliasMap,
std::map<expr*, expr*> & concatAliasMap, std::map<expr*, expr*> & varConstMap,
std::map<expr*, expr*> & concatConstMap, std::map<expr*, std::map<expr*, int> > & varEqConcatMap,
std::map<expr*, std::map<std::vector<expr*>, std::set<expr*> > > & groundedMap);
void get_grounded_concats(unsigned depth,
expr* node, std::map<expr*, expr*> & varAliasMap,
std::map<expr*, expr*> & concatAliasMap, std::map<expr*, expr*> & varConstMap,
std::map<expr*, expr*> & concatConstMap, std::map<expr*, std::map<expr*, int> > & varEqConcatMap,
std::map<expr*, std::map<std::vector<expr*>, std::set<expr*> > > & groundedMap);
void print_grounded_concat(expr * node, std::map<expr*, std::map<std::vector<expr*>, std::set<expr*> > > & groundedMap);
void check_subsequence(expr* str, expr* strDeAlias, expr* subStr, expr* subStrDeAlias, expr* boolVar,
std::map<expr*, std::map<std::vector<expr*>, std::set<expr*> > > & groundedMap);