Merge pull request #1089 from agurfinkel/fixes

Fixes

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 {

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<format**,f2f>(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<format**,f2f>(m(), fs, fs+1, f2f(), var_name.c_str ()));
         }
         return mk_seq5(m(), buf.begin(), buf.end(), f2f());
     }

src/ast/expr_map.h

@@ -35,6 +35,13 @@ class expr_map {
     obj_map<expr, expr*>  m_expr2expr;
     obj_map<expr, proof*> m_expr2pr;
 public:
+    typedef obj_map<expr, expr*> 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; 

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<expr> 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;
                     }

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;
 

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;
     }