From be77b1de394ea45e781477181ffc4e5cc70a21df Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Wed, 13 Dec 2017 16:24:33 -0500
Subject: [PATCH] Improve interface of term_graph

---
 src/muz/spacer/spacer_term_graph.cpp | 19 +++++++++++++------
 src/muz/spacer/spacer_term_graph.h   | 10 ++++++++--
 2 files changed, 21 insertions(+), 8 deletions(-)

diff --git a/src/muz/spacer/spacer_term_graph.cpp b/src/muz/spacer/spacer_term_graph.cpp
index c34022d48..61f7fb369 100644
--- a/src/muz/spacer/spacer_term_graph.cpp
+++ b/src/muz/spacer/spacer_term_graph.cpp
@@ -91,7 +91,7 @@ public:
 
     virtual ~arith_term_graph_plugin() {}
 
-    bool mk_eq_core (expr *_e1, expr *_e2, app* &res) {
+    bool mk_eq_core (expr *_e1, expr *_e2, app_ref &res) {
         expr *e1, *e2;
         e1 = _e1;
         e2 = _e2;
@@ -115,7 +115,7 @@ public:
         return true;
     }
 
-    bool mk_le_core (expr *arg1, expr * arg2, app* &result) {
+    bool mk_le_core (expr *arg1, expr * arg2, app_ref &result) {
         // t <= -1  ==> t < 0 ==> ! (t >= 0)
         if (m_arith.is_int (arg1) && m_arith.is_minus_one (arg2)) {
             result = m.mk_not (m_arith.mk_ge (arg1, mk_zero ()));
@@ -130,7 +130,7 @@ public:
         return m_arith.is_numeral (n, val) && val.is_one ();
     }
 
-    bool mk_ge_core (expr * arg1, expr * arg2, app* &result) {
+    bool mk_ge_core (expr * arg1, expr * arg2, app_ref &result) {
         // t >= 1 ==> t > 0 ==> ! (t <= 0)
         if (m_arith.is_int (arg1) && is_one (arg2)) {
             result = m.mk_not (m_arith.mk_le (arg1, mk_zero ()));
@@ -139,11 +139,12 @@ public:
         return false;
     }
 
-    virtual app* process_lit (app *lit) {
+    virtual app_ref process_lit (app *lit) {
         expr *e1, *e2;
 
 
-   app *res = lit;
+        app_ref res(m);
+        res = lit;
         if (m.is_eq (lit, e1, e2)) {
             mk_eq_core(e1, e2, res);
         }
@@ -429,7 +430,13 @@ void term_graph::to_lits (app_ref_vector &lits, bool all_equalities) {
             mk_equalities(*t, lits);
         }
     }
-
+}
+void term_graph::to_lits (expr_ref_vector &lits, bool all_equalities) {
+    app_ref_vector out(m);
+    to_lits (out, all_equalities);
+    for (unsigned i = 0, sz = out.size(); i < sz; ++i) {
+        lits.push_back(out.get(i));
+    }
 }
 
 app_ref term_graph::to_app() {
diff --git a/src/muz/spacer/spacer_term_graph.h b/src/muz/spacer/spacer_term_graph.h
index 6e5ea9a6a..b547adef3 100644
--- a/src/muz/spacer/spacer_term_graph.h
+++ b/src/muz/spacer/spacer_term_graph.h
@@ -36,7 +36,7 @@ public:
     family_id get_family_id() const {return m_id;}
 
     /// Process (and potentially augment) a literal
-    virtual app* process_lit (app *lit) {return lit;}
+    virtual app_ref process_lit (app *lit) = 0;
 };
 
 class term_graph {
@@ -80,9 +80,15 @@ public:
     ast_manager &get_ast_manager() const {return m;}
 
     void add_lit(app *lit);
+    void add_lits(expr_ref_vector const &lits) {
+        for (unsigned i = 0, sz = lits.size(); i < sz; ++i) {
+            add_lit(::to_app(lits.get(i)));
+        }
+    }
 
     void reset();
-    void to_lits (app_ref_vector &lits, bool all_equalities = false);
+    void to_lits(app_ref_vector &lits, bool all_equalities = false);
+    void to_lits(expr_ref_vector &lits, bool all_equalities = false);
     app_ref to_app();
 
 };