From 892be69d5142e4c889ad60f3dfa36e8166f6f245 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 25 Mar 2019 10:40:08 -0700
Subject: [PATCH] nits

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_special_relations.cpp | 15 ++++-----------
 src/smt/theory_special_relations.h   | 10 +++++-----
 2 files changed, 9 insertions(+), 16 deletions(-)

diff --git a/src/smt/theory_special_relations.cpp b/src/smt/theory_special_relations.cpp
index 95cfb410e..03066f766 100644
--- a/src/smt/theory_special_relations.cpp
+++ b/src/smt/theory_special_relations.cpp
@@ -115,15 +115,11 @@ namespace smt {
 
     void theory_special_relations::new_eq_eh(theory_var v1, theory_var v2) {
         context& ctx = get_context();
-        app_ref eq(get_manager());
         app* t1 = get_enode(v1)->get_owner();
         app* t2 = get_enode(v2)->get_owner();
-        eq = get_manager().mk_eq(t1, t2);
-        VERIFY(internalize_atom(eq, false));
-        literal l(ctx.get_literal(eq));
-        obj_map<func_decl, relation*>::iterator it = m_relations.begin(), end = m_relations.end();
-        for (; !ctx.inconsistent() && it != end; ++it) {
-            relation& r = *it->m_value;
+        literal eq = mk_eq(t1, t2, false);
+        for (auto const& kv : m_relations) {
+            relation& r = *kv.m_value;
             if (!r.new_eq_eh(l, v1, v2)) {
                 set_neg_cycle_conflict(r);
                 break;
@@ -175,9 +171,8 @@ namespace smt {
 
     literal theory_special_relations::mk_literal(expr* _e) {
         expr_ref e(_e, get_manager());
-        context& ctx = get_context();
         ensure_enode(e);
-        return ctx.get_literal(e);
+        return get_context().get_literal(e);
     }
 
     theory_var theory_special_relations::mk_var(enode* n) {
@@ -520,7 +515,6 @@ namespace smt {
     }
 
     expr_ref theory_special_relations::mk_inj(relation& r, model_generator& mg) {
-      // context& ctx = get_context();
         ast_manager& m = get_manager();
         r.push();
         ensure_strict(r.m_graph);
@@ -545,7 +539,6 @@ namespace smt {
     }
 
     expr_ref theory_special_relations::mk_class(relation& r, model_generator& mg) {
-      //context& ctx = get_context();
         ast_manager& m = get_manager();
         expr_ref result(m);
         func_decl_ref fn(m);
diff --git a/src/smt/theory_special_relations.h b/src/smt/theory_special_relations.h
index 7c243dee0..01314b362 100644
--- a/src/smt/theory_special_relations.h
+++ b/src/smt/theory_special_relations.h
@@ -17,14 +17,14 @@ Notes:
 
 --*/
 
+#ifndef THEORY_SPECIAL_RELATIONS_H_
+#define THEORY_SPECIAL_RELATIONS_H_
+
 #include "ast/special_relations_decl_plugin.h"
 #include "smt/smt_theory.h"
 #include "smt/theory_diff_logic.h"
 #include "util/union_find.h"
-#include "solver/solver.h"
-
-#ifndef THEORY_SPECIAL_RELATIONS_H_
-#define THEORY_SPECIAL_RELATIONS_H_
+#include "util/rational.h"
 
 namespace smt {
     class theory_special_relations : public theory {
@@ -140,7 +140,7 @@ namespace smt {
         void set_neg_cycle_conflict(relation& r);
         void set_conflict(relation& r);
         lbool  propagate_plo(atom& a);
-        lbool  propagate_po(atom& a); //ASHU: added to modify po solving
+        lbool  propagate_po(atom& a); 
         theory_var mk_var(expr* e);
         void count_children(graph const& g, unsigned_vector& num_children);
         void ensure_strict(graph& g);