From f22abaa7135f46953211fc304aa51e938e0d0948 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 20 Apr 2018 11:44:30 +0300 Subject: [PATCH] enable patterns on equality, add trace for variables for axiom profiling. Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 7 ++++++- src/parsers/util/pattern_validation.cpp | 2 +- 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 7e143e1a3..12ca136c5 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -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) { diff --git a/src/parsers/util/pattern_validation.cpp b/src/parsers/util/pattern_validation.cpp index 0d076aadd..df1f6cd00 100644 --- a/src/parsers/util/pattern_validation.cpp +++ b/src/parsers/util/pattern_validation.cpp @@ -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;