simplify some verbose trace-stream

Z3Prover · Jul 11, 2021 · 5fac396 · 5fac396
1 parent bc2e6ce
commit 5fac396
Show file tree

Hide file tree

Showing 3 changed files with 27 additions and 18 deletions.
diff --git a/src/smt/smt_theory.cpp b/src/smt/smt_theory.cpp
@@ -195,6 +195,18 @@ namespace smt {
         log_axiom_instantiation(mk_or(fmls));
     }
 
+
+    void theory::log_axiom_instantiation(literal_buffer const& ls) {
+        ast_manager& m = get_manager();
+        expr_ref_vector fmls(m);
+        expr_ref tmp(m);
+        for (literal l : ls) {
+            ctx.literal2expr(l, tmp);
+            fmls.push_back(tmp);
+        }
+        log_axiom_instantiation(mk_or(fmls));
+    }
+
     void theory::log_axiom_instantiation(app * r, unsigned axiom_id, unsigned num_bindings, app * const * bindings, unsigned pattern_id, const vector<std::tuple<enode *, enode *>> & used_enodes) {
         ast_manager & m = get_manager();
         app_ref _r(r, m);

diff --git a/src/smt/smt_theory.h b/src/smt/smt_theory.h
@@ -124,6 +124,12 @@ namespace smt {
                 }
             }
 
+            scoped_trace_stream(theory& th, literal_buffer const& lits) : m(th.get_manager()) {
+                if (m.has_trace_stream()) {
+                    th.log_axiom_instantiation(lits);
+                }
+            }
+
             scoped_trace_stream(theory& th, literal lit): m(th.get_manager()) {
                 if (m.has_trace_stream()) {
                     literal_vector lits;
@@ -464,6 +470,8 @@ namespace smt {
 
         void log_axiom_instantiation(literal_vector const& ls);
 
+        void log_axiom_instantiation(literal_buffer const& ls);
+
         void log_axiom_instantiation(app * r, unsigned num_blamed_enodes, enode ** blamed_enodes) {
             vector<std::tuple<enode *, enode *>> used_enodes;
             for (unsigned i = 0; i < num_blamed_enodes; ++i) {

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
@@ -1321,13 +1321,8 @@ class theory_lra::imp {
                 exprs.push_back(c.bool_var2expr(mod_j.var()));
                 ctx().mark_as_relevant(mod_j);
             }
-            if (m.has_trace_stream()) {
-                app_ref body(m);
-                body = m.mk_or(exprs.size(), exprs.data());
-                th.log_axiom_instantiation(body);
-            }
+            scoped_trace_stream _st(th, lits);
             ctx().mk_th_axiom(get_id(), lits.size(), lits.begin());                
-            if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
         }            
     }
 
@@ -1750,20 +1745,14 @@ class theory_lra::imp {
                 literal p_ge_r1  = mk_literal(a.mk_ge(p, a.mk_numeral(lo, true)));
                 literal n_le_div = mk_literal(a.mk_le(n, a.mk_numeral(div_r, true)));
                 literal n_ge_div = mk_literal(a.mk_ge(n, a.mk_numeral(div_r, true)));
-                if (m.has_trace_stream()) {
-                    app_ref body(m);
-                    body = m.mk_implies(ctx().bool_var2expr(p_le_r1.var()), ctx().bool_var2expr(n_le_div.var()));
-                    th.log_axiom_instantiation(body);
+                {
+                    scoped_trace_stream _sts(th, ~p_le_r1, n_le_div);
+                    mk_axiom(~p_le_r1, n_le_div);
                 }
-                mk_axiom(~p_le_r1, n_le_div); 
-                if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
-                if (m.has_trace_stream()) {
-                    app_ref body(m);
-                    body = m.mk_implies(ctx().bool_var2expr(p_ge_r1.var()), ctx().bool_var2expr(n_ge_div.var()));
-                    th.log_axiom_instantiation(body);
+                {
+                    scoped_trace_stream _sts(th, ~p_ge_r1, n_ge_div);
+                    mk_axiom(~p_ge_r1, n_ge_div);
                 }
-                mk_axiom(~p_ge_r1, n_ge_div);
-                if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
 
                 all_divs_valid = false;