From de367df3e7aeac2d6c4f5d80bebef6cdc6e29021 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Wed, 25 Sep 2013 13:23:23 -0500 Subject: [PATCH] fix the infinite issue --- src/theory/arith/theory_arith_private.cpp | 32 +++-------------------- src/theory/strings/theory_strings.cpp | 8 +++--- 2 files changed, 7 insertions(+), 33 deletions(-) diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 63eb301b6..9d13dccb7 100644 --- 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 1f0eee2e2..df55bcf83 100644 --- 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]; -- 2.30.2