diff options
Diffstat (limited to 'src/theory/strings/theory_strings.cpp')
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 1711 |
1 files changed, 1711 insertions, 0 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp new file mode 100644 index 000000000..7d5edd0f7 --- /dev/null +++ b/src/theory/strings/theory_strings.cpp @@ -0,0 +1,1711 @@ +/********************* */ +/*! \file theory_strings.cpp + ** \verbatim + ** Original author: Tianyi Liang + ** Major contributors: Tianyi Liang, Andrew Reynolds + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2013-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Implementation of the theory of strings. + ** + ** Implementation of the theory of strings. + **/ + + +#include "theory/strings/theory_strings.h" +#include "theory/valuation.h" +#include "expr/kind.h" +#include "theory/rewriter.h" +#include "expr/command.h" +#include "theory/model.h" +#include "smt/logic_exception.h" +#include "theory/strings/options.h" +#include "theory/strings/type_enumerator.h" +#include <cmath> + +#define STR_UNROLL_INDUCTION + +using namespace std; +using namespace CVC4::context; + +namespace CVC4 { +namespace theory { +namespace strings { + +TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) + : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo, qe), + d_notify( *this ), + d_equalityEngine(d_notify, c, "theory::strings::TheoryStrings"), + d_conflict( c, false ), + d_infer(c), + d_infer_exp(c), + d_nf_pairs(c), + d_ind_map1(c), + d_ind_map2(c), + d_ind_map_exp(c), + d_ind_map_lemma(c), + //d_lit_to_decide_index( c, 0 ), + //d_lit_to_decide( c ), + d_lit_to_unroll( c ) +{ + // The kinds we are treating as function application in congruence + d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP); + d_equalityEngine.addFunctionKind(kind::STRING_LENGTH); + d_equalityEngine.addFunctionKind(kind::STRING_CONCAT); + + d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) ); + d_emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") ); + d_true = NodeManager::currentNM()->mkConst( true ); + d_false = NodeManager::currentNM()->mkConst( false ); +} + +TheoryStrings::~TheoryStrings() { + +} + +Node TheoryStrings::getRepresentative( Node t ) { + if( d_equalityEngine.hasTerm( t ) ){ + return d_equalityEngine.getRepresentative( t ); + }else{ + return t; + } +} + +bool TheoryStrings::hasTerm( Node a ){ + return d_equalityEngine.hasTerm( a ); +} + +bool TheoryStrings::areEqual( Node a, Node b ){ + if( a==b ){ + return true; + }else if( hasTerm( a ) && hasTerm( b ) ){ + return d_equalityEngine.areEqual( a, b ); + }else{ + return false; + } +} + +bool TheoryStrings::areDisequal( Node a, Node b ){ + if( hasTerm( a ) && hasTerm( b ) ){ + return d_equalityEngine.areDisequal( a, b, false ); + }else{ + return false; + } +} + +Node TheoryStrings::getLength( Node t ) { + EqcInfo * ei = getOrMakeEqcInfo( t ); + Node length_term = ei->d_length_term; + if( length_term.isNull()) { + //typically shouldnt be necessary + length_term = t; + } + return NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, length_term ); +} + +void TheoryStrings::setMasterEqualityEngine(eq::EqualityEngine* eq) { + d_equalityEngine.setMasterEqualityEngine(eq); +} + +void TheoryStrings::addSharedTerm(TNode t) { + Debug("strings") << "TheoryStrings::addSharedTerm(): " + << t << " " << t.getType().isBoolean() << endl; + d_equalityEngine.addTriggerTerm(t, THEORY_STRINGS); + Debug("strings") << "TheoryStrings::addSharedTerm() finished" << std::endl; +} + +EqualityStatus TheoryStrings::getEqualityStatus(TNode a, TNode b) { + if( d_equalityEngine.hasTerm(a) && d_equalityEngine.hasTerm(b) ){ + if (d_equalityEngine.areEqual(a, b)) { + // The terms are implied to be equal + return EQUALITY_TRUE; + } + if (d_equalityEngine.areDisequal(a, b, false)) { + // The terms are implied to be dis-equal + return EQUALITY_FALSE; + } + } + return EQUALITY_UNKNOWN; +} + +void TheoryStrings::propagate(Effort e) +{ + // direct propagation now +} + +bool TheoryStrings::propagate(TNode literal) { + Debug("strings-propagate") << "TheoryStrings::propagate(" << literal << ")" << std::endl; + // If already in conflict, no more propagation + if (d_conflict) { + Debug("strings-propagate") << "TheoryStrings::propagate(" << literal << "): already in conflict" << std::endl; + return false; + } + Trace("strings-prop") << "strPropagate " << literal << std::endl; + // Propagate out + bool ok = d_out->propagate(literal); + if (!ok) { + d_conflict = true; + } + return ok; +} + +/** explain */ +void TheoryStrings::explain(TNode literal, std::vector<TNode>& assumptions){ + Debug("strings-explain") << "Explain " << literal << std::endl; + bool polarity = literal.getKind() != kind::NOT; + TNode atom = polarity ? literal : literal[0]; + if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) { + d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions); + } else { + d_equalityEngine.explainPredicate(atom, polarity, assumptions); + } +} + +Node TheoryStrings::explain( TNode literal ){ + std::vector< TNode > assumptions; + explain( literal, assumptions ); + if( assumptions.empty() ){ + return d_true; + }else if( assumptions.size()==1 ){ + return assumptions[0]; + }else{ + return NodeManager::currentNM()->mkNode( kind::AND, assumptions ); + } +} + +///////////////////////////////////////////////////////////////////////////// +// MODEL GENERATION +///////////////////////////////////////////////////////////////////////////// + + +void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) { + Trace("strings-model") << "TheoryStrings : Collect model info, fullModel = " << fullModel << std::endl; + Trace("strings-model") << "TheoryStrings : assertEqualityEngine." << std::endl; + m->assertEqualityEngine( &d_equalityEngine ); + // Generate model + std::vector< Node > nodes; + getEquivalenceClasses( nodes ); + std::map< Node, Node > processed; + std::vector< std::vector< Node > > col; + std::vector< Node > lts; + seperateByLength( nodes, col, lts ); + //step 1 : get all values for known lengths + std::vector< Node > lts_values; + //std::map< Node, bool > values_used; + for( unsigned i=0; i<col.size(); i++ ){ + Trace("strings-model") << "Checking length for " << col[i][0] << " (length is " << lts[i] << ")" << std::endl; + if( lts[i].isConst() ){ + lts_values.push_back( lts[i] ); + //values_used[ lts[i] ] = true; + }else{ + //get value for lts[i]; + if( !lts[i].isNull() ){ + Node v = d_valuation.getModelValue(lts[i]); + //Node v = m->getValue(lts[i]); + Trace("strings-model") << "Model value for " << lts[i] << " is " << v << std::endl; + lts_values.push_back( v ); + //values_used[ v ] = true; + }else{ + Trace("strings-model-warn") << "No length for eqc " << col[i][0] << std::endl; + Assert( false ); + lts_values.push_back( Node::null() ); + } + } + } + ////step 2 : assign arbitrary values for unknown lengths? + //for( unsigned i=0; i<col.size(); i++ ){ + // if( + //} + Trace("strings-model") << "Assign to equivalence classes..." << std::endl; + //step 3 : assign values to equivalence classes that are pure variables + for( unsigned i=0; i<col.size(); i++ ){ + std::vector< Node > pure_eq; + Trace("strings-model") << "The equivalence classes "; + for( unsigned j=0; j<col[i].size(); j++ ) { + Trace("strings-model") << col[i][j] << " "; + //check if col[i][j] has only variables + EqcInfo* ei = getOrMakeEqcInfo( col[i][j], false ); + Node cst = ei ? ei->d_const_term : Node::null(); + if( cst.isNull() ){ + Assert( d_normal_forms.find( col[i][j] )!=d_normal_forms.end() ); + if( d_normal_forms[col[i][j]].size()==1 ){//&& d_normal_forms[col[i][j]][0]==col[i][j] ){ + pure_eq.push_back( col[i][j] ); + } + }else{ + processed[col[i][j]] = cst; + } + } + Trace("strings-model") << "have length " << lts_values[i] << std::endl; + + Trace("strings-model") << "Need to assign values of length " << lts_values[i] << " to equivalence classes "; + for( unsigned j=0; j<pure_eq.size(); j++ ){ + Trace("strings-model") << pure_eq[j] << " "; + } + Trace("strings-model") << std::endl; + + //use type enumerator + StringEnumeratorLength sel(lts_values[i].getConst<Rational>().getNumerator().toUnsignedInt()); + for( unsigned j=0; j<pure_eq.size(); j++ ){ + Assert( !sel.isFinished() ); + Node c = *sel; + while( d_equalityEngine.hasTerm( c ) ){ + ++sel; + Assert( !sel.isFinished() ); + c = *sel; + } + ++sel; + Trace("strings-model") << "*** Assigned constant " << c << " for " << pure_eq[j] << std::endl; + processed[pure_eq[j]] = c; + m->assertEquality( pure_eq[j], c, true ); + } + } + Trace("strings-model") << "String Model : Finished." << std::endl; + //step 4 : assign constants to all other equivalence classes + for( unsigned i=0; i<nodes.size(); i++ ){ + if( processed.find( nodes[i] )==processed.end() ){ + Assert( d_normal_forms.find( nodes[i] )!=d_normal_forms.end() ); + Trace("strings-model") << "Construct model for " << nodes[i] << " based on normal form "; + for( unsigned j=0; j<d_normal_forms[nodes[i]].size(); j++ ) { + if( j>0 ) Trace("strings-model") << " ++ "; + Trace("strings-model") << d_normal_forms[nodes[i]][j]; + Node r = getRepresentative( d_normal_forms[nodes[i]][j] ); + if( !r.isConst() && processed.find( r )==processed.end() ){ + Trace("strings-model") << "(UNPROCESSED)"; + } + } + Trace("strings-model") << std::endl; + std::vector< Node > nc; + for( unsigned j=0; j<d_normal_forms[nodes[i]].size(); j++ ) { + Node r = getRepresentative( d_normal_forms[nodes[i]][j] ); + Assert( r.isConst() || processed.find( r )!=processed.end() ); + nc.push_back(r.isConst() ? r : processed[r]); + } + Node cc = mkConcat( nc ); + Assert( cc.getKind()==kind::CONST_STRING ); + Trace("strings-model") << "*** Determined constant " << cc << " for " << nodes[i] << std::endl; + processed[nodes[i]] = cc; + m->assertEquality( nodes[i], cc, true ); + } + } +} + +///////////////////////////////////////////////////////////////////////////// +// MAIN SOLVER +///////////////////////////////////////////////////////////////////////////// + +void TheoryStrings::preRegisterTerm(TNode n) { + Debug("strings-prereg") << "TheoryStrings::preRegisterTerm() " << n << endl; + //collectTerms( n ); + switch (n.getKind()) { + case kind::EQUAL: + d_equalityEngine.addTriggerEquality(n); + break; + case kind::STRING_IN_REGEXP: + d_equalityEngine.addTriggerPredicate(n); + break; + default: + if(n.getKind() == kind::VARIABLE || n.getKind()==kind::SKOLEM) { + if( std::find( d_length_intro_vars.begin(), d_length_intro_vars.end(), n )==d_length_intro_vars.end() ){ + Node n_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n); + Node n_len_geq_zero = NodeManager::currentNM()->mkNode( kind::GEQ, n_len, d_zero); + Trace("strings-lemma") << "Strings: Add lemma " << n_len_geq_zero << std::endl; + d_out->lemma(n_len_geq_zero); + } + } + if (n.getType().isBoolean()) { + // Get triggered for both equal and dis-equal + d_equalityEngine.addTriggerPredicate(n); + } else { + // Function applications/predicates + d_equalityEngine.addTerm(n); + } + break; + } +} + +void TheoryStrings::check(Effort e) { + bool polarity; + TNode atom; + + if( !done() && !hasTerm( d_emptyString ) ){ + preRegisterTerm( d_emptyString ); + } + + // Trace("strings-process") << "Theory of strings, check : " << e << std::endl; + Trace("strings-check") << "Theory of strings, check : " << e << std::endl; + while ( !done() && !d_conflict) + { + // Get all the assertions + Assertion assertion = get(); + TNode fact = assertion.assertion; + + Trace("strings-assertion") << "get assertion: " << fact << endl; + + polarity = fact.getKind() != kind::NOT; + atom = polarity ? fact : fact[0]; + if (atom.getKind() == kind::EQUAL) { + d_equalityEngine.assertEquality(atom, polarity, fact); + } else { + d_equalityEngine.assertPredicate(atom, polarity, fact); + } +#ifdef STR_UNROLL_INDUCTION + //check if it is a literal to unroll? + if( d_lit_to_unroll.find( atom )!=d_lit_to_unroll.end() ){ + Trace("strings-ind") << "Strings-ind : Possibly unroll for : " << atom << ", polarity = " << polarity << std::endl; + } +#endif + } + doPendingFacts(); + + + bool addedLemma = false; + if( e == EFFORT_FULL && !d_conflict ) { + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); + while( !eqcs_i.isFinished() ){ + Node eqc = (*eqcs_i); + //if eqc.getType is string + if (eqc.getType().isString()) { + //EqcInfo* ei = getOrMakeEqcInfo( eqc, true ); + //get the constant for the equivalence class + //int c_len = ...; + eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); + while( !eqc_i.isFinished() ){ + Node n = (*eqc_i); + + //if n is concat, and + //if n has not instantiatied the concat..length axiom + //then, add lemma + if( n.getKind() == kind::STRING_CONCAT || n.getKind() == kind::CONST_STRING ){ + if( d_length_inst.find(n)==d_length_inst.end() ){ + d_length_inst[n] = true; + Trace("strings-debug") << "get n: " << n << endl; + Node sk = NodeManager::currentNM()->mkSkolem( "lsym_$$", n.getType(), "created for concat lemma" ); + d_length_intro_vars.push_back( sk ); + Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, n ); + eq = Rewriter::rewrite(eq); + Trace("strings-lemma") << "Strings: Add lemma " << eq << std::endl; + d_out->lemma(eq); + Node skl = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk ); + Node lsum; + if( n.getKind() == kind::STRING_CONCAT ){ + //add lemma + std::vector<Node> node_vec; + for( unsigned i=0; i<n.getNumChildren(); i++ ) { + Node lni = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[i] ); + node_vec.push_back(lni); + } + lsum = NodeManager::currentNM()->mkNode( kind::PLUS, node_vec ); + }else{ + //add lemma + lsum = NodeManager::currentNM()->mkConst( ::CVC4::Rational( n.getConst<String>().size() ) ); + } + Node ceq = NodeManager::currentNM()->mkNode( kind::EQUAL, skl, lsum ); + ceq = Rewriter::rewrite(ceq); + Trace("strings-lemma") << "Strings: Add lemma " << ceq << std::endl; + d_out->lemma(ceq); + addedLemma = true; + } + } + ++eqc_i; + } + } + ++eqcs_i; + } + if( !addedLemma ){ + addedLemma = checkNormalForms(); + Trace("strings-process") << "Done check normal forms, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; + if(!d_conflict && !addedLemma) { + addedLemma = checkCardinality(); + Trace("strings-process") << "Done check cardinality, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; + if( !d_conflict && !addedLemma ){ + addedLemma = checkInductiveEquations(); + Trace("strings-process") << "Done check inductive equations, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; + } + } + } + } + Trace("strings-process") << "Theory of strings, done check : " << e << std::endl; +} + +TheoryStrings::EqcInfo::EqcInfo( context::Context* c ) : d_const_term(c), d_length_term(c), d_cardinality_lem_k(c) { + +} + +TheoryStrings::EqcInfo * TheoryStrings::getOrMakeEqcInfo( Node eqc, bool doMake ) { + std::map< Node, EqcInfo* >::iterator eqc_i = d_eqc_info.find( eqc ); + if( eqc_i==d_eqc_info.end() ){ + if( doMake ){ + EqcInfo* ei = new EqcInfo( getSatContext() ); + d_eqc_info[eqc] = ei; + return ei; + }else{ + return NULL; + } + }else{ + return (*eqc_i).second; + } +} + + +/** Conflict when merging two constants */ +void TheoryStrings::conflict(TNode a, TNode b){ + Node conflictNode; + if (a.getKind() == kind::CONST_BOOLEAN) { + conflictNode = explain( a.iffNode(b) ); + } else { + conflictNode = explain( a.eqNode(b) ); + } + Debug("strings-conflict") << "CONFLICT: Eq engine conflict : " << conflictNode << std::endl; + d_out->conflict( conflictNode ); + d_conflict = true; +} + +/** called when a new equivalance class is created */ +void TheoryStrings::eqNotifyNewClass(TNode t){ + if( t.getKind() == kind::CONST_STRING ){ + EqcInfo * ei =getOrMakeEqcInfo( t, true ); + ei->d_const_term = t; + } + if( t.getKind() == kind::STRING_LENGTH ){ + Trace("strings-debug") << "New length eqc : " << t << std::endl; + Node r = d_equalityEngine.getRepresentative(t[0]); + EqcInfo * ei = getOrMakeEqcInfo( r, true ); + ei->d_length_term = t[0]; + } +} + +/** called when two equivalance classes will merge */ +void TheoryStrings::eqNotifyPreMerge(TNode t1, TNode t2){ + EqcInfo * e2 = getOrMakeEqcInfo(t2, false); + if( e2 ){ + EqcInfo * e1 = getOrMakeEqcInfo( t1 ); + //add information from e2 to e1 + if( !e2->d_const_term.get().isNull() ){ + e1->d_const_term.set( e2->d_const_term ); + } + if( !e2->d_length_term.get().isNull() ){ + e1->d_length_term.set( e2->d_length_term ); + } + if( e2->d_cardinality_lem_k.get()>e1->d_cardinality_lem_k.get() ) { + e1->d_cardinality_lem_k.set( e2->d_cardinality_lem_k ); + } + } + if( hasTerm( d_zero ) ){ + Node leqc; + if( areEqual(d_zero, t1) ){ + leqc = t2; + }else if( areEqual(d_zero, t2) ){ + leqc = t1; + } + if( !leqc.isNull() ){ + //scan equivalence class to see if we apply + eq::EqClassIterator eqc_i = eq::EqClassIterator( leqc, &d_equalityEngine ); + while( !eqc_i.isFinished() ){ + Node n = (*eqc_i); + if( n.getKind()==kind::STRING_LENGTH ){ + if( !hasTerm( d_emptyString ) || !areEqual(n[0], d_emptyString ) ){ + //apply the rule length(n[0])==0 => n[0] == "" + Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, n[0], d_emptyString ); + d_pending.push_back( eq ); + Node eq_exp = NodeManager::currentNM()->mkNode( kind::EQUAL, n, d_zero ); + d_pending_exp[eq] = eq_exp; + Trace("strings-infer") << "Strings : Infer " << eq << " from " << eq_exp << std::endl; + d_infer.push_back(eq); + d_infer_exp.push_back(eq_exp); + } + } + ++eqc_i; + } + } + } +} + +/** called when two equivalance classes have merged */ +void TheoryStrings::eqNotifyPostMerge(TNode t1, TNode t2) { + +} + +/** called when two equivalance classes are disequal */ +void TheoryStrings::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { + +} + +void TheoryStrings::computeCareGraph(){ + Theory::computeCareGraph(); +} + +void TheoryStrings::doPendingFacts() { + int i=0; + while( !d_conflict && i<(int)d_pending.size() ){ + Node fact = d_pending[i]; + Node exp = d_pending_exp[ fact ]; + Trace("strings-pending") << "Process pending fact : " << fact << " from " << exp << std::endl; + bool polarity = fact.getKind() != kind::NOT; + TNode atom = polarity ? fact : fact[0]; + if (atom.getKind() == kind::EQUAL) { + 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 ); + } + i++; + } + d_pending.clear(); + d_pending_exp.clear(); +} +void TheoryStrings::doPendingLemmas() { + if( !d_conflict && !d_lemma_cache.empty() ){ + for( unsigned i=0; i<d_lemma_cache.size(); i++ ){ + Trace("strings-pending") << "Process pending lemma : " << d_lemma_cache[i] << std::endl; + d_out->lemma( d_lemma_cache[i] ); + } + for( std::map< Node, bool >::iterator it = d_pending_req_phase.begin(); it != d_pending_req_phase.end(); ++it ){ + Trace("strings-pending") << "Require phase : " << it->first << ", polarity = " << it->second << std::endl; + d_out->requirePhase( it->first, it->second ); + } + d_lemma_cache.clear(); + d_pending_req_phase.clear(); + } +} + +void TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std::vector< Node > & nf, + std::vector< std::vector< Node > > &normal_forms, std::vector< std::vector< Node > > &normal_forms_exp, std::vector< Node > &normal_form_src) { + // EqcItr + eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); + while( !eqc_i.isFinished() ) { + Node n = (*eqc_i); + Trace("strings-process") << "Process term " << n << std::endl; + if( n.getKind() == kind::CONST_STRING || n.getKind() == kind::STRING_CONCAT ) { + std::vector<Node> nf_n; + std::vector<Node> nf_exp_n; + if( n.getKind() == kind::CONST_STRING ){ + if( n!=d_emptyString ) { + nf_n.push_back( n ); + } + } else if( n.getKind() == kind::STRING_CONCAT ) { + for( unsigned i=0; i<n.getNumChildren(); i++ ) { + Node nr = d_equalityEngine.getRepresentative( n[i] ); + std::vector< Node > nf_temp; + std::vector< Node > nf_exp_temp; + Trace("strings-process") << "Normalizing subterm " << n[i] << " = " << nr << std::endl; + normalizeEquivalenceClass( nr, visited, nf_temp, nf_exp_temp ); + if( d_conflict || !d_pending.empty() || !d_lemma_cache.empty() ) { + return; + } + if( nf.size()!=1 || nf[0]!=d_emptyString ) { + for( unsigned r=0; r<nf_temp.size(); r++ ) { + Assert( nf_temp[r].getKind()!=kind::STRING_CONCAT ); + } + nf_n.insert( nf_n.end(), nf_temp.begin(), nf_temp.end() ); + } + nf_exp_n.insert( nf_exp_n.end(), nf_exp_temp.begin(), nf_exp_temp.end() ); + if( nr!=n[i] ) { + nf_exp_n.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, n[i], nr ) ); + } + } + } + normal_forms.push_back(nf_n); + normal_forms_exp.push_back(nf_exp_n); + normal_form_src.push_back(n); + } + /* should we add these? + else { + //var/sk? + std::vector<Node> nf_n; + std::vector<Node> nf_exp_n; + nf_n.push_back(n); + normal_forms.push_back(nf_n); + normal_forms_exp.push_back(nf_exp_n); + normal_form_src.push_back(n); + }*/ + ++eqc_i; + } + + // Test the result + if( !normal_forms.empty() ) { + Trace("strings-solve") << "--- Normal forms for equivlance class " << eqc << " : " << std::endl; + for( unsigned i=0; i<normal_forms.size(); i++ ) { + Trace("strings-solve") << "#" << i << " (from " << normal_form_src[i] << ") : "; + for( unsigned j=0; j<normal_forms[i].size(); j++ ) { + if(j>0) Trace("strings-solve") << ", "; + Trace("strings-solve") << normal_forms[i][j]; + } + Trace("strings-solve") << std::endl; + Trace("strings-solve") << " Explanation is : "; + if(normal_forms_exp[i].size() == 0) { + Trace("strings-solve") << "NONE"; + } else { + for( unsigned j=0; j<normal_forms_exp[i].size(); j++ ) { + if(j>0) Trace("strings-solve") << " AND "; + Trace("strings-solve") << normal_forms_exp[i][j]; + } + } + Trace("strings-solve") << std::endl; + } + } +} +//nf_exp is conjunction +void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< Node > & nf_exp ) { + Trace("strings-process") << "Process equivalence class " << eqc << std::endl; + if( std::find( visited.begin(), visited.end(), eqc )!=visited.end() ){ + //nf.push_back( eqc ); + if( eqc.getKind()==kind::STRING_CONCAT ){ + for( unsigned i=0; i<eqc.getNumChildren(); i++ ){ + if( !d_equalityEngine.hasTerm(d_emptyString) || !d_equalityEngine.areEqual( eqc[i], d_emptyString ) ){ + nf.push_back( eqc[i] ); + } + } + }else if( !d_equalityEngine.hasTerm(d_emptyString) || !d_equalityEngine.areEqual( eqc, d_emptyString ) ){ + nf.push_back( eqc ); + } + Trace("strings-process") << "Return process equivalence class " << eqc << " : already visited." << std::endl; + } else if (d_equalityEngine.hasTerm(d_emptyString) && d_equalityEngine.areEqual( eqc, d_emptyString )){ + //do nothing + Trace("strings-process") << "Return process equivalence class " << eqc << " : empty." << std::endl; + d_normal_forms[eqc].clear(); + d_normal_forms_exp[eqc].clear(); + } else { + visited.push_back( eqc ); + if(d_normal_forms.find(eqc)==d_normal_forms.end() ){ + //phi => t = s1 * ... * sn + // normal form for each non-variable term in this eqc (s1...sn) + std::vector< std::vector< Node > > normal_forms; + // explanation for each normal form (phi) + std::vector< std::vector< Node > > normal_forms_exp; + // record terms for each normal form (t) + std::vector< Node > normal_form_src; + //Get Normal Forms + getNormalForms(eqc, visited, nf, normal_forms, normal_forms_exp, normal_form_src); + if( d_conflict || !d_pending.empty() || !d_lemma_cache.empty() ) { + return; + } + + unsigned i = 0; + //unify each normal form > 0 with normal_forms[0] + for( unsigned j=1; j<normal_forms.size(); j++ ) { + + Trace("strings-solve") << "Process normal form #0 against #" << j << "..." << std::endl; + if( isNormalFormPair( normal_form_src[i], normal_form_src[j] ) ){ + Trace("strings-solve") << "Already normalized (in cache)." << std::endl; + }else{ + Trace("strings-solve") << "Not in cache." << std::endl; + //the current explanation for why the prefix is equal + std::vector< Node > curr_exp; + curr_exp.insert(curr_exp.end(), normal_forms_exp[i].begin(), normal_forms_exp[i].end() ); + curr_exp.insert(curr_exp.end(), normal_forms_exp[j].begin(), normal_forms_exp[j].end() ); + curr_exp.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, normal_form_src[i], normal_form_src[j] ) ); + //ensure that normal_forms[i] and normal_forms[j] are the same modulo equality + unsigned index_i = 0; + unsigned index_j = 0; + bool success; + do + { + success = false; + //if we are at the end + if(index_i==normal_forms[i].size() || index_j==normal_forms[j].size() ) { + if( index_i==normal_forms[i].size() && index_j==normal_forms[j].size() ){ + //we're done + addNormalFormPair( normal_form_src[i], normal_form_src[j] ); + }else{ + //the remainder must be empty + unsigned k = index_i==normal_forms[i].size() ? j : i; + unsigned index_k = index_i==normal_forms[i].size() ? index_j : index_i; + while(!d_conflict && index_k<normal_forms[k].size()) { + //can infer that this string must be empty + Node eq_exp; + if( curr_exp.empty() ) { + eq_exp = d_true; + } else if( curr_exp.size() == 1 ) { + eq_exp = curr_exp[0]; + } else { + eq_exp = NodeManager::currentNM()->mkNode( kind::AND, curr_exp ); + } + 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_pending.push_back( eq ); + d_pending_exp[eq] = eq_exp; + d_infer.push_back(eq); + d_infer_exp.push_back(eq_exp); + index_k++; + } + } + }else { + Trace("strings-solve-debug") << "Process " << normal_forms[i][index_i] << " ... " << normal_forms[j][index_j] << std::endl; + if(areEqual(normal_forms[i][index_i],normal_forms[j][index_j])){ + Trace("strings-solve-debug") << "Case 1 : strings are equal" << std::endl; + //terms are equal, continue + if( normal_forms[i][index_i]!=normal_forms[j][index_j] ){ + Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL,normal_forms[i][index_i], + normal_forms[j][index_j]); + Trace("strings-solve-debug") << "Add to explanation : " << eq << std::endl; + curr_exp.push_back(eq); + } + index_j++; + index_i++; + success = true; + }else{ + Node length_term_i = getLength( normal_forms[i][index_i] ); + Node length_term_j = getLength( normal_forms[j][index_j] ); + //check if length(normal_forms[i][index]) == length(normal_forms[j][index]) + if( areEqual(length_term_i, length_term_j) ){ + Trace("strings-solve-debug") << "Case 2 : string lengths are equal" << std::endl; + //length terms are equal, merge equivalence classes if not already done so + Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[i][index_i], normal_forms[j][index_j] ); + std::vector< Node > temp_exp; + temp_exp.insert(temp_exp.end(), curr_exp.begin(), curr_exp.end() ); + temp_exp.push_back(NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j )); + Node eq_exp = temp_exp.empty() ? d_true : + temp_exp.size() == 1 ? temp_exp[0] : NodeManager::currentNM()->mkNode( kind::AND, temp_exp ); + Trace("strings-lemma") << "Strings : Infer " << eq << " from " << eq_exp << std::endl; + //d_equalityEngine.assertEquality( eq, true, eq_exp ); + d_pending.push_back( eq ); + d_pending_exp[eq] = eq_exp; + d_infer.push_back(eq); + d_infer_exp.push_back(eq_exp); + return; + }else if( ( normal_forms[i][index_i].getKind()!=kind::CONST_STRING && index_i==normal_forms[i].size()-1 ) || + ( normal_forms[j][index_j].getKind()!=kind::CONST_STRING && index_j==normal_forms[j].size()-1 ) ){ + Trace("strings-solve-debug") << "Case 3 : at endpoint" << std::endl; + Node conc; + std::vector< Node > antec; + antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); + std::vector< Node > antec_new_lits; + std::vector< Node > eqn; + for( unsigned r=0; r<2; r++ ){ + int index_k = r==0 ? index_i : index_j; + int k = r==0 ? i : j; + std::vector< Node > eqnc; + for( unsigned index_l=index_k; index_l<normal_forms[k].size(); index_l++ ){ + eqnc.push_back( normal_forms[k][index_l] ); + } + eqn.push_back( mkConcat( eqnc ) ); + } + conc = eqn[0].eqNode( eqn[1] ); + Node ant = mkExplain( antec, antec_new_lits ); + sendLemma( ant, conc, "Endpoint" ); + return; + }else{ + Trace("strings-solve-debug") << "Case 4 : must compare strings" << std::endl; + Node conc; + std::vector< Node > antec; + std::vector< Node > antec_new_lits; + //check for loops + //Trace("strings-loop") << "Check for loops i,j = " << (index_i+1) << "/" << normal_forms[i].size() << " " << (index_j+1) << "/" << normal_forms[j].size() << std::endl; + int has_loop[2] = { -1, -1 }; + for( unsigned r=0; r<2; r++ ){ + int index = (r==0 ? index_i : index_j); + int other_index = (r==0 ? index_j : index_i ); + int n_index = (r==0 ? i : j); + int other_n_index = (r==0 ? j : i); + if( normal_forms[other_n_index][other_index].getKind() != kind::CONST_STRING ) { + for( unsigned lp = index+1; lp<normal_forms[n_index].size(); lp++ ){ + if( normal_forms[n_index][lp]==normal_forms[other_n_index][other_index] ){ + has_loop[r] = lp; + break; + } + } + } + } + if( has_loop[0]!=-1 || has_loop[1]!=-1 ){ + int loop_n_index = has_loop[0]!=-1 ? i : j; + int other_n_index = has_loop[0]!=-1 ? j : i; + int loop_index = has_loop[0]!=-1 ? has_loop[0] : has_loop[1]; + int index = has_loop[0]!=-1 ? index_i : index_j; + int other_index = has_loop[0]!=-1 ? index_j : index_i; + Trace("strings-loop") << "Detected possible loop for " << normal_forms[loop_n_index][loop_index]; + Trace("strings-loop") << " ... " << normal_forms[other_n_index][other_index] << std::endl; + + //we have x * s1 * .... * sm = t1 * ... * tn * x * r1 * ... * rp + //check if + //t1 * ... * tn = n[loop_n_index][index]....n[loop_n_index][loop_index-1] = y * z + // and + //s1 * ... * sk = n[other_n_index][other_index+1].....n[other_n_index][k+1] = z * y + // for some y,z,k + + Trace("strings-loop") << "Must add lemma." << std::endl; + //need to break + Node sk_y= NodeManager::currentNM()->mkSkolem( "ysym_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); + Node sk_z= NodeManager::currentNM()->mkSkolem( "zsym_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); + + antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); + //require that x is non-empty + Node x_empty = normal_forms[loop_n_index][loop_index].eqNode( d_emptyString ); + x_empty = Rewriter::rewrite( x_empty ); + //if( d_equalityEngine.hasTerm( d_emptyString ) && d_equalityEngine.areDisequal( normal_forms[loop_n_index][loop_index], d_emptyString, true ) ){ + // antec.push_back( x_empty.negate() ); + //}else{ + antec_new_lits.push_back( x_empty.negate() ); + //} + d_pending_req_phase[ x_empty ] = true; + + + //t1 * ... * tn = y * z + std::vector< Node > c1c; + //n[loop_n_index][index]....n[loop_n_index][loop_lindex-1] + for( int r=index; r<=loop_index-1; r++ ) { + c1c.push_back( normal_forms[loop_n_index][r] ); + } + Node conc1 = mkConcat( c1c ); + conc1 = NodeManager::currentNM()->mkNode( kind::EQUAL, conc1, + NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk_y, sk_z ) ); + std::vector< Node > c2c; + //s1 * ... * sk = n[other_n_index][other_index+1].....n[other_n_index][k+1] + for( int r=other_index+1; r < (int)normal_forms[other_n_index].size(); r++ ) { + c2c.push_back( normal_forms[other_n_index][r] ); + } + Node left2 = mkConcat( c2c ); + std::vector< Node > c3c; + c3c.push_back( sk_z ); + c3c.push_back( sk_y ); + //r1 * ... * rk = n[loop_n_index][loop_index+1]....n[loop_n_index][loop_index-1] + for( int r=loop_index+1; r < (int)normal_forms[loop_n_index].size(); r++ ) { + c3c.push_back( normal_forms[loop_n_index][r] ); + } + Node conc2 = NodeManager::currentNM()->mkNode( kind::EQUAL, left2, + mkConcat( c3c ) ); + + 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 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 ant = mkExplain( antec, antec_new_lits ); + 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 ); + + //we will be done + addNormalFormPair( normal_form_src[i], normal_form_src[j] ); + sendLemma( ant, conc, "Loop" ); + addInductiveEquation( normal_forms[other_n_index][other_index], sk_y, sk_z, ant, "Loop Induction" ); + return; + }else{ + Trace("strings-solve-debug") << "No loops detected." << std::endl; + if( normal_forms[i][index_i].getKind() == kind::CONST_STRING || + normal_forms[j][index_j].getKind() == kind::CONST_STRING) { + unsigned const_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? i : j; + unsigned const_index_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? index_i : index_j; + unsigned nconst_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? j : i; + unsigned nconst_index_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? index_j : index_i; + Node const_str = normal_forms[const_k][const_index_k]; + Node other_str = normal_forms[nconst_k][nconst_index_k]; + if( other_str.getKind() == kind::CONST_STRING ) { + unsigned len_short = const_str.getConst<String>().size() <= other_str.getConst<String>().size() ? const_str.getConst<String>().size() : other_str.getConst<String>().size(); + if( const_str.getConst<String>().strncmp(other_str.getConst<String>(), len_short) ) { + //same prefix + //k is the index of the string that is shorter + int k = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? i : j; + int index_k = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? index_i : index_j; + int l = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? j : i; + int index_l = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? index_j : index_i; + Node remainderStr = NodeManager::currentNM()->mkConst( normal_forms[l][index_l].getConst<String>().substr(len_short) ); + Trace("strings-solve-debug-test") << "Break normal form of " << normal_forms[l][index_l] << " into " << normal_forms[k][index_k] << ", " << remainderStr << std::endl; + normal_forms[l].insert( normal_forms[l].begin()+index_l + 1, remainderStr ); + normal_forms[l][index_l] = normal_forms[k][index_k]; + success = true; + } else { + //curr_exp is conflict + antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); + Node ant = mkExplain( antec, antec_new_lits ); + sendLemma( ant, conc, "Conflict" ); + return; + } + } else { + Assert( other_str.getKind()!=kind::STRING_CONCAT ); + antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); + Node firstChar = const_str.getConst<String>().size() == 1 ? const_str : + NodeManager::currentNM()->mkConst( const_str.getConst<String>().substr(0, 1) ); + //split the string + Node sk = NodeManager::currentNM()->mkSkolem( "ssym_$$", normal_forms[i][index_i].getType(), "created for split" ); + + Node eq1 = NodeManager::currentNM()->mkNode( kind::EQUAL, other_str, d_emptyString ); + Node eq2_m = NodeManager::currentNM()->mkNode( kind::EQUAL, other_str, + NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, firstChar, sk ) ); + Node eq2 = eq2_m;//NodeManager::currentNM()->mkNode( kind::AND, eq2_m, sk_len_geq_zero ); + conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 ); + Trace("strings-solve-debug") << "Break normal form constant/variable " << std::endl; + + Node ant = mkExplain( antec, antec_new_lits ); + sendLemma( ant, conc, "Constant Split" ); + return; + } + }else{ + antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); + + Node ldeq = NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j ).negate(); + if( d_equalityEngine.areDisequal( length_term_i, length_term_j, true ) ){ + antec.push_back( ldeq ); + }else{ + antec_new_lits.push_back(ldeq); + } + Node sk = NodeManager::currentNM()->mkSkolem( "ssym_$$", normal_forms[i][index_i].getType(), "created for split" ); + Node eq1 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[i][index_i], + NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[j][index_j], sk ) ); + Node eq2 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[j][index_j], + NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[i][index_i], sk ) ); + conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 ); + // |sk| > 0 + //Node sk_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk ); + //Node sk_gt_zero = NodeManager::currentNM()->mkNode( kind::GT, sk_len, d_zero); + Node sk_gt_zero = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, d_emptyString).negate(); + Trace("strings-lemma") << "Strings lemma : " << sk_gt_zero << std::endl; + //d_out->lemma(sk_gt_zero); + d_lemma_cache.push_back( sk_gt_zero ); + + Node ant = mkExplain( antec, antec_new_lits ); + sendLemma( ant, conc, "Split" ); + return; + } + } + } + } + } + }while(success); + } + } + + //construct the normal form + if( normal_forms.empty() ){ + Trace("strings-solve-debug2") << "construct the normal form" << std::endl; + nf.push_back( eqc ); + } else { + Trace("strings-solve-debug2") << "just take the first normal form" << std::endl; + //just take the first normal form + nf.insert( nf.end(), normal_forms[0].begin(), normal_forms[0].end() ); + nf_exp.insert( nf_exp.end(), normal_forms_exp[0].begin(), normal_forms_exp[0].end() ); + if( eqc!=normal_form_src[0] ){ + nf_exp.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, eqc, normal_form_src[0] ) ); + } + Trace("strings-solve-debug2") << "just take the first normal form ... done" << std::endl; + } + //if( visited.empty() ){ + //TODO : cache? + //} + d_normal_forms[eqc].insert( d_normal_forms[eqc].end(), nf.begin(), nf.end() ); + d_normal_forms_exp[eqc].insert( d_normal_forms_exp[eqc].end(), nf_exp.begin(), nf_exp.end() ); + Trace("strings-process") << "Return process equivalence class " << eqc << " : returned." << std::endl; + }else{ + Trace("strings-process") << "Return process equivalence class " << eqc << " : already computed." << std::endl; + nf.insert( nf.end(), d_normal_forms[eqc].begin(), d_normal_forms[eqc].end() ); + nf_exp.insert( nf_exp.end(), d_normal_forms_exp[eqc].begin(), d_normal_forms_exp[eqc].end() ); + } + visited.pop_back(); + } +} + +bool TheoryStrings::normalizeDisequality( Node ni, Node nj ) { + //Assert( areDisequal( ni, nj ) ); + if( d_normal_forms[ni].size()>1 || d_normal_forms[nj].size()>1 ){ + unsigned index = 0; + while( index<d_normal_forms[ni].size() ){ + Node i = d_normal_forms[ni][index]; + Node j = d_normal_forms[nj][index]; + Trace("strings-solve-debug") << "...Processing " << i << " " << j << std::endl; + if( !areEqual( i, j ) ){ + Node li = getLength( i ); + Node lj = getLength( j ); + if( !areEqual(li, lj) ){ + Trace("strings-solve") << "Case 2 : add lemma " << std::endl; + //must add lemma + std::vector< Node > antec; + std::vector< Node > antec_new_lits; + antec.insert( antec.end(), d_normal_forms_exp[ni].begin(), d_normal_forms_exp[ni].end() ); + antec.insert( antec.end(), d_normal_forms_exp[nj].begin(), d_normal_forms_exp[nj].end() ); + antec.push_back( ni.eqNode( nj ).negate() ); + antec_new_lits.push_back( li.eqNode( lj ) ); + std::vector< Node > conc; + Node sk1 = NodeManager::currentNM()->mkSkolem( "w1sym_$$", ni.getType(), "created for disequality normalization" ); + Node sk2 = NodeManager::currentNM()->mkSkolem( "w2sym_$$", ni.getType(), "created for disequality normalization" ); + Node sk3 = NodeManager::currentNM()->mkSkolem( "w3sym_$$", ni.getType(), "created for disequality normalization" ); + Node sk4 = NodeManager::currentNM()->mkSkolem( "w4sym_$$", ni.getType(), "created for disequality normalization" ); + Node sk5 = NodeManager::currentNM()->mkSkolem( "w5sym_$$", ni.getType(), "created for disequality normalization" ); + Node w1w2w3 = NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2, sk3 ); + Node w1w4w5 = NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk4, sk5 ); + Node s_eq_w1w2w3 = NodeManager::currentNM()->mkNode( kind::EQUAL, ni, w1w2w3 ); + conc.push_back( s_eq_w1w2w3 ); + Node t_eq_w1w4w5 = NodeManager::currentNM()->mkNode( kind::EQUAL, nj, w1w4w5 ); + conc.push_back( t_eq_w1w4w5 ); + Node w2_neq_w4 = sk2.eqNode( sk4 ).negate(); + conc.push_back( w2_neq_w4 ); + Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational( 1 ) ); + Node w2_len_one = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2), one); + conc.push_back( w2_len_one ); + Node w4_len_one = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk4), one); + conc.push_back( w4_len_one ); + + //Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2), + // NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk4) ); + //conc.push_back( eq ); + sendLemma( mkExplain( antec, antec_new_lits ), NodeManager::currentNM()->mkNode( kind::AND, conc ), "Disequality Normalize" ); + return true; + }else if( areDisequal( i, j ) ){ + Trace("strings-solve") << "Case 1 : found equal length disequal sub strings " << i << " " << j << std::endl; + //we are done + return false; + } + } + index++; + } + Assert( false ); + } + return false; +} + +void TheoryStrings::addNormalFormPair( Node n1, Node n2 ) { + if( !isNormalFormPair( n1, n2 ) ){ + NodeList* lst; + NodeListMap::iterator nf_i = d_nf_pairs.find( n1 ); + if( nf_i == d_nf_pairs.end() ){ + if( d_nf_pairs.find( n2 )!=d_nf_pairs.end() ){ + addNormalFormPair( n2, n1 ); + return; + } + lst = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false, + ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) ); + d_nf_pairs.insertDataFromContextMemory( n1, lst ); + Trace("strings-nf") << "Create cache for " << n1 << std::endl; + }else{ + lst = (*nf_i).second; + } + Trace("strings-nf") << "Add normal form pair : " << n1 << " " << n2 << std::endl; + lst->push_back( n2 ); + Assert( isNormalFormPair( n1, n2 ) ); + }else{ + Trace("strings-nf-debug") << "Already a normal form pair " << n1 << " " << n2 << std::endl; + } + +} +bool TheoryStrings::isNormalFormPair( Node n1, Node n2 ) { + //TODO: modulo equality? + return isNormalFormPair2( n1, n2 ) || isNormalFormPair2( n2, n1 ); +} +bool TheoryStrings::isNormalFormPair2( Node n1, Node n2 ) { + //Trace("strings-debug") << "is normal form pair. " << n1 << " " << n2 << std::endl; + NodeList* lst; + NodeListMap::iterator nf_i = d_nf_pairs.find( n1 ); + if( nf_i != d_nf_pairs.end() ){ + lst = (*nf_i).second; + for( NodeList::const_iterator i = lst->begin(); i != lst->end(); ++i ) { + Node n = *i; + if( n==n2 ){ + return true; + } + } + } + return false; +} + +bool TheoryStrings::addInductiveEquation( Node x, Node y, Node z, Node exp, const char * c ) { + Trace("strings-solve-debug") << "add inductive equation for " << x << " = (" << y << " " << z << ")* " << y << std::endl; +#ifdef STR_UNROLL_INDUCTION + Node w = NodeManager::currentNM()->mkSkolem( "wsym_$$", x.getType(), "created for induction" ); + Node x_eq_y_w = NodeManager::currentNM()->mkNode( kind::EQUAL, x, + NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, y, w ) ); + Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, x_eq_y_w ); + Trace("strings-lemma") << "Strings " << c << " lemma : " << lem << std::endl; + d_lemma_cache.push_back( lem ); + + //add initial induction + Node lit1 = w.eqNode( d_emptyString ); + lit1 = Rewriter::rewrite( lit1 ); + Node wp = NodeManager::currentNM()->mkSkolem( "wpsym_$$", x.getType(), "created for induction" ); + Node lit2 = w.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, z, y, wp ) ); + lit2 = Rewriter::rewrite( lit2 ); + Node split_lem = NodeManager::currentNM()->mkNode( kind::OR, lit1, lit2 ); + Trace("strings-ind") << "Strings : Lemma " << c << " for unrolling " << split_lem << std::endl; + Trace("strings-lemma") << "Strings : Lemma " << c << " for unrolling " << split_lem << std::endl; + d_lemma_cache.push_back( split_lem ); + + //d_lit_to_decide.push_back( lit1 ); + d_lit_to_unroll[lit2] = true; + d_pending_req_phase[lit1] = true; + d_pending_req_phase[lit2] = false; + + x = w; + std::vector< Node > skc; + skc.push_back( y ); + skc.push_back( z ); + y = d_emptyString; + z = mkConcat( skc ); +#endif + + NodeListMap::iterator itr_x_y = d_ind_map1.find(x); + NodeList* lst1; + NodeList* lst2; + NodeList* lste; + NodeList* lstl; + if( itr_x_y == d_ind_map1.end() ) { + // add x->y + lst1 = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false, + ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) ); + d_ind_map1.insertDataFromContextMemory( x, lst1 ); + // add x->z + lst2 = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false, + ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) ); + d_ind_map2.insertDataFromContextMemory( x, lst2 ); + // add x->exp + lste = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false, + ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) ); + d_ind_map_exp.insertDataFromContextMemory( x, lste ); + // add x->hasLemma false + lstl = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false, + ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) ); + d_ind_map_lemma.insertDataFromContextMemory( x, lstl ); + } else { + //TODO: x in (yz)*y (exp) vs x in (y1 z1)*y1 (exp1) + lst1 = (*itr_x_y).second; + lst2 = (*d_ind_map2.find(x)).second; + lste = (*d_ind_map_exp.find(x)).second; + lstl = (*d_ind_map_lemma.find(x)).second; + Trace("strings-solve-debug") << "Already in maps " << x << " = (" << lst1 << " " << lst2 << ")* " << lst1 << std::endl; + Trace("strings-solve-debug") << "... with exp = " << lste << std::endl; + } + lst1->push_back( y ); + lst2->push_back( z ); + lste->push_back( exp ); +#ifdef STR_UNROLL_INDUCTION + return true; +#else + return false; +#endif +} + +void TheoryStrings::sendLemma( Node ant, Node conc, const char * c ) { + if( conc.isNull() ){ + d_out->conflict(ant); + Trace("strings-conflict") << "CONFLICT : Strings conflict : " << ant << std::endl; + d_conflict = true; + }else{ + Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, ant, conc ); + Trace("strings-lemma") << "Strings " << c << " lemma : " << lem << std::endl; + d_lemma_cache.push_back( lem ); + } +} + +void TheoryStrings::sendSplit( Node a, Node b, const char * c ) { + Node eq = a.eqNode( b ); + eq = Rewriter::rewrite( eq ); + Node neq = NodeManager::currentNM()->mkNode( kind::NOT, eq ); + Node lemma_or = NodeManager::currentNM()->mkNode( kind::OR, eq, neq ); + Trace("strings-lemma") << "Strings " << c << " split lemma : " << lemma_or << std::endl; + d_lemma_cache.push_back(lemma_or); + d_pending_req_phase[eq] = true; +} + +Node TheoryStrings::mkConcat( std::vector< Node >& c ) { + Node cc = c.size()>1 ? NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, c ) : ( c.size()==1 ? c[0] : d_emptyString ); + return Rewriter::rewrite( cc ); +} + +Node TheoryStrings::mkExplain( std::vector< Node >& a, std::vector< Node >& an ) { + std::vector< TNode > antec_exp; + for( unsigned i=0; i<a.size(); i++ ){ + Trace("strings-solve-debug") << "Ask for explanation of " << a[i] << std::endl; + //assert + if(a[i].getKind() == kind::EQUAL) { + //assert( hasTerm(a[i][0]) ); + //assert( hasTerm(a[i][1]) ); + Assert( areEqual(a[i][0], a[i][1]) ); + } else if( a[i].getKind()==kind::NOT && a[i][0].getKind()==kind::EQUAL ){ + Assert( hasTerm(a[i][0][0]) ); + Assert( hasTerm(a[i][0][1]) ); + Assert( d_equalityEngine.areDisequal(a[i][0][0], a[i][0][1], true) ); + } + unsigned ps = antec_exp.size(); + explain(a[i], antec_exp); + Trace("strings-solve-debug") << "Done, explanation was : " << std::endl; + for( unsigned j=ps; j<antec_exp.size(); j++ ){ + Trace("strings-solve-debug") << " " << antec_exp[j] << std::endl; + } + Trace("strings-solve-debug") << std::endl; + } + for( unsigned i=0; i<an.size(); i++ ){ + Trace("strings-solve-debug") << "Add to explanation (new literal) " << an[i] << std::endl; + antec_exp.push_back(an[i]); + } + Node ant; + if( antec_exp.empty() ) { + ant = d_true; + } else if( antec_exp.size()==1 ) { + ant = antec_exp[0]; + } else { + ant = NodeManager::currentNM()->mkNode( kind::AND, antec_exp ); + } + ant = Rewriter::rewrite( ant ); + return ant; +} + +bool TheoryStrings::checkNormalForms() { + Trace("strings-process") << "Normalize equivalence classes...." << std::endl; + eq::EqClassesIterator eqcs2_i = eq::EqClassesIterator( &d_equalityEngine ); + for( unsigned t=0; t<2; t++ ){ + Trace("strings-eqc") << (t==0 ? "STRINGS:" : "OTHER:") << std::endl; + while( !eqcs2_i.isFinished() ){ + Node eqc = (*eqcs2_i); + bool print = (t==0 && eqc.getType().isString() ) || (t==1 && !eqc.getType().isString() ); + if (print) { + eq::EqClassIterator eqc2_i = eq::EqClassIterator( eqc, &d_equalityEngine ); + Trace("strings-eqc") << "Eqc( " << eqc << " ) : "; + while( !eqc2_i.isFinished() ) { + if( (*eqc2_i)!=eqc ){ + Trace("strings-eqc") << (*eqc2_i) << " "; + } + ++eqc2_i; + } + Trace("strings-eqc") << std::endl; + } + ++eqcs2_i; + } + Trace("strings-eqc") << std::endl; + } + Trace("strings-eqc") << std::endl; + for( NodeListMap::const_iterator it = d_nf_pairs.begin(); it != d_nf_pairs.end(); ++it ){ + NodeList* lst = (*it).second; + NodeList::const_iterator it2 = lst->begin(); + Trace("strings-nf") << (*it).first << " has been unified with "; + while( it2!=lst->end() ){ + Trace("strings-nf") << (*it2); + ++it2; + } + Trace("strings-nf") << std::endl; + } + Trace("strings-nf") << std::endl; + Trace("strings-nf") << "Current inductive equations : " << std::endl; + for( NodeListMap::const_iterator it = d_ind_map1.begin(); it != d_ind_map1.end(); ++it ){ + Node x = (*it).first; + NodeList* lst1 = (*it).second; + NodeList* lst2 = (*d_ind_map2.find(x)).second; + NodeList::const_iterator i1 = lst1->begin(); + NodeList::const_iterator i2 = lst2->begin(); + while( i1!=lst1->end() ){ + Node y = *i1; + Node z = *i2; + Trace("strings-nf") << "Inductive equation : " << x << " = ( " << y << " ++ " << z << " ) * " << y << std::endl; + ++i1; + ++i2; + } + } + + bool addedFact; + do { + Trace("strings-process") << "Check Normal Forms........next round" << std::endl; + //calculate normal forms for each equivalence class, possibly adding splitting lemmas + d_normal_forms.clear(); + d_normal_forms_exp.clear(); + std::map< Node, Node > nf_to_eqc; + std::map< Node, Node > eqc_to_exp; + d_lemma_cache.clear(); + d_pending_req_phase.clear(); + //get equivalence classes + std::vector< Node > eqcs; + getEquivalenceClasses( eqcs ); + for( unsigned i=0; i<eqcs.size(); i++ ){ + Node eqc = eqcs[i]; + Trace("strings-process") << "- Verify normal forms are the same for " << eqc << std::endl; + std::vector< Node > visited; + std::vector< Node > nf; + std::vector< Node > nf_exp; + normalizeEquivalenceClass(eqc, visited, nf, nf_exp); + if( d_conflict ){ + return true; + }else if ( d_pending.empty() && d_lemma_cache.empty() ){ + Node nf_term; + if( nf.size()==0 ){ + nf_term = d_emptyString; + }else if( nf.size()==1 ) { + nf_term = nf[0]; + } else { + nf_term = NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, nf ); + } + nf_term = Rewriter::rewrite( nf_term ); + Trace("strings-debug") << "Make nf_term_exp..." << std::endl; + Node nf_term_exp = nf_exp.empty() ? d_true : + nf_exp.size()==1 ? nf_exp[0] : NodeManager::currentNM()->mkNode( kind::AND, nf_exp ); + if( nf_to_eqc.find(nf_term)!=nf_to_eqc.end() ){ + //Trace("strings-debug") << "Merge because of normal form : " << eqc << " and " << nf_to_eqc[nf_term] << " both have normal form " << nf_term << std::endl; + //two equivalence classes have same normal form, merge + Node eq_exp = NodeManager::currentNM()->mkNode( kind::AND, nf_term_exp, eqc_to_exp[nf_to_eqc[nf_term]] ); + Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, eqc, nf_to_eqc[nf_term] ); + Trace("strings-lemma") << "Strings (by normal forms) : Infer " << eq << " from " << eq_exp << std::endl; + //d_equalityEngine.assertEquality( eq, true, eq_exp ); + d_pending.push_back( eq ); + d_pending_exp[eq] = eq_exp; + d_infer.push_back(eq); + d_infer_exp.push_back(eq_exp); + }else{ + nf_to_eqc[nf_term] = eqc; + eqc_to_exp[eqc] = nf_term_exp; + } + } + Trace("strings-process") << "Done verifying normal forms are the same for " << eqc << std::endl; + } + + Trace("strings-nf-debug") << "**** Normal forms are : " << std::endl; + for( std::map< Node, Node >::iterator it = nf_to_eqc.begin(); it != nf_to_eqc.end(); ++it ){ + Trace("strings-nf-debug") << " normal_form(" << it->second << ") = " << it->first << std::endl; + } + Trace("strings-nf-debug") << std::endl; + addedFact = !d_pending.empty(); + doPendingFacts(); + } while ( !d_conflict && d_lemma_cache.empty() && addedFact ); + + + //process disequalities between equivalence classes + if( !d_conflict && d_lemma_cache.empty() ){ + std::vector< Node > eqcs; + getEquivalenceClasses( eqcs ); + std::vector< std::vector< Node > > cols; + std::vector< Node > lts; + seperateByLength( eqcs, cols, lts ); + for( unsigned i=0; i<cols.size(); i++ ){ + if( cols[i].size()>1 && d_lemma_cache.empty() ){ + Trace("strings-solve") << "- Verify disequalities are processed for "; + printConcat( d_normal_forms[cols[i][0]], "strings-solve" ); + Trace("strings-solve") << "..." << std::endl; + //must ensure that normal forms are disequal + for( unsigned j=1; j<cols[i].size(); j++ ){ + if( !d_equalityEngine.areDisequal( cols[i][0], cols[i][j], false ) ){ + sendSplit( cols[i][0], cols[i][j], "Disequality Normalization" ); + break; + }else{ + Trace("strings-solve") << " against "; + printConcat( d_normal_forms[cols[i][j]], "strings-solve" ); + Trace("strings-solve") << "..." << std::endl; + if( normalizeDisequality( cols[i][0], cols[i][j] ) ){ + break; + } + } + } + } + } + } + + //flush pending lemmas + if( !d_conflict && !d_lemma_cache.empty() ){ + doPendingLemmas(); + return true; + }else{ + return false; + } +} + +bool TheoryStrings::checkCardinality() { + int cardinality = options::stringCharCardinality(); + Trace("strings-solve-debug2") << "get cardinality: " << cardinality << endl; + + std::vector< Node > eqcs; + getEquivalenceClasses( eqcs ); + + std::vector< std::vector< Node > > cols; + std::vector< Node > lts; + seperateByLength( eqcs, cols, lts ); + + for( unsigned i = 0; i<cols.size(); ++i ){ + Node lr = lts[i]; + Trace("string-cardinality") << "Number of strings with length equal to " << lr << " is " << cols[i].size() << std::endl; + // size > c^k + double k = std::log( cols[i].size() ) / log((double) cardinality); + unsigned int int_k = (unsigned int)k; + Node k_node = NodeManager::currentNM()->mkConst( ::CVC4::Rational( int_k ) ); + //double c_k = pow ( (double)cardinality, (double)lr ); + if( cols[i].size() > 1 ) { + bool allDisequal = true; + for( std::vector< Node >::iterator itr1 = cols[i].begin(); + itr1 != cols[i].end(); ++itr1) { + for( std::vector< Node >::iterator itr2 = itr1 + 1; + itr2 != cols[i].end(); ++itr2) { + if(!d_equalityEngine.areDisequal( *itr1, *itr2, false )) { + allDisequal = false; + // add split lemma + sendSplit( *itr1, *itr2, "Cardinality" ); + doPendingLemmas(); + return true; + } + } + } + if(allDisequal) { + EqcInfo* ei = getOrMakeEqcInfo( lr, true ); + Trace("string-cardinality") << "Previous cardinality used for " << lr << " is " << ((int)ei->d_cardinality_lem_k.get()-1) << std::endl; + if( int_k+1 > ei->d_cardinality_lem_k.get() ){ + //add cardinality lemma + Node dist = NodeManager::currentNM()->mkNode( kind::DISTINCT, cols[i] ); + std::vector< Node > vec_node; + vec_node.push_back( dist ); + for( std::vector< Node >::iterator itr1 = cols[i].begin(); + itr1 != cols[i].end(); ++itr1) { + Node len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, *itr1 ); + if( len!=lr ){ + Node len_eq_lr = NodeManager::currentNM()->mkNode( kind::EQUAL, lr, len ); + vec_node.push_back( len_eq_lr ); + } + } + Node antc = NodeManager::currentNM()->mkNode( kind::AND, vec_node ); + Node len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, cols[i][0] ); + Node cons = NodeManager::currentNM()->mkNode( kind::GT, len, k_node ); + /* + sendLemma( antc, cons, "Cardinality" ); + ei->d_cardinality_lem_k.set( int_k+1 ); + if( !d_lemma_cache.empty() ){ + doPendingLemmas(); + return true; + } + */ + Node lemma = NodeManager::currentNM()->mkNode( kind::IMPLIES, antc, cons ); + lemma = Rewriter::rewrite( lemma ); + ei->d_cardinality_lem_k.set( int_k+1 ); + if( lemma!=d_true ){ + Trace("strings-lemma") << "Strings cardinality lemma : " << lemma << std::endl; + d_out->lemma(lemma); + return true; + } + } + } + } + } + return false; +} + +int TheoryStrings::gcd ( int a, int b ) { + int c; + while ( a != 0 ) { + c = a; a = b%a; b = c; + } + return b; +} + +bool TheoryStrings::checkInductiveEquations() { + bool hasEq = false; + if(d_ind_map1.size() != 0){ + Trace("strings-ind") << "We are sat, with these inductive equations : " << std::endl; + for( NodeListMap::const_iterator it = d_ind_map1.begin(); it != d_ind_map1.end(); ++it ){ + Node x = (*it).first; + Trace("strings-ind-debug") << "Check eq for " << x << std::endl; + 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::const_iterator i1 = lst1->begin(); + NodeList::const_iterator i2 = lst2->begin(); + NodeList::const_iterator ie = lste->begin(); + //NodeList::const_iterator il = lstl->begin(); + while( i1!=lst1->end() ){ + Node y = *i1; + Node z = *i2; + //Trace("strings-ind-debug") << "Check y=" << y << " , z=" << z << std::endl; + //if( il==lstl->end() ) { + std::vector< Node > nf_y, nf_z, exp_y, exp_z; + + //getFinalNormalForm( y, nf_y, exp_y); + //getFinalNormalForm( z, nf_z, exp_z); + //std::vector< Node > vec_empty; + //Node nexp_y = mkExplain( exp_y, vec_empty ); + //Trace("strings-ind-debug") << "Check nexp_y=" << nexp_y << std::endl; + //Node nexp_z = mkExplain( exp_z, vec_empty ); + + //Node exp = *ie; + //Trace("strings-ind-debug") << "Check exp=" << exp << std::endl; + + //exp = NodeManager::currentNM()->mkNode( kind::AND, exp, nexp_y, nexp_z ); + //exp = Rewriter::rewrite( exp ); + + Trace("strings-ind") << "Inductive equation : " << x << " = ( " << y << " ++ " << z << " )* " << y << std::endl; + /* + for( std::vector< Node >::const_iterator itr = nf_y.begin(); itr != nf_y.end(); ++itr) { + Trace("strings-ind") << (*itr) << " "; + } + Trace("strings-ind") << " ++ "; + for( std::vector< Node >::const_iterator itr = nf_z.begin(); itr != nf_z.end(); ++itr) { + Trace("strings-ind") << (*itr) << " "; + } + Trace("strings-ind") << " )* "; + for( std::vector< Node >::const_iterator itr = nf_y.begin(); itr != nf_y.end(); ++itr) { + Trace("strings-ind") << (*itr) << " "; + } + Trace("strings-ind") << std::endl; + */ + /* + Trace("strings-ind") << "Explanation is : " << exp << std::endl; + std::vector< Node > nf_yz; + nf_yz.insert( nf_yz.end(), nf_y.begin(), nf_y.end() ); + nf_yz.insert( nf_yz.end(), nf_z.begin(), nf_z.end() ); + std::vector< std::vector< Node > > cols; + std::vector< Node > lts; + seperateByLength( nf_yz, cols, lts ); + Trace("strings-ind") << "This can be grouped into collections : " << std::endl; + for( unsigned j=0; j<cols.size(); j++ ){ + Trace("strings-ind") << " : "; + for( unsigned k=0; k<cols[j].size(); k++ ){ + Trace("strings-ind") << cols[j][k] << " "; + } + Trace("strings-ind") << std::endl; + } + Trace("strings-ind") << std::endl; + + Trace("strings-ind") << "Add length lemma..." << std::endl; + std::vector< int > co; + co.push_back(0); + for(unsigned int k=0; k<lts.size(); ++k) { + if(lts[k].isConst() && lts[k].getType().isInteger()) { + int len = lts[k].getConst<Rational>().getNumerator().toUnsignedInt(); + co[0] += cols[k].size() * len; + } else { + co.push_back( cols[k].size() ); + } + } + int g_co = co[0]; + for(unsigned k=1; k<co.size(); ++k) { + g_co = gcd(g_co, co[k]); + } + Node lemma_len; + // both constants + Node len_x = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, x ); + Node sk = NodeManager::currentNM()->mkSkolem( "argsym_$$", NodeManager::currentNM()->integerType(), "created for length inductive lemma" ); + Node g_co_node = NodeManager::currentNM()->mkConst( CVC4::Rational(g_co) ); + Node sk_m_gcd = NodeManager::currentNM()->mkNode( kind::MULT, g_co_node, sk ); + Node len_y = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, y ); + Node sk_m_g_p_y = NodeManager::currentNM()->mkNode( kind::PLUS, sk_m_gcd, len_y ); + lemma_len = NodeManager::currentNM()->mkNode( kind::EQUAL, sk_m_g_p_y, len_x ); + //Node sk_geq_zero = NodeManager::currentNM()->mkNode( kind::GEQ, sk, d_zero ); + //lemma_len = NodeManager::currentNM()->mkNode( kind::AND, lemma_len, sk_geq_zero ); + lemma_len = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, lemma_len ); + Trace("strings-lemma") << "Strings: Add lemma " << lemma_len << std::endl; + d_out->lemma(lemma_len); + lstl->push_back( d_true ); + return true;*/ + //} + ++i1; + ++i2; + ++ie; + //++il; + if( !d_equalityEngine.hasTerm( d_emptyString ) || !d_equalityEngine.areEqual( y, d_emptyString ) || !d_equalityEngine.areEqual( x, d_emptyString ) ){ + hasEq = true; + } + } + } + } + if( hasEq ){ + Trace("strings-ind") << "It is incomplete." << std::endl; + d_out->setIncomplete(); + }else{ + Trace("strings-ind") << "We can answer SAT." << std::endl; + } + return false; +} + +void TheoryStrings::getEquivalenceClasses( std::vector< Node >& eqcs ) { + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); + while( !eqcs_i.isFinished() ) { + Node eqc = (*eqcs_i); + //if eqc.getType is string + if (eqc.getType().isString()) { + eqcs.push_back( eqc ); + } + ++eqcs_i; + } +} + +void TheoryStrings::getFinalNormalForm( Node n, std::vector< Node >& nf, std::vector< Node >& exp ) { + if( n!=d_emptyString ){ + if( n.getKind()==kind::STRING_CONCAT ){ + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + getFinalNormalForm( n[i], nf, exp ); + } + }else{ + Trace("strings-debug") << "Get final normal form " << n << std::endl; + Assert( d_equalityEngine.hasTerm( n ) ); + Node nr = d_equalityEngine.getRepresentative( n ); + EqcInfo *eqc_n = getOrMakeEqcInfo( nr, false ); + Node nc = eqc_n ? eqc_n->d_const_term.get() : Node::null(); + if( !nc.isNull() ){ + nf.push_back( nc ); + if( n!=nc ){ + exp.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, n, nc ) ); + } + }else{ + Assert( d_normal_forms.find( nr )!=d_normal_forms.end() ); + if( d_normal_forms[nr][0]==nr ){ + Assert( d_normal_forms[nr].size()==1 ); + nf.push_back( nr ); + if( n!=nr ){ + exp.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, n, nr ) ); + } + }else{ + for( unsigned i=0; i<d_normal_forms[nr].size(); i++ ){ + Assert( d_normal_forms[nr][i]!=nr ); + getFinalNormalForm( d_normal_forms[nr][i], nf, exp ); + } + exp.insert( exp.end(), d_normal_forms_exp[nr].begin(), d_normal_forms_exp[nr].end() ); + } + } + Trace("strings-ind-nf") << "The final normal form of " << n << " is " << nf << std::endl; + } + } +} + +void TheoryStrings::seperateByLength( std::vector< Node >& n, std::vector< std::vector< Node > >& cols, + std::vector< Node >& lts ) { + unsigned leqc_counter = 0; + std::map< Node, unsigned > eqc_to_leqc; + std::map< unsigned, Node > leqc_to_eqc; + std::map< unsigned, std::vector< Node > > eqc_to_strings; + for( unsigned i=0; i<n.size(); i++ ){ + Node eqc = n[i]; + Assert( d_equalityEngine.getRepresentative(eqc)==eqc ); + EqcInfo* ei = getOrMakeEqcInfo( eqc, false ); + Node lt = ei ? ei->d_length_term : Node::null(); + if( !lt.isNull() ){ + lt = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, lt ); + Node r = d_equalityEngine.getRepresentative( lt ); + if( eqc_to_leqc.find( r )==eqc_to_leqc.end() ){ + eqc_to_leqc[r] = leqc_counter; + leqc_to_eqc[leqc_counter] = r; + leqc_counter++; + } + eqc_to_strings[ eqc_to_leqc[r] ].push_back( eqc ); + }else{ + eqc_to_strings[leqc_counter].push_back( eqc ); + leqc_counter++; + } + } + for( std::map< unsigned, std::vector< Node > >::iterator it = eqc_to_strings.begin(); it != eqc_to_strings.end(); ++it ){ + std::vector< Node > vec; + vec.insert( vec.end(), it->second.begin(), it->second.end() ); + lts.push_back( leqc_to_eqc[it->first] ); + cols.push_back( vec ); + } +} + +void TheoryStrings::printConcat( std::vector< Node >& n, const char * c ) { + for( unsigned i=0; i<n.size(); i++ ){ + if( i>0 ) Trace(c) << " ++ "; + Trace(c) << n[i]; + } +} + +/* +Node TheoryStrings::getNextDecisionRequest() { + if( d_lit_to_decide_index.get()<d_lit_to_decide.size() ){ + Node l = d_lit_to_decide[d_lit_to_decide_index.get()]; + d_lit_to_decide_index.set( d_lit_to_decide_index.get() + 1 ); + Trace("strings-ind") << "Strings-ind : decide on " << l << std::endl; + return l; + }else{ + return Node::null(); + } +} +*/ +}/* CVC4::theory::strings namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ |