mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
Merge branch 'master' of https://github.com/z3prover/z3
This commit is contained in:
commit
ad973d5c6d
|
@ -1932,8 +1932,14 @@ class MLComponent(Component):
|
|||
OCAML_FLAGS = ''
|
||||
if DEBUG_MODE:
|
||||
OCAML_FLAGS += '-g'
|
||||
OCAMLCF = OCAMLC + ' ' + OCAML_FLAGS
|
||||
OCAMLOPTF = OCAMLOPT + ' ' + OCAML_FLAGS
|
||||
|
||||
if OCAMLFIND:
|
||||
# Load Big_int, which is no longer part of the standard library, via the num package: https://github.com/ocaml/num
|
||||
OCAMLCF = OCAMLFIND + ' ' + 'ocamlc -package num' + ' ' + OCAML_FLAGS
|
||||
OCAMLOPTF = OCAMLFIND + ' ' + 'ocamlopt -package num' + ' ' + OCAML_FLAGS
|
||||
else:
|
||||
OCAMLCF = OCAMLC + ' ' + OCAML_FLAGS
|
||||
OCAMLOPTF = OCAMLOPT + ' ' + OCAML_FLAGS
|
||||
|
||||
src_dir = self.to_src_dir
|
||||
mk_dir(os.path.join(BUILD_DIR, self.sub_dir))
|
||||
|
|
|
@ -912,7 +912,7 @@ class smt2_printer {
|
|||
var_name = mk_smt2_quoted_symbol (*it);
|
||||
}
|
||||
else {
|
||||
var_name = it->str ();\
|
||||
var_name = it->str ();
|
||||
}
|
||||
buf.push_back(mk_seq1<format**,f2f>(m(), fs, fs+1, f2f(), var_name.c_str ()));
|
||||
}
|
||||
|
|
|
@ -108,7 +108,9 @@ public:
|
|||
#endif
|
||||
}
|
||||
~line_reader() {
|
||||
fclose(m_file);
|
||||
if (m_file != nullptr){
|
||||
fclose(m_file);
|
||||
}
|
||||
}
|
||||
|
||||
bool operator()() { return m_ok; }
|
||||
|
|
|
@ -627,10 +627,7 @@ namespace smt {
|
|||
*/
|
||||
void context::remove_parents_from_cg_table(enode * r1) {
|
||||
// Remove parents from the congruence table
|
||||
enode_vector::iterator it = r1->begin_parents();
|
||||
enode_vector::iterator end = r1->end_parents();
|
||||
for (; it != end; ++it) {
|
||||
enode * parent = *it;
|
||||
for (enode * parent : r1->get_parents()) {
|
||||
#if 0
|
||||
{
|
||||
static unsigned num_eqs = 0;
|
||||
|
@ -675,10 +672,7 @@ namespace smt {
|
|||
*/
|
||||
void context::reinsert_parents_into_cg_table(enode * r1, enode * r2, enode * n1, enode * n2, eq_justification js) {
|
||||
enode_vector & r2_parents = r2->m_parents;
|
||||
enode_vector::iterator it = r1->begin_parents();
|
||||
enode_vector::iterator end = r1->end_parents();
|
||||
for (; it != end; ++it) {
|
||||
enode * parent = *it;
|
||||
for (enode * parent : r1->get_parents()) {
|
||||
if (!parent->is_marked())
|
||||
continue;
|
||||
parent->unset_mark();
|
||||
|
@ -1008,10 +1002,7 @@ namespace smt {
|
|||
r2->m_parents.shrink(r2_num_parents);
|
||||
|
||||
// try to reinsert parents of r1 that are not cgr
|
||||
it = r1->begin_parents();
|
||||
end = r1->end_parents();
|
||||
for (; it != end; ++it) {
|
||||
enode * parent = *it;
|
||||
for (enode * parent : r1->get_parents()) {
|
||||
TRACE("add_eq_parents", tout << "visiting: #" << parent->get_owner_id() << "\n";);
|
||||
if (parent->is_cgc_enabled()) {
|
||||
enode * cg = parent->m_cg;
|
||||
|
@ -1206,10 +1197,7 @@ namespace smt {
|
|||
bool context::is_diseq_slow(enode * n1, enode * n2) const {
|
||||
if (n1->get_num_parents() > n2->get_num_parents())
|
||||
std::swap(n1, n2);
|
||||
enode_vector::iterator it = n1->begin_parents();
|
||||
enode_vector::iterator end = n1->end_parents();
|
||||
for (; it != end; ++it) {
|
||||
enode * parent = *it;
|
||||
for (enode * parent : n1->get_parents()) {
|
||||
if (parent->is_eq() && is_relevant(parent->get_owner()) && get_assignment(enode2bool_var(parent)) == l_false &&
|
||||
((parent->get_arg(0)->get_root() == n1->get_root() && parent->get_arg(1)->get_root() == n2->get_root()) ||
|
||||
(parent->get_arg(1)->get_root() == n1->get_root() && parent->get_arg(0)->get_root() == n2->get_root()))) {
|
||||
|
@ -1241,10 +1229,7 @@ namespace smt {
|
|||
return false;
|
||||
if (r1->get_num_parents() < SMALL_NUM_PARENTS) {
|
||||
TRACE("is_ext_diseq", tout << mk_bounded_pp(n1->get_owner(), m_manager) << " " << mk_bounded_pp(n2->get_owner(), m_manager) << " " << depth << "\n";);
|
||||
enode_vector::iterator it1 = r1->begin_parents();
|
||||
enode_vector::iterator end1 = r1->end_parents();
|
||||
for (; it1 != end1; ++it1) {
|
||||
enode * p1 = *it1;
|
||||
for (enode* p1 : r1->get_parents()) {
|
||||
if (!is_relevant(p1))
|
||||
continue;
|
||||
if (p1->is_eq())
|
||||
|
@ -1254,10 +1239,7 @@ namespace smt {
|
|||
func_decl * f = p1->get_decl();
|
||||
TRACE("is_ext_diseq", tout << "p1: " << mk_bounded_pp(p1->get_owner(), m_manager) << "\n";);
|
||||
unsigned num_args = p1->get_num_args();
|
||||
enode_vector::iterator it2 = r2->begin_parents();
|
||||
enode_vector::iterator end2 = r2->end_parents();
|
||||
for (; it2 != end2; ++it2) {
|
||||
enode * p2 = *it2;
|
||||
for (enode * p2 : r2->get_parents()) {
|
||||
if (!is_relevant(p2))
|
||||
continue;
|
||||
if (p2->is_eq())
|
||||
|
@ -1295,10 +1277,7 @@ namespace smt {
|
|||
}
|
||||
almost_cg_table & table = *(m_almost_cg_tables[depth]);
|
||||
table.reset(r1, r2);
|
||||
enode_vector::iterator it1 = r1->begin_parents();
|
||||
enode_vector::iterator end1 = r1->end_parents();
|
||||
for (; it1 != end1; ++it1) {
|
||||
enode * p1 = *it1;
|
||||
for (enode* p1 : r1->get_parents()) {
|
||||
if (!is_relevant(p1))
|
||||
continue;
|
||||
if (p1->is_eq())
|
||||
|
@ -1309,10 +1288,7 @@ namespace smt {
|
|||
}
|
||||
if (table.empty())
|
||||
return false;
|
||||
enode_vector::iterator it2 = r2->begin_parents();
|
||||
enode_vector::iterator end2 = r2->end_parents();
|
||||
for (; it2 != end2; ++it2) {
|
||||
enode * p2 = *it2;
|
||||
for (enode * p2 : r2->get_parents()) {
|
||||
if (!is_relevant(p2))
|
||||
continue;
|
||||
if (p2->is_eq())
|
||||
|
@ -1519,10 +1495,7 @@ namespace smt {
|
|||
}
|
||||
TRACE("push_new_th_diseqs", tout << "#" << r->get_owner_id() << " v" << v << "\n";);
|
||||
theory_id th_id = th->get_id();
|
||||
enode_vector::iterator it = r->begin_parents();
|
||||
enode_vector::iterator end = r->end_parents();
|
||||
for (; it != end; ++it) {
|
||||
enode * parent = *it;
|
||||
for (enode * parent : r->get_parents()) {
|
||||
CTRACE("parent_bug", parent == 0, tout << "#" << r->get_owner_id() << ", num_parents: " << r->get_num_parents() << "\n"; display(tout););
|
||||
if (parent->is_eq()) {
|
||||
bool_var bv = get_bool_var_of_id(parent->get_owner_id());
|
||||
|
@ -2197,9 +2170,7 @@ namespace smt {
|
|||
TRACE("cached_generation", tout << "caching: #" << n->get_id() << " " << e->get_generation() << "\n";);
|
||||
m_cached_generation.insert(n, e->get_generation());
|
||||
}
|
||||
unsigned num_args = to_app(n)->get_num_args();
|
||||
for (unsigned i = 0; i < num_args; i++) {
|
||||
expr * arg = to_app(n)->get_arg(i);
|
||||
for (expr * arg : *to_app(n)) {
|
||||
if (is_app(arg) || is_quantifier(arg))
|
||||
todo.push_back(arg);
|
||||
}
|
||||
|
@ -4228,10 +4199,7 @@ namespace smt {
|
|||
theory_var_list * l = n->get_th_var_list();
|
||||
theory_id th_id = l->get_th_id();
|
||||
|
||||
enode_vector::const_iterator it = n->begin_parents();
|
||||
enode_vector::const_iterator end = n->end_parents();
|
||||
for (; it != end; ++it) {
|
||||
enode * parent = *it;
|
||||
for (enode* parent : n->get_parents()) {
|
||||
family_id fid = parent->get_owner()->get_family_id();
|
||||
if (fid != th_id && fid != m_manager.get_basic_family_id()) {
|
||||
TRACE("is_shared", tout << mk_pp(n->get_owner(), m_manager) << "\nis shared because of:\n" << mk_pp(parent->get_owner(), m_manager) << "\n";);
|
||||
|
|
|
@ -341,10 +341,7 @@ namespace smt {
|
|||
}
|
||||
|
||||
void context::display_parent_eqs(std::ostream & out, enode * n) const {
|
||||
enode_vector::iterator it = n->begin_parents();
|
||||
enode_vector::iterator end = n->end_parents();
|
||||
for (; it != end; ++it) {
|
||||
enode * parent = *it;
|
||||
for (enode* parent : n->get_parents()) {
|
||||
if (parent->is_eq())
|
||||
display_eq_detail(out, parent);
|
||||
}
|
||||
|
|
|
@ -216,15 +216,28 @@ namespace smt {
|
|||
return m_args;
|
||||
}
|
||||
|
||||
class args {
|
||||
class const_args {
|
||||
enode const& n;
|
||||
public:
|
||||
args(enode const& n):n(n) {}
|
||||
args(enode const* n):n(*n) {}
|
||||
enode_vector::const_iterator begin() const { return n.get_args(); }
|
||||
enode_vector::const_iterator end() const { return n.get_args() + n.get_num_args(); }
|
||||
const_args(enode const& n):n(n) {}
|
||||
const_args(enode const* n):n(*n) {}
|
||||
enode_vector::const_iterator begin() const { return n.m_args; }
|
||||
enode_vector::const_iterator end() const { return n.m_args + n.get_num_args(); }
|
||||
};
|
||||
|
||||
class args {
|
||||
enode & n;
|
||||
public:
|
||||
args(enode & n):n(n) {}
|
||||
args(enode * n):n(*n) {}
|
||||
enode_vector::iterator begin() const { return n.m_args; }
|
||||
enode_vector::iterator end() const { return n.m_args + n.get_num_args(); }
|
||||
};
|
||||
|
||||
const_args get_const_args() const { return const_args(this); }
|
||||
|
||||
// args get_args() { return args(this); }
|
||||
|
||||
// unsigned get_id() const {
|
||||
// return m_id;
|
||||
// }
|
||||
|
@ -294,15 +307,27 @@ namespace smt {
|
|||
return m_commutative;
|
||||
}
|
||||
|
||||
class parents {
|
||||
class const_parents {
|
||||
enode const& n;
|
||||
public:
|
||||
parents(enode const& _n):n(_n) {}
|
||||
parents(enode const* _n):n(*_n) {}
|
||||
const_parents(enode const& _n):n(_n) {}
|
||||
const_parents(enode const* _n):n(*_n) {}
|
||||
enode_vector::const_iterator begin() const { return n.begin_parents(); }
|
||||
enode_vector::const_iterator end() const { return n.end_parents(); }
|
||||
};
|
||||
|
||||
class parents {
|
||||
enode& n;
|
||||
public:
|
||||
parents(enode & _n):n(_n) {}
|
||||
parents(enode * _n):n(*_n) {}
|
||||
enode_vector::iterator begin() const { return n.begin_parents(); }
|
||||
enode_vector::iterator end() const { return n.end_parents(); }
|
||||
};
|
||||
|
||||
parents get_parents() { return parents(this); }
|
||||
|
||||
const_parents get_const_parents() const { return const_parents(this); }
|
||||
|
||||
unsigned get_num_parents() const {
|
||||
return m_parents.size();
|
||||
|
|
|
@ -34,6 +34,16 @@ bool is_smt2_quoted_symbol(char const * s) {
|
|||
if ('0' <= s[0] && s[0] <= '9')
|
||||
return true;
|
||||
unsigned len = static_cast<unsigned>(strlen(s));
|
||||
if (len >= 2 && s[0] == '|' && s[len-1] == '|') {
|
||||
for (unsigned i = 1; i + 1 < len; i++) {
|
||||
if (s[i] == '\\' && i + 2 < len && (s[i+1] == '\\' || s[i+1] == '|')) {
|
||||
i++;
|
||||
}
|
||||
else if (s[i] == '\\' || s[i] == '|')
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
for (unsigned i = 0; i < len; i++)
|
||||
if (!is_smt2_simple_symbol_char(s[i]))
|
||||
return true;
|
||||
|
|
Loading…
Reference in a new issue