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

enable patterns on equality, add trace for variables for axiom profiling.

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-04-20 11:44:30 +03:00
parent b79440a21d
commit f22abaa713
2 changed files with 7 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/ast/ast.cpp
View file

@ -2254,7 +2254,12 @@ var * ast_manager::mk_var(unsigned idx, sort * s) {
unsigned sz = var::get_obj_size();
void * mem = allocate_node(sz);
var * new_node = new (mem) var(idx, s);
return register_node(new_node);
var * r = register_node(new_node);
if (m_trace_stream && r == new_node) {
*m_trace_stream << "[mk-var] #" << r->get_id() << "\n";
}
return r;
}
app * ast_manager::mk_label(bool pos, unsigned num_names, symbol const * names, expr * n) {

2
src/parsers/util/pattern_validation.cpp
View file

@ -48,7 +48,7 @@ struct pattern_validation_functor {
bool is_forbidden(func_decl const * decl) {
family_id fid = decl->get_family_id();
if (fid == m_bfid && decl->get_decl_kind() != OP_TRUE && decl->get_decl_kind() != OP_FALSE)
if (fid == m_bfid && decl->get_decl_kind() != OP_EQ && decl->get_decl_kind() != OP_TRUE && decl->get_decl_kind() != OP_FALSE)
return true;
if (fid == m_lfid)
return true;