From 69a3e984aa12aaaaa7a1318aad7913dbb035313d Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Tue, 20 Jun 2017 20:09:33 -0400 Subject: [PATCH 1/6] add is_hypothesis() method --- src/ast/ast.h | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/ast/ast.h b/src/ast/ast.h index 6bb3b01c9..475e58ac7 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -2082,6 +2082,7 @@ public: bool is_undef_proof(expr const * e) const { return e == m_undef_proof; } bool is_asserted(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_ASSERTED); } + bool is_hypothesis (expr const *e) const {return is_app_of (e, m_basic_family_id, PR_HYPOTHESIS);} bool is_goal(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_GOAL); } bool is_modus_ponens(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_MODUS_PONENS); } bool is_reflexivity(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_REFLEXIVITY); } @@ -2112,6 +2113,7 @@ public: bool is_skolemize(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_SKOLEMIZE); } MATCH_UNARY(is_asserted); + MATCH_UNARY(is_hypothesis); MATCH_UNARY(is_lemma); bool has_fact(proof const * p) const { From e9100854b9c0980b3aad2408e285b572b6448868 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Tue, 20 Jun 2017 20:09:57 -0400 Subject: [PATCH 2/6] ensure that variable names are properly quoted --- src/ast/ast_smt2_pp.cpp | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp index 89af8bd3e..d5e46548a 100644 --- a/src/ast/ast_smt2_pp.cpp +++ b/src/ast/ast_smt2_pp.cpp @@ -557,7 +557,14 @@ class smt2_printer { format * f; if (v->get_idx() < m_var_names.size()) { symbol s = m_var_names[m_var_names.size() - v->get_idx() - 1]; - f = mk_string(m(), s.str().c_str()); + std::string vname; + if (is_smt2_quoted_symbol (s)) { + vname = mk_smt2_quoted_symbol (s); + } + else { + vname = s.str(); + } + f = mk_string(m(), vname.c_str ()); } else { // fallback... it is not supposed to happen when the printer is correctly used. @@ -884,7 +891,14 @@ class smt2_printer { symbol * it = m_var_names.end() - num_decls; for (unsigned i = 0; i < num_decls; i++, it++) { format * fs[1] = { m_env.pp_sort(q->get_decl_sort(i)) }; - buf.push_back(mk_seq1(m(), fs, fs+1, f2f(), it->str().c_str())); + std::string var_name; + if (is_smt2_quoted_symbol (*it)) { + var_name = mk_smt2_quoted_symbol (*it); + } + else { + var_name = it->str ();\ + } + buf.push_back(mk_seq1(m(), fs, fs+1, f2f(), var_name.c_str ())); } return mk_seq5(m(), buf.begin(), buf.end(), f2f()); } From 6eced8836d86d39bf1d26dc5137f13f5fa0de19e Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Tue, 20 Jun 2017 20:10:22 -0400 Subject: [PATCH 3/6] expose iterators in expr_map --- src/ast/expr_map.h | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/ast/expr_map.h b/src/ast/expr_map.h index ddd94ea13..2b49a4a30 100644 --- a/src/ast/expr_map.h +++ b/src/ast/expr_map.h @@ -35,6 +35,13 @@ class expr_map { obj_map m_expr2expr; obj_map m_expr2pr; public: + typedef obj_map Map; + typedef Map::iterator iterator; + typedef Map::key key; + typedef Map::value value; + typedef Map::data data; + typedef Map::entry entry; + expr_map(ast_manager & m); expr_map(ast_manager & m, bool store_proofs); ~expr_map(); @@ -44,6 +51,8 @@ public: void erase(expr * k); void reset(); void flush(); + iterator begin () const { return m_expr2expr.begin (); } + iterator end () const {return m_expr2expr.end (); } void set_store_proofs(bool f) { if (m_store_proofs != f) flush(); m_store_proofs = f; From f3019a3de964a9e7af6f3bcc9224220647be0d08 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Tue, 20 Jun 2017 20:52:06 -0400 Subject: [PATCH 4/6] api to accumulate stopwatches --- src/util/stopwatch.h | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/util/stopwatch.h b/src/util/stopwatch.h index b1f6bba03..7a9066030 100644 --- a/src/util/stopwatch.h +++ b/src/util/stopwatch.h @@ -43,6 +43,8 @@ public: } ~stopwatch() {}; + + void add (const stopwatch &s) {/* TODO */} void reset() { m_elapsed.QuadPart = 0; } @@ -90,6 +92,8 @@ public: ~stopwatch() {} + void add (const stopwatch &s) {m_time += s.m_time;} + void reset() { m_time = 0ull; } @@ -141,6 +145,8 @@ public: ~stopwatch() {} + void add (const stopwatch &s) {m_time += s.m_time;} + void reset() { m_time = 0ull; } From 372e8b3c4910954d4df1e466a2000aca7a9b3df0 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Tue, 20 Jun 2017 20:53:04 -0400 Subject: [PATCH 5/6] expose iterator api of obj_hashtable --- src/util/obj_hashtable.h | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/util/obj_hashtable.h b/src/util/obj_hashtable.h index 383ecaeb3..2720f1b00 100644 --- a/src/util/obj_hashtable.h +++ b/src/util/obj_hashtable.h @@ -70,6 +70,7 @@ public: m_value(v) { } Value const & get_value() const { return m_value; } + Key & get_key () const { return *m_key; } unsigned hash() const { return m_key->hash(); } bool operator==(key_data const & other) const { return m_key == other.m_key; } }; @@ -100,6 +101,8 @@ public: m_table(DEFAULT_HASHTABLE_INITIAL_CAPACITY) {} typedef typename table::iterator iterator; + typedef typename table::data data; + typedef typename table::entry entry; typedef Key key; typedef Value value; From 625874e66fde340fe9ba1399df43b3788026828e Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Tue, 20 Jun 2017 20:54:43 -0400 Subject: [PATCH 6/6] remove debug code --- src/tactic/core/blast_term_ite_tactic.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/tactic/core/blast_term_ite_tactic.cpp b/src/tactic/core/blast_term_ite_tactic.cpp index ea59641c9..483b59776 100644 --- a/src/tactic/core/blast_term_ite_tactic.cpp +++ b/src/tactic/core/blast_term_ite_tactic.cpp @@ -62,14 +62,14 @@ class blast_term_ite_tactic : public tactic { for (unsigned i = 0; i < num_args; ++i) { expr* c, *t, *e; if (!m.is_bool(args[i]) && m.is_ite(args[i], c, t, e)) { - enable_trace("blast_term_ite"); + // enable_trace("blast_term_ite"); TRACE("blast_term_ite", result = m.mk_app(f, num_args, args); tout << result << "\n";); expr_ref e1(m), e2(m); ptr_vector args1(num_args, args); args1[i] = t; ++m_num_fresh; e1 = m.mk_app(f, num_args, args1.c_ptr()); - if (t == e) { + if (m.are_equal(t,e)) { result = e1; return BR_REWRITE1; }