From 5c6ba045a0306e16d8867d96b145d8892e3feefc Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Wed, 25 Sep 2013 13:00:13 -0500 Subject: [PATCH] for morgan to see the regression problems --- src/parser/smt2/Smt2.g | 5 +++ src/theory/arith/theory_arith_private.cpp | 10 ++++++ src/theory/strings/theory_strings.cpp | 38 ++++++++++++++++------- 3 files changed, 42 insertions(+), 11 deletions(-) diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 638c64a69..8af543039 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -870,6 +870,10 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] expr = MK_EXPR(kind, args); } } + //| /* substring */ + //LPAREN_TOK STRSUB_TOK n1=INTEGER_LITERAL n2=INTEGER_LITERAL RPAREN_TOK + //{ + //} | /* A non-built-in function application */ LPAREN_TOK functionName[name, CHECK_DECLARED] @@ -1620,6 +1624,7 @@ STRCON_TOK : 'str.++'; STRLEN_TOK : 'str.len'; STRINRE_TOK : 'str.in.re'; STRTORE_TOK : 'str.to.re'; +//STRSUB_TOK : 'str.sub' ; RECON_TOK : 're.++'; REOR_TOK : 're.or'; REINTER_TOK : 're.inter'; diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 7e5c01291..63eb301b6 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -738,6 +738,16 @@ void TheoryArithPrivate::addSharedTerm(TNode n){ } Node TheoryArithPrivate::getModelValue(TNode var) { + /*try{ + DeltaRational drv = getDeltaValue(term); + const Rational& delta = d_partialModel.getDelta(); + Rational qmodel = drv.substituteDelta( delta ); + return mkRationalNode( qmodel ); + } catch (DeltaRationalException& dr) { + 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; diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index b88ca3dac..1f0eee2e2 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -55,6 +55,8 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu d_emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") ); d_true = NodeManager::currentNM()->mkConst( true ); d_false = NodeManager::currentNM()->mkConst( false ); + + //preRegisterTerm( d_emptyString ); } TheoryStrings::~TheoryStrings() { @@ -510,7 +512,9 @@ void TheoryStrings::doPendingFacts() { bool polarity = fact.getKind() != kind::NOT; TNode atom = polarity ? fact : fact[0]; if (atom.getKind() == kind::EQUAL) { - d_equalityEngine.assertEquality( atom, polarity, exp ); + Assert( d_equalityEngine.hasTerm( atom[0] ) ); + Assert( d_equalityEngine.hasTerm( atom[1] ) ); + d_equalityEngine.assertEquality( atom, polarity, exp ); }else{ d_equalityEngine.assertPredicate( atom, polarity, exp ); } @@ -679,6 +683,7 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v } Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, d_emptyString, normal_forms[k][index_k] ); Trace("strings-lemma") << "Strings : Infer " << eq << " from " << eq_exp << std::endl; + Assert( !d_equalityEngine.areEqual( d_emptyString, normal_forms[k][index_k] ) ); //d_equalityEngine.assertEquality( eq, true, eq_exp ); d_pending.push_back( eq ); d_pending_exp[eq] = eq_exp; @@ -782,7 +787,7 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v } term_s = mkConcat( sc ); Trace("strings-loop") << "Find y,z from t,s = " << term_t << ", " << term_s << std::endl; - /*TODO: incomplete start*/ + /*TODO: incomplete start */ if( term_t==term_s ){ found_size_y = -2; }else if( term_t.getKind()==kind::STRING_CONCAT && term_s.getKind()==kind::STRING_CONCAT ){ @@ -848,26 +853,37 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v Node conc2 = NodeManager::currentNM()->mkNode( kind::EQUAL, left2, mkConcat( c3c ) ); - //Node sk_y_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_y ); + Node sk_y_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_y ); //Node sk_z_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_z ); //Node len_y_eq_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_y_len, d_zero); //Node len_z_eq_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_z_len, d_zero); //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 sk_x_rest = NodeManager::currentNM()->mkSkolem( "ldssym_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); + 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 ); + //Node sk_x_rest = NodeManager::currentNM()->mkSkolem( "ldissym_$$", normal_forms[i][index_i].getType(), "created for induction" ); //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 - //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, 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 ); Node loop_x = normal_forms[other_n_index][other_index]; - Node loop_y = sk_y; - Node loop_z = sk_z; + Node loop_y = sk_y; + Node loop_z = sk_z; + + //Node loop_x = sk_x_rest; + //std::vector< Node > skc; + //skc.push_back( sk_y ); + //skc.push_back( sk_z ); + //Node loop_y = d_emptyString; + //Node loop_z = mkConcat( skc ); + //we will be done addNormalFormPair( normal_form_src[i], normal_form_src[j] ); Node ant = mkExplain( antec, antec_new_lits ); @@ -1415,7 +1431,7 @@ bool TheoryStrings::checkInductiveEquations() { NodeList* lst1 = (*it).second; NodeList* lst2 = (*d_ind_map2.find(x)).second; NodeList* lste = (*d_ind_map_exp.find(x)).second; - NodeList* lstl = (*d_ind_map_lemma.find(x)).second; + //NodeList* lstl = (*d_ind_map_lemma.find(x)).second; NodeList::const_iterator i1 = lst1->begin(); NodeList::const_iterator i2 = lst2->begin(); NodeList::const_iterator ie = lste->begin(); -- 2.30.2