From 3852b3a75397675a84c0103a9e88746465c26f3a Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 26 Oct 2013 15:03:39 +0800
Subject: [PATCH] working on internalizer

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_diff_logic.h     |  1 +
 src/smt/theory_diff_logic_def.h | 53 ++++++++++++++++++---------------
 2 files changed, 30 insertions(+), 24 deletions(-)

diff --git a/src/smt/theory_diff_logic.h b/src/smt/theory_diff_logic.h
index 9447b0d3e..ab47b9423 100644
--- a/src/smt/theory_diff_logic.h
+++ b/src/smt/theory_diff_logic.h
@@ -310,6 +310,7 @@ namespace smt {
 
         typedef vector <std::pair<theory_var, rational> > objective_term;
         vector<objective_term> m_objectives;
+        vector<rational>       m_objective_vars;
 
         void internalize_objective(app * n, objective_term & objective);
 
diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h
index 684850d77..f392ac423 100644
--- a/src/smt/theory_diff_logic_def.h
+++ b/src/smt/theory_diff_logic_def.h
@@ -55,6 +55,8 @@ std::ostream& theory_diff_logic<Ext>::atom::display(theory_diff_logic const& th,
 template<typename Ext>
 void theory_diff_logic<Ext>::nc_functor::reset() {
     m_antecedents.reset();
+    m_objectives.reset();
+    m_objective_vars.reset();
 }
 
 
@@ -999,11 +1001,11 @@ void theory_diff_logic<Ext>::get_implied_bound_antecedents(edge_id bridge_edge,
 template<typename Ext>
 bool theory_diff_logic<Ext>::maximize(theory_var v) {
     IF_VERBOSE(1,
-                objective_term objective = m_objectives[v];
-                for (unsigned i = 0; i < objective.size(); ++i) {
-	                verbose_stream() << "coefficient " << objective[i].second << " of theory_var " << objective[i].first << "\n";
-                }
-                verbose_stream() << "\n";);
+               objective_term const& objective = m_objectives[v];
+               for (unsigned i = 0; i < objective.size(); ++i) {
+                   verbose_stream() << "coefficient " << objective[i].second << " of theory_var " << objective[i].first << "\n";
+               }
+               verbose_stream() << m_objective_vars[v] << "\n";);
     NOT_IMPLEMENTED_YET();
     return false;
 }
@@ -1011,39 +1013,38 @@ bool theory_diff_logic<Ext>::maximize(theory_var v) {
 template<typename Ext>
 theory_var theory_diff_logic<Ext>::add_objective(app* term) {
     objective_term objective;
-    internalize_objective(term, objective);
-    m_objectives.push_back(objective);
-    return m_objectives.size()-1; 
+    theory_var result = m_objectives.size();
+    rational q(1), r(0);
+    if (!internalize_objective(term, q, r, objective)) {
+        result = null_theory_var;
+    }
+    else {
+        m_objectives.push_back(objective);
+        m_objective_vars.push_back(r);
+    }
+    return result; 
 }
 
 template<typename Ext>
 inf_eps_rational<inf_rational> theory_diff_logic<Ext>::get_objective_value(theory_var v) { 
-	inf_rational objective;
+    inf_rational objective;
     inf_eps_rational<inf_rational> val(objective);     
     return val; 
 }
 
 template<typename Ext>
-void theory_diff_logic<Ext>::internalize_objective(app * n, objective_term & objective) {
-    // TODO: Need some simplification on n to ensure no bad case 
-    SASSERT(!m_util.is_div(n));
-    SASSERT(!m_util.is_idiv(n));
-    SASSERT(!m_util.is_mod(n));
-    SASSERT(!m_util.is_rem(n));
-    SASSERT(!m_util.is_to_real(n));
-    SASSERT(!m_util.is_to_int(n));
-    SASSERT(!m_util.is_power(n));
-    SASSERT(!m_util.is_irrational_algebraic_numeral(n));
+bool theory_diff_logic<Ext>::internalize_objective(app * n, rational& q, objective_term & objective) {
 
     // Compile term into objective_term format
     rational r;
     if (m_util.is_numeral(n, r)) {
-        theory_var v = mk_num(n, r);
-        objective.push_back(std::make_pair(v, r));
+        q += r;
     }
     else if (m_util.is_add(n)) {
         for (unsigned i = 0; i < n->get_num_args(); ++i) {
-            internalize_objective(to_app(n->get_arg(i)), objective);
+            if (!internalize_objective(to_app(n->get_arg(i)), objective)) {
+                return false;
+            }
         };
     }
     else if (m_util.is_mul(n)) {
@@ -1054,17 +1055,21 @@ void theory_diff_logic<Ext>::internalize_objective(app * n, objective_term & obj
         SASSERT(m_util.is_numeral(lhs, r) || m_util.is_numeral(rhs, r));
 
         if (!m_util.is_numeral(lhs, r))
-	        std::swap(lhs, rhs);
-
+            std::swap(lhs, rhs);
+        
         m_util.is_numeral(lhs, r);
         theory_var v = mk_var(rhs);
         objective.push_back(std::make_pair(v, r));
     }
+    else if (n->get_family_id() == m_util.get_family_id()) {
+        return false;
+    }
     else {
         theory_var v = mk_var(n);
         rational r(1);
         objective.push_back(std::make_pair(v, r));
     }
+    return true;
 }
 
 #endif /* _THEORY_DIFF_LOGIC_DEF_H_ */