fix the infinite issue

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 63eb301b6bbb2b3f89c1694771237ca70a865c43..9d13dccb7b693a381de347efe1a69a98d02e2dc4 100644 (file)
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -737,8 +737,8 @@ void TheoryArithPrivate::addSharedTerm(TNode n){
   }
 }
 
-Node TheoryArithPrivate::getModelValue(TNode var) {
-  /*try{
+Node TheoryArithPrivate::getModelValue(TNode term) {
+  try{
     DeltaRational drv = getDeltaValue(term);
     const Rational& delta = d_partialModel.getDelta();
     Rational qmodel = drv.substituteDelta( delta );
@@ -747,33 +747,7 @@ Node TheoryArithPrivate::getModelValue(TNode var) {
     return Node::null();
   } catch (ModelException& me) {
     return Node::null();
-  }*/
-       //if( d_partialModel.hasNode( var ) ){
-       if( var.getKind()==kind::STRING_LENGTH ){
-               Trace("strings-temp") << "Get model value of " << var << std::endl;
-               /*
-               ArithVar v;
-               bool foundV = false;
-           ArithVariables& avnm = d_partialModel;
-           ArithVariables::var_iterator vi, vend;
-           for(vi = avnm.var_begin(), vend = avnm.var_end(); vi != vend; ++vi ){
-                       if( avnm.asNode(*vi)==var ){
-                               v = *vi;
-                               foundV = true;
-                               break;
-                       }
-               }
-               if( foundV ){
-                       */
-               ArithVar v = d_partialModel.asArithVar( var );
-               DeltaRational drv = d_partialModel.getAssignment( v );
-               const Rational& delta = d_partialModel.getDelta();
-               Rational qmodel = drv.substituteDelta( delta );
-               Trace("strings-temp") << "Value is " << drv << ", after subs : " << qmodel << std::endl;
-               return mkRationalNode( qmodel );
-       }
-       //}
-       return var;
+  }
 }
 
 namespace attr {

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 1f0eee2e20d671ba2cdf5cba91340d09ffdba849..df55bcf838fed816741f1d1052b863df11feec14 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -860,7 +860,7 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
                                                                                        //Node len_y_eq_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_y, d_emptyString);
                                                                                        //Node zz_imp_yz = NodeManager::currentNM()->mkNode( kind::IMPLIES, len_z_eq_zero, len_y_eq_zero);
                                                                                        
-                                                                                       Node z_neq_empty = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_z, d_emptyString).negate();
+                                                                                       //Node z_neq_empty = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_z, d_emptyString).negate();
                                                                                        //Node len_x_gt_len_y = NodeManager::currentNM()->mkNode( kind::GT, 
                                                                                        //                                              NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, normal_forms[other_n_index][other_index]),
                                                                                        //                                              sk_y_len );
@@ -868,9 +868,9 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v
                                                                                        //Node x_eq_y_rest = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[other_n_index][other_index], 
                                                                                        //                                              NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk_y, sk_x_rest ) );
                                                                                        
-                                                                                       conc = NodeManager::currentNM()->mkNode( kind::AND, conc1, conc2, z_neq_empty );//, x_eq_y_rest );// , z_neq_empty //, len_x_gt_len_y
-                                                                                       Node x_eq_empty = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[other_n_index][other_index], d_emptyString);
-                                                                                       conc = NodeManager::currentNM()->mkNode( kind::OR, x_eq_empty, conc );
+                                                                                       conc = NodeManager::currentNM()->mkNode( kind::AND, conc1, conc2 );//, x_eq_y_rest );// , z_neq_empty //, len_x_gt_len_y
+                                                                                       //Node x_eq_empty = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[other_n_index][other_index], d_emptyString);
+                                                                                       //conc = NodeManager::currentNM()->mkNode( kind::OR, x_eq_empty, conc );
 
                                             
                                                                                        Node loop_x = normal_forms[other_n_index][other_index];