--- /dev/null
+/********************* */
+/*! \file anti_skolem.cpp
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 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 anti-skolemization
+ ** ( forall x. P[ f( x ) ] ^ forall x. Q[ f( x ) ] ) => forall x. exists y. ( P[ y ] ^ Q[ y ] )
+ **/
+
+#include "theory/quantifiers/anti_skolem.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "options/quantifiers_options.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+
+
+struct sortTypeOrder {
+ TermDb* d_tdb;
+ bool operator() (TypeNode i, TypeNode j) {
+ return d_tdb->getIdForType( i )<d_tdb->getIdForType( j );
+ }
+};
+
+void QuantAntiSkolem::SkQuantTypeCache::add( std::vector< TypeNode >& typs, Node q, unsigned index ) {
+ if( index==typs.size() ){
+ Assert( std::find( d_quants.begin(), d_quants.end(), q )==d_quants.end() );
+ d_quants.push_back( q );
+ }else{
+ d_children[typs[index]].add( typs, q, index+1 );
+ }
+}
+
+void QuantAntiSkolem::SkQuantTypeCache::sendLemmas( QuantAntiSkolem * ask ) {
+ for( std::map< TypeNode, SkQuantTypeCache >::iterator it = d_children.begin(); it != d_children.end(); ++it ){
+ it->second.sendLemmas( ask );
+ }
+ if( !d_quants.empty() ){
+ ask->sendAntiSkolemizeLemma( d_quants );
+ }
+}
+
+bool QuantAntiSkolem::CDSkQuantCache::add( context::Context* c, std::vector< Node >& quants, unsigned index ) {
+ if( index==quants.size() ){
+ if( !d_valid.get() ){
+ d_valid.set( true );
+ return true;
+ }else{
+ return false;
+ }
+ }else{
+ Node n = quants[index];
+ std::map< Node, CDSkQuantCache* >::iterator it = d_data.find( n );
+ CDSkQuantCache* skc;
+ if( it==d_data.end() ){
+ skc = new CDSkQuantCache( c );
+ d_data[n] = skc;
+ }else{
+ skc = it->second;
+ }
+ return skc->add( c, quants, index+1 );
+ }
+}
+
+QuantAntiSkolem::QuantAntiSkolem( QuantifiersEngine * qe ) : QuantifiersModule( qe ){
+ d_sqc = new CDSkQuantCache( qe->getUserContext() );
+}
+
+/* Call during quantifier engine's check */
+void QuantAntiSkolem::check( Theory::Effort e, unsigned quant_e ) {
+ if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){
+ d_sqtc.clear();
+ for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+ Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
+ if( d_quant_processed.find( q )==d_quant_processed.end() ){
+ d_quant_processed[q] = true;
+ Trace("anti-sk") << "Process quantified formula : " << q << std::endl;
+ bool success = false;
+ if( d_quant_sip[q].init( q[1] ) ){
+ Trace("anti-sk") << "- Partitioned to single invocation parts : " << std::endl;
+ d_quant_sip[q].debugPrint( "anti-sk" );
+ //check if it is single invocation
+ if( d_quant_sip[q].isPurelySingleInvocation() ){
+ //for now, only do purely single invocation
+ success = true;
+ }
+ }else{
+ Trace("anti-sk") << "- Failed to initialize." << std::endl;
+ }
+ if( success ){
+ //sort the argument variables
+ d_ask_types[q].insert( d_ask_types[q].end(), d_quant_sip[q].d_arg_types.begin(), d_quant_sip[q].d_arg_types.end() );
+ std::map< TypeNode, std::vector< unsigned > > indices;
+ for( unsigned j=0; j<d_ask_types[q].size(); j++ ){
+ indices[d_ask_types[q][j]].push_back( j );
+ }
+ sortTypeOrder sto;
+ sto.d_tdb = d_quantEngine->getTermDatabase();
+ std::sort( d_ask_types[q].begin(), d_ask_types[q].end(), sto );
+ //increment j on inner loop
+ for( unsigned j=0; j<d_ask_types[q].size(); ){
+ TypeNode curr = d_ask_types[q][j];
+ for( unsigned k=0; k<indices[curr].size(); k++ ){
+ Assert( d_ask_types[q][j]==curr );
+ d_ask_types_index[q].push_back( indices[curr][k] );
+ j++;
+ }
+ }
+ Assert( d_ask_types_index[q].size()==d_ask_types[q].size() );
+ }else{
+ d_quant_sip.erase( q );
+ }
+ }
+ //now, activate the quantified formula
+ std::map< Node, std::vector< TypeNode > >::iterator it = d_ask_types.find( q );
+ if( it!=d_ask_types.end() ){
+ d_sqtc.add( it->second, q );
+ }
+ }
+ Trace("anti-sk-debug") << "Process lemmas..." << std::endl;
+ //send out lemmas for each anti-skolemizable group of quantified formulas
+ d_sqtc.sendLemmas( this );
+ Trace("anti-sk-debug") << "...Finished process lemmas" << std::endl;
+ }
+}
+
+bool QuantAntiSkolem::sendAntiSkolemizeLemma( std::vector< Node >& quants, bool pconnected ) {
+ Assert( !quants.empty() );
+ std::sort( quants.begin(), quants.end() );
+ if( d_sqc->add( d_quantEngine->getUserContext(), quants ) ){
+ //partition into connected components
+ if( pconnected && quants.size()>1 ){
+ Trace("anti-sk-debug") << "Partition into connected components..." << std::endl;
+ int eqc_count = 0;
+ std::map< Node, int > func_to_eqc;
+ std::map< int, std::vector< Node > > eqc_to_func;
+ std::map< int, std::vector< Node > > eqc_to_quant;
+ for( unsigned i=0; i<quants.size(); i++ ){
+ Node q = quants[i];
+ std::vector< int > eqcs;
+ for( std::map< Node, bool >::iterator it = d_quant_sip[q].d_funcs.begin(); it != d_quant_sip[q].d_funcs.end(); ++it ){
+ Node f = it->first;
+ std::map< Node, int >::iterator itf = func_to_eqc.find( f );
+ if( itf == func_to_eqc.end() ){
+ if( eqcs.empty() ){
+ func_to_eqc[f] = eqc_count;
+ eqc_to_func[eqc_count].push_back( f );
+ eqc_count++;
+ }else{
+ func_to_eqc[f] = eqcs[0];
+ eqc_to_func[eqcs[0]].push_back( f );
+ }
+ }
+ if( std::find( eqcs.begin(), eqcs.end(), func_to_eqc[f] )==eqcs.end() ){
+ eqcs.push_back( func_to_eqc[f] );
+ }
+ }
+ Assert( !eqcs.empty() );
+ //merge equivalence classes
+ int id = eqcs[0];
+ eqc_to_quant[id].push_back( q );
+ for( unsigned j=1; j<eqcs.size(); j++ ){
+ int id2 = eqcs[j];
+ std::map< int, std::vector< Node > >::iterator itef = eqc_to_func.find( id2 );
+ if( itef!=eqc_to_func.end() ){
+ for( unsigned k=0; k<itef->second.size(); k++ ){
+ func_to_eqc[itef->second[k]] = id;
+ eqc_to_func[id].push_back( itef->second[k] );
+ }
+ eqc_to_func.erase( id2 );
+ }
+ itef = eqc_to_quant.find( id2 );
+ if( itef!=eqc_to_quant.end() ){
+ eqc_to_quant[id].insert( eqc_to_quant[id].end(), itef->second.begin(), itef->second.end() );
+ eqc_to_quant.erase( id2 );
+ }
+ }
+ }
+ if( eqc_to_quant.size()>1 ){
+ bool addedLemma = false;
+ for( std::map< int, std::vector< Node > >::iterator it = eqc_to_quant.begin(); it != eqc_to_quant.end(); ++it ){
+ Assert( it->second.size()<quants.size() );
+ bool ret = sendAntiSkolemizeLemma( it->second, false );
+ addedLemma = addedLemma || ret;
+ }
+ return addedLemma;
+ }
+ }
+
+ Trace("anti-sk") << "Anti-skolemize group : " << std::endl;
+ for( unsigned i=0; i<quants.size(); i++ ){
+ Trace("anti-sk") << " " << quants[i] << std::endl;
+ }
+
+ std::vector< Node > outer_vars;
+ std::vector< Node > inner_vars;
+ Node q = quants[0];
+ for( unsigned i=0; i<d_ask_types[q].size(); i++ ){
+ Node v = NodeManager::currentNM()->mkBoundVar( d_ask_types[q][i] );
+ Trace("anti-sk-debug") << "Outer var " << i << " : " << v << std::endl;
+ outer_vars.push_back( v );
+ }
+
+ std::map< Node, Node > func_to_var;
+ std::vector< Node > conj;
+ for( unsigned i=0; i<quants.size(); i++ ){
+ Node q = quants[i];
+ Trace("anti-sk-debug") << "Process " << q << std::endl;
+ std::vector< Node > subs_lhs;
+ std::vector< Node > subs_rhs;
+ //get outer variable substitution
+ Assert( d_ask_types_index[q].size()==d_ask_types[q].size() );
+ for( unsigned j=0; j<d_ask_types_index[q].size(); j++ ){
+ Trace("anti-sk-debug") << " o_subs : " << d_quant_sip[q].d_si_vars[d_ask_types_index[q][j]] << " -> " << outer_vars[j] << std::endl;
+ subs_lhs.push_back( d_quant_sip[q].d_si_vars[d_ask_types_index[q][j]] );
+ subs_rhs.push_back( outer_vars[j] );
+ }
+ //get function substitution
+ for( std::map< Node, bool >::iterator it = d_quant_sip[q].d_funcs.begin(); it != d_quant_sip[q].d_funcs.end(); ++it ){
+ Node f = it->first;
+ Node fv = d_quant_sip[q].d_func_fo_var[it->first];
+ if( func_to_var.find( f )==func_to_var.end() ){
+ Node v = NodeManager::currentNM()->mkBoundVar( fv.getType() );
+ Trace("anti-sk-debug") << "Inner var for " << f << " : " << v << std::endl;
+ inner_vars.push_back( v );
+ func_to_var[f] = v;
+ }
+ subs_lhs.push_back( fv );
+ subs_rhs.push_back( func_to_var[f] );
+ Trace("anti-sk-debug") << " i_subs : " << fv << " -> " << func_to_var[f] << std::endl;
+ }
+ Node c = d_quant_sip[q].getSingleInvocation();
+ if( !subs_lhs.empty() ){
+ c = c.substitute( subs_lhs.begin(), subs_lhs.end(), subs_rhs.begin(), subs_rhs.end() );
+ }
+ conj.push_back( c );
+ }
+ Node body = conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( kind::AND, conj );
+ if( !inner_vars.empty() ){
+ Node bvl = NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, inner_vars );
+ body = NodeManager::currentNM()->mkNode( kind::EXISTS, bvl, body );
+ }
+ if( !outer_vars.empty() ){
+ Node bvl = NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, outer_vars );
+ body = NodeManager::currentNM()->mkNode( kind::FORALL, bvl, body );
+ }
+ Trace("anti-sk") << "Produced : " << body << std::endl;
+ quants.push_back( body.negate() );
+ Node lem = NodeManager::currentNM()->mkNode( kind::AND, quants ).negate();
+ Trace("anti-sk-lemma") << "Anti-skolemize lemma : " << lem << std::endl;
+ quants.pop_back();
+ return d_quantEngine->addLemma( lem );
+ }else{
+ return false;
+ }
+}
+
std::vector< std::vector< Node > > normal_forms;
// explanation for each normal form (phi)
std::vector< std::vector< Node > > normal_forms_exp;
+ // dependency information
+ std::vector< std::map< Node, std::map< bool, int > > > normal_forms_exp_depend;
// record terms for each normal form (t)
std::vector< Node > normal_form_src;
//Get Normal Forms
- result = getNormalForms(eqc, nf, normal_forms, normal_forms_exp, normal_form_src);
+ result = getNormalForms(eqc, normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend);
if( hasProcessed() ){
- return true;
+ return true;
}else if( result ){
- if( processNEqc(normal_forms, normal_forms_exp, normal_form_src) ){
+ if( processNEqc(normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend) ){
return true;
}
}
if( normal_forms.empty() ){
Trace("strings-solve-debug2") << "construct the normal form" << std::endl;
getConcatVec( eqc, nf );
+ d_normal_forms_base[eqc] = 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( eqc.eqNode( normal_form_src[0] ) );
+ int nf_index = 0;
+ //nf.insert( nf.end(), normal_forms[nf_index].begin(), normal_forms[nf_index].end() );
+ //nf_exp.insert( nf_exp.end(), normal_forms_exp[nf_index].begin(), normal_forms_exp[nf_index].end() );
+ //Trace("strings-solve-debug2") << "take normal form ... done" << std::endl;
+ //d_normal_forms_base[eqc] = normal_form_src[nf_index];
+ ///*
+ std::vector< Node >::iterator itn = std::find( normal_form_src.begin(), normal_form_src.end(), eqc );
+ if( itn!=normal_form_src.end() ){
+ nf_index = itn - normal_form_src.begin();
+ Trace("strings-solve-debug2") << "take normal form " << nf_index << std::endl;
+ Assert( normal_form_src[nf_index]==eqc );
+ }else{
+ //just take the first normal form
+ Trace("strings-solve-debug2") << "take the first normal form" << std::endl;
}
- Trace("strings-solve-debug2") << "just take the first normal form ... done" << std::endl;
+ nf.insert( nf.end(), normal_forms[nf_index].begin(), normal_forms[nf_index].end() );
+ nf_exp.insert( nf_exp.end(), normal_forms_exp[nf_index].begin(), normal_forms_exp[nf_index].end() );
+ //if( eqc!=normal_form_src[nf_index] ){
+ // nf_exp.push_back( eqc.eqNode( normal_form_src[nf_index] ) );
+ //}
+ Trace("strings-solve-debug2") << "take normal form ... done" << std::endl;
+ d_normal_forms_base[eqc] = normal_form_src[nf_index];
+ //*/
}
- d_normal_forms_base[eqc] = normal_form_src.empty() ? eqc : normal_form_src[0];
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-debug") << "Return process equivalence class " << eqc << " : returned, size = " << nf.size() << std::endl;
}
}
-bool TheoryStrings::getNormalForms( Node &eqc, 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) {
+bool TheoryStrings::getNormalForms( Node &eqc, std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src,
+ std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend ) {
Trace("strings-process-debug") << "Get normal forms " << eqc << std::endl;
eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
while( !eqc_i.isFinished() ){
if( d_congruent.find( n )==d_congruent.end() ){
if( n.getKind() == kind::CONST_STRING || n.getKind() == kind::STRING_CONCAT ){
Trace("strings-process-debug") << "Get Normal Form : Process term " << n << " in eqc " << eqc << std::endl;
- std::vector<Node> nf_n;
- std::vector<Node> nf_exp_n;
+ std::vector< Node > nf_n;
+ std::vector< Node > nf_exp_n;
+ std::map< Node, std::map< bool, int > > nf_exp_depend_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-debug") << "Normalizing subterm " << n[i] << " = " << nr << std::endl;
Assert( d_normal_forms.find( nr )!=d_normal_forms.end() );
- nf_temp.insert( nf_temp.end(), d_normal_forms[nr].begin(), d_normal_forms[nr].end() );
- nf_exp_temp.insert( nf_exp_temp.end(), d_normal_forms_exp[nr].begin(), d_normal_forms_exp[nr].end() );
+ unsigned orig_size = nf_n.size();
+ unsigned add_size = d_normal_forms[nr].size();
//if not the empty string, add to current normal form
- if( nf.size()!=1 || nf[0]!=d_emptyString ){
- for( unsigned r=0; r<nf_temp.size(); r++ ) {
+ if( !d_normal_forms[nr].empty() ){
+ for( unsigned r=0; r<d_normal_forms[nr].size(); r++ ) {
if( Trace.isOn("strings-error") ) {
- if( nf_temp[r].getKind()==kind::STRING_CONCAT ){
+ if( d_normal_forms[nr][r].getKind()==kind::STRING_CONCAT ){
Trace("strings-error") << "Strings::Error: From eqc = " << eqc << ", " << n << " index " << i << ", bad normal form : ";
- for( unsigned rr=0; rr<nf_temp.size(); rr++ ) {
- Trace("strings-error") << nf_temp[rr] << " ";
+ for( unsigned rr=0; rr<d_normal_forms[nr].size(); rr++ ) {
+ Trace("strings-error") << d_normal_forms[nr][rr] << " ";
}
Trace("strings-error") << std::endl;
}
}
- Assert( nf_temp[r].getKind()!=kind::STRING_CONCAT );
+ Assert( d_normal_forms[nr][r].getKind()!=kind::STRING_CONCAT );
+ }
+ nf_n.insert( nf_n.end(), d_normal_forms[nr].begin(), d_normal_forms[nr].end() );
+ }
+
+ for( unsigned j=0; j<d_normal_forms_exp[nr].size(); j++ ){
+ Node exp = d_normal_forms_exp[nr][j];
+ nf_exp_n.push_back( exp );
+ //track depends
+ for( unsigned k=0; k<2; k++ ){
+ int prev_dep = d_normal_forms_exp_depend[nr][exp][k==1];
+ if( k==0 ){
+ nf_exp_depend_n[exp][false] = orig_size + prev_dep;
+ }else if( k==1 ){
+ //store forward index (restored to reverse index below)
+ nf_exp_depend_n[exp][true] = orig_size + ( add_size - prev_dep );
+ }
}
- 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( n[i].eqNode( nr ) );
+ Node eq = n[i].eqNode( nr );
+ nf_exp_n.push_back( eq );
+ //track depends
+ nf_exp_depend_n[eq][false] = orig_size;
+ nf_exp_depend_n[eq][true] = orig_size + add_size;
}
}
+ //convert forward indices to reverse indices
+ int total_size = nf_n.size();
+ for( std::map< Node, std::map< bool, int > >::iterator it = nf_exp_depend_n.begin(); it != nf_exp_depend_n.end(); ++it ){
+ it->second[true] = total_size - it->second[true];
+ Assert( it->second[true]>=0 );
+ }
}
//if not equal to self
if( nf_n.size()>1 || ( nf_n.size()==1 && nf_n[0].getKind()==kind::CONST_STRING ) ){
}
}
normal_forms.push_back(nf_n);
- normal_forms_exp.push_back(nf_exp_n);
normal_form_src.push_back(n);
+ normal_forms_exp.push_back(nf_exp_n);
+ normal_forms_exp_depend.push_back(nf_exp_depend_n);
}else{
//this was redundant: combination of self + empty string(s)
Node nn = nf_n.size()==0 ? d_emptyString : nf_n[0];
}
Trace("strings-solve") << normal_forms_exp[i][j];
}
+ Trace("strings-solve") << std::endl;
+ Trace("strings-solve") << "WITH DEPENDENCIES : " << std::endl;
+ for( unsigned j=0; j<normal_forms_exp[i].size(); j++ ) {
+ Trace("strings-solve") << " " << normal_forms_exp[i][j] << " -> ";
+ Trace("strings-solve") << normal_forms_exp_depend[i][normal_forms_exp[i][j]][false] << ",";
+ Trace("strings-solve") << normal_forms_exp_depend[i][normal_forms_exp[i][j]][true] << std::endl;
+ }
}
Trace("strings-solve") << std::endl;
+
}
} else {
- //std::vector< Node > nf;
- //nf.push_back( eqc );
- //normal_forms.push_back(nf);
- //std::vector< Node > nf_exp_def;
- //normal_forms_exp.push_back(nf_exp_def);
- //normal_form_src.push_back(eqc);
Trace("strings-solve") << "--- Single normal form for equivalence class " << eqc << std::endl;
}
}
return true;
}
+void TheoryStrings::getExplanationVectorForPrefix( std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src,
+ std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend,
+ unsigned i, unsigned j, int index, bool isRev, std::vector< Node >& curr_exp ) {
+ if( index==-1 || !options::stringMinPrefixExplain() ){
+ 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() );
+ }else{
+ Trace("strings-explain-prefix") << "Get explanation for prefix " << index << " of normal forms " << i << " and " << j << ", reverse = " << isRev << std::endl;
+ for( unsigned r=0; r<2; r++ ){
+ int tindex = r==0 ? i : j;
+ for( unsigned k=0; k<normal_forms_exp[tindex].size(); k++ ){
+ Node exp = normal_forms_exp[tindex][k];
+ int dep = normal_forms_exp_depend[tindex][exp][isRev];
+ if( dep<=index ){
+ curr_exp.push_back( exp );
+ Trace("strings-explain-prefix-debug") << " include : " << exp << std::endl;
+ }else{
+ Trace("strings-explain-prefix-debug") << " exclude : " << exp << std::endl;
+ }
+ }
+ }
+ Trace("strings-explain-prefix") << "Included " << curr_exp.size() << " / " << ( normal_forms_exp[i].size() + normal_forms_exp[j].size() ) << std::endl;
+ }
+ if( normal_form_src[i]!=normal_form_src[j] ){
+ curr_exp.push_back( normal_form_src[i].eqNode( normal_form_src[j] ) );
+ }
+}
-bool TheoryStrings::processNEqc( std::vector< std::vector< Node > > &normal_forms, std::vector< std::vector< Node > > &normal_forms_exp,
- std::vector< Node > &normal_form_src) {
+bool TheoryStrings::processNEqc( std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src,
+ std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend ) {
bool flag_lb = false;
std::vector< Node > c_lb_exp;
- int c_i, c_j, c_loop_n_index, c_other_n_index, c_loop_index, c_index, c_other_index;
+ int c_i, c_j, c_loop_n_index, c_other_n_index, c_loop_index, c_index;
for(unsigned i=0; i<normal_forms.size()-1; i++) {
//unify each normalform[j] with normal_forms[i]
for(unsigned j=i+1; j<normal_forms.size(); j++ ) {
Trace("strings-solve") << "Strings: Process normal form #" << i << " against #" << j << "..." << std::endl;
if( isNormalFormPair( normal_form_src[i], normal_form_src[j] ) ) {
Trace("strings-solve") << "Strings: Already cached." << std::endl;
- } else {
- //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() );
- if( normal_form_src[i]!=normal_form_src[j] ){
- curr_exp.push_back( normal_form_src[i].eqNode( normal_form_src[j] ) );
- }
-
+ }else{
//process the reverse direction first (check for easy conflicts and inferences)
- if( processReverseNEq( normal_forms, normal_form_src, curr_exp, i, j ) ){
+ if( processReverseNEq( normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend, i, j ) ){
return true;
}
//ensure that normal_forms[i] and normal_forms[j] are the same modulo equality
- unsigned index_i = 0;
- unsigned index_j = 0;
+ unsigned index = 0;
bool success;
do{
//simple check
- if( processSimpleNEq( normal_forms, normal_form_src, curr_exp, i, j, index_i, index_j, false ) ){
+ if( processSimpleNEq( normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend, i, j, index, false ) ){
//added a lemma, return
return true;
}
success = false;
//if we are at the end
- if(index_i==normal_forms[i].size() || index_j==normal_forms[j].size() ) {
- Assert( index_i==normal_forms[i].size() && index_j==normal_forms[j].size() );
+ if(index==normal_forms[i].size() || index==normal_forms[j].size() ) {
+ Assert( index==normal_forms[i].size() && index==normal_forms[j].size() );
//we're done
//addNormalFormPair( normal_form_src[i], normal_form_src[j] );
} else {
std::vector< Node > lexp;
- Node length_term_i = getLength( normal_forms[i][index_i], lexp );
- Node length_term_j = getLength( normal_forms[j][index_j], lexp );
+ Node length_term_i = getLength( normal_forms[i][index], lexp );
+ Node length_term_j = getLength( normal_forms[j][index], lexp );
//check length(normal_forms[i][index]) == length(normal_forms[j][index])
if( !areDisequal(length_term_i, length_term_j) && !areEqual(length_term_i, length_term_j) &&
- normal_forms[i][index_i].getKind()!=kind::CONST_STRING && normal_forms[j][index_j].getKind()!=kind::CONST_STRING ) {
+ normal_forms[i][index].getKind()!=kind::CONST_STRING && normal_forms[j][index].getKind()!=kind::CONST_STRING ) {
//length terms are equal, merge equivalence classes if not already done so
Node length_eq = NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j );
Trace("strings-solve-debug") << "Non-simple Case 1 : string lengths neither equal nor disequal" << std::endl;
Trace("strings-solve-debug") << "Non-simple Case 2 : must compare strings" << std::endl;
int loop_in_i = -1;
int loop_in_j = -1;
- if( detectLoop(normal_forms, i, j, index_i, index_j, loop_in_i, loop_in_j) ){
+ if( detectLoop(normal_forms, i, j, index, loop_in_i, loop_in_j) ){
if( !flag_lb ){
c_i = i;
c_j = j;
c_loop_n_index = loop_in_i!=-1 ? i : j;
c_other_n_index = loop_in_i!=-1 ? j : i;
c_loop_index = loop_in_i!=-1 ? loop_in_i : loop_in_j;
- c_index = loop_in_i!=-1 ? index_i : index_j;
- c_other_index = loop_in_i!=-1 ? index_j : index_i;
-
- c_lb_exp = curr_exp;
+ c_index = index;
+
+ getExplanationVectorForPrefix( normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend, i, j, -1, false, c_lb_exp );
if(options::stringLB() == 0) {
flag_lb = true;
} else {
- if(processLoop(c_lb_exp, normal_forms, normal_form_src,
- c_i, c_j, c_loop_n_index, c_other_n_index, c_loop_index, c_index, c_other_index)) {
+ if(processLoop(c_lb_exp, normal_forms, normal_form_src, c_i, c_j, c_loop_n_index, c_other_n_index, c_loop_index, c_index)) {
return true;
}
}
Node conc;
std::vector< Node > antec;
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( normal_forms[i][index].getKind() == kind::CONST_STRING || normal_forms[j][index].getKind() == kind::CONST_STRING) {
+ unsigned const_k = normal_forms[i][index].getKind() == kind::CONST_STRING ? i : j;
+ unsigned nconst_k = normal_forms[i][index].getKind() == kind::CONST_STRING ? j : i;
+ Node const_str = normal_forms[const_k][index];
+ Node other_str = normal_forms[nconst_k][index];
Assert( other_str.getKind()!=kind::CONST_STRING, "Other string is not constant." );
Assert( other_str.getKind()!=kind::STRING_CONCAT, "Other string is not CONCAT." );
if( !d_equalityEngine.areDisequal(other_str, d_emptyString, true) ) {
sendSplit( other_str, d_emptyString, "Len-Split(CST)" );
} else {
Assert(areDisequal(other_str, d_emptyString), "CST Split on empty Var");
- antec.insert( antec.end(), curr_exp.begin(), curr_exp.end() );
+ getExplanationVectorForPrefix( normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend, i, j, index, false, antec );
Node xnz = other_str.eqNode(d_emptyString).negate();
antec.push_back( xnz );
Node conc;
- if( normal_forms[nconst_k].size() > nconst_index_k + 1 && normal_forms[nconst_k][nconst_index_k + 1].isConst() ) {
+ if( normal_forms[nconst_k].size() > index + 1 && normal_forms[nconst_k][index + 1].isConst() ) {
CVC4::String stra = const_str.getConst<String>();
- CVC4::String strb = normal_forms[nconst_k][nconst_index_k + 1].getConst<String>();
+ CVC4::String strb = normal_forms[nconst_k][index + 1].getConst<String>();
CVC4::String stra1 = stra.substr(1);
size_t p = stra.size() - stra1.overlap(strb);
size_t p2 = stra1.find(strb);
return true;
} else {
std::vector< Node > antec_new_lits;
- antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
+ getExplanationVectorForPrefix( normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend, i, j, index, false, antec );
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 ) ){
//x!=e /\ y!=e
for(unsigned xory=0; xory<2; xory++) {
- Node x = xory==0 ? normal_forms[i][index_i] : normal_forms[j][index_j];
+ Node x = xory==0 ? normal_forms[i][index] : normal_forms[j][index];
Node xgtz = x.eqNode( d_emptyString ).negate();
if( d_equalityEngine.areDisequal( x, d_emptyString, true ) ) {
antec.push_back( xgtz );
antec_new_lits.push_back( xgtz );
}
}
- Node sk = mkSkolemCached( normal_forms[i][index_i], normal_forms[j][index_j], sk_id_v_spt, "v_spt", 1 );
- Node eq1 = normal_forms[i][index_i].eqNode( mkConcat(normal_forms[j][index_j], sk) );
- Node eq2 = normal_forms[j][index_j].eqNode( mkConcat(normal_forms[i][index_i], sk) );
+ Node sk = mkSkolemCached( normal_forms[i][index], normal_forms[j][index], sk_id_v_spt, "v_spt", 1 );
+ Node eq1 = normal_forms[i][index].eqNode( mkConcat(normal_forms[j][index], sk) );
+ Node eq2 = normal_forms[j][index].eqNode( mkConcat(normal_forms[i][index], sk) );
if( options::stringCheckEntailLen() ){
//check entailment
for( unsigned e=0; e<2; e++ ){
}
}
if(flag_lb) {
- if(processLoop(c_lb_exp, normal_forms, normal_form_src,
- c_i, c_j, c_loop_n_index, c_other_n_index, c_loop_index, c_index, c_other_index)) {
+ if(processLoop(c_lb_exp, normal_forms, normal_form_src, c_i, c_j, c_loop_n_index, c_other_n_index, c_loop_index, c_index)) {
return true;
}
}
}
bool TheoryStrings::processReverseNEq( std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src,
- std::vector< Node > &curr_exp, unsigned i, unsigned j ) {
+ std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend,
+ unsigned i, unsigned j ) {
//reverse normal form of i, j
std::reverse( normal_forms[i].begin(), normal_forms[i].end() );
std::reverse( normal_forms[j].begin(), normal_forms[j].end() );
- std::vector< Node > t_curr_exp;
- t_curr_exp.insert( t_curr_exp.begin(), curr_exp.begin(), curr_exp.end() );
- unsigned index_i = 0;
- unsigned index_j = 0;
- bool ret = processSimpleNEq( normal_forms, normal_form_src, t_curr_exp, i, j, index_i, index_j, true );
+ unsigned index = 0;
+ bool ret = processSimpleNEq( normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend, i, j, index, true );
//reverse normal form of i, j
std::reverse( normal_forms[i].begin(), normal_forms[i].end() );
return ret;
}
-bool TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src, std::vector< Node > &curr_exp,
- unsigned i, unsigned j, unsigned& index_i, unsigned& index_j, bool isRev ) {
+bool TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src,
+ std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend,
+ unsigned i, unsigned j, unsigned& index, bool isRev ) {
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() ) {
+ if(index==normal_forms[i].size() || index==normal_forms[j].size() ) {
+ if( index==normal_forms[i].size() && index==normal_forms[j].size() ) {
//we're done
} 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;
+ unsigned k = index==normal_forms[i].size() ? j : i;
+ unsigned index_k = index;
//Node eq_exp = mkAnd( curr_exp );
+ std::vector< Node > curr_exp;
+ getExplanationVectorForPrefix( normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend, i, j, -1, isRev, curr_exp );
while(!d_conflict && index_k<normal_forms[k].size()) {
//can infer that this string must be empty
Node eq = normal_forms[k][index_k].eqNode( d_emptyString );
return true;
}
}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") << "Process " << normal_forms[i][index] << " ... " << normal_forms[j][index] << std::endl;
+ if( normal_forms[i][index]==normal_forms[j][index] ){
Trace("strings-solve-debug") << "Simple Case 1 : strings are equal" << std::endl;
- //terms are equal, continue
- if( normal_forms[i][index_i]!=normal_forms[j][index_j] ){
- Node eq = normal_forms[i][index_i].eqNode(normal_forms[j][index_j]);
- Trace("strings-solve-debug") << "Add to explanation : " << eq << std::endl;
- curr_exp.push_back(eq);
- }
- index_j++;
- index_i++;
+ index++;
success = true;
- } else {
+ }else{
+ Assert( !areEqual(normal_forms[i][index], normal_forms[j][index]) );
std::vector< Node > temp_exp;
- Node length_term_i = getLength( normal_forms[i][index_i], temp_exp );
- Node length_term_j = getLength( normal_forms[j][index_j], temp_exp );
+ Node length_term_i = getLength( normal_forms[i][index], temp_exp );
+ Node length_term_j = getLength( normal_forms[j][index], temp_exp );
//check length(normal_forms[i][index]) == length(normal_forms[j][index])
if( areEqual( length_term_i, length_term_j ) ){
Trace("strings-solve-debug") << "Simple Case 2 : string lengths are equal" << std::endl;
- Node eq = normal_forms[i][index_i].eqNode( normal_forms[j][index_j] );
+ Node eq = normal_forms[i][index].eqNode( normal_forms[j][index] );
//eq = Rewriter::rewrite( eq );
Node length_eq = length_term_i.eqNode( length_term_j );
- temp_exp.insert(temp_exp.end(), curr_exp.begin(), curr_exp.end() );
+ //temp_exp.insert(temp_exp.end(), curr_exp.begin(), curr_exp.end() );
+ getExplanationVectorForPrefix( normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend, i, j, index, isRev, temp_exp );
temp_exp.push_back(length_eq);
sendInference( temp_exp, eq, "LengthEq" );
return true;
- }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 ) ){
+ }else if( ( normal_forms[i][index].getKind()!=kind::CONST_STRING && index==normal_forms[i].size()-1 ) ||
+ ( normal_forms[j][index].getKind()!=kind::CONST_STRING && index==normal_forms[j].size()-1 ) ){
Trace("strings-solve-debug") << "Simple Case 3 : at endpoint" << std::endl;
Node conc;
std::vector< Node > antec;
- antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
+ //antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
+ getExplanationVectorForPrefix( normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend, i, j, -1, isRev, antec );
std::vector< Node > eqn;
for( unsigned r=0; r<2; r++ ) {
- int index_k = r==0 ? index_i : index_j;
+ int index_k = index;
int k = r==0 ? i : j;
std::vector< Node > eqnc;
for( unsigned index_l=index_k; index_l<normal_forms[k].size(); index_l++ ) {
sendInference( antec, conc, "ENDPOINT", true );
return true;
}else{
- index_i = normal_forms[i].size();
- index_j = normal_forms[j].size();
+ Assert( normal_forms[i].size()==normal_forms[j].size() );
+ index = normal_forms[i].size();
}
- } else if(normal_forms[i][index_i].isConst() && normal_forms[j][index_j].isConst()) {
- Node const_str = normal_forms[i][index_i];
- Node other_str = normal_forms[j][index_j];
+ } else if( normal_forms[i][index].isConst() && normal_forms[j][index].isConst() ){
+ Node const_str = normal_forms[i][index];
+ Node other_str = normal_forms[j][index];
Trace("strings-solve-debug") << "Simple Case 3 : Const Split : " << const_str << " vs " << other_str << std::endl;
unsigned len_short = const_str.getConst<String>().size() <= other_str.getConst<String>().size() ? const_str.getConst<String>().size() : other_str.getConst<String>().size();
bool isSameFix = isRev ? const_str.getConst<String>().rstrncmp(other_str.getConst<String>(), len_short): const_str.getConst<String>().strncmp(other_str.getConst<String>(), len_short);
//same prefix/suffix
//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;
if(isRev) {
- int new_len = normal_forms[l][index_l].getConst<String>().size() - len_short;
- Node remainderStr = NodeManager::currentNM()->mkConst( normal_forms[l][index_l].getConst<String>().substr(0, new_len) );
- 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 );
+ int new_len = normal_forms[l][index].getConst<String>().size() - len_short;
+ Node remainderStr = NodeManager::currentNM()->mkConst( normal_forms[l][index].getConst<String>().substr(0, new_len) );
+ Trace("strings-solve-debug-test") << "Break normal form of " << normal_forms[l][index] << " into " << normal_forms[k][index] << ", " << remainderStr << std::endl;
+ normal_forms[l].insert( normal_forms[l].begin()+index + 1, remainderStr );
} else {
- 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 );
+ Node remainderStr = NodeManager::currentNM()->mkConst(normal_forms[l][index].getConst<String>().substr(len_short));
+ Trace("strings-solve-debug-test") << "Break normal form of " << normal_forms[l][index] << " into " << normal_forms[k][index] << ", " << remainderStr << std::endl;
+ normal_forms[l].insert( normal_forms[l].begin()+index + 1, remainderStr );
}
- normal_forms[l][index_l] = normal_forms[k][index_k];
- index_i++;
- index_j++;
+ normal_forms[l][index] = normal_forms[k][index];
+ index++;
success = true;
} else {
std::vector< Node > antec;
//curr_exp is conflict
- antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
+ //antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
+ getExplanationVectorForPrefix( normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend, i, j, index, isRev, antec );
sendInference( antec, d_false, "Const Conflict", true );
return true;
}
return false;
}
-bool TheoryStrings::detectLoop( std::vector< std::vector< Node > > &normal_forms, int i, int j,
- int index_i, int index_j, int &loop_in_i, int &loop_in_j) {
+bool TheoryStrings::detectLoop( std::vector< std::vector< Node > > &normal_forms, int i, int j, int index, int &loop_in_i, int &loop_in_j) {
int has_loop[2] = { -1, -1 };
if( options::stringLB() != 2 ) {
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 ) {
+ if( normal_forms[other_n_index][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] ){
+ if( normal_forms[n_index][lp]==normal_forms[other_n_index][index] ){
has_loop[r] = lp;
break;
}
//xs(zy)=t(yz)xr
bool TheoryStrings::processLoop( std::vector< Node > &antec, std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src,
- int i, int j, int loop_n_index, int other_n_index, int loop_index, int index, int other_index) {
+ int i, int j, int loop_n_index, int other_n_index, int loop_index, int index) {
if( options::stringAbortLoop() ){
Message() << "Looping word equation encountered." << std::endl;
exit( 1 );
}else{
Node conc;
Trace("strings-loop") << "Detected possible loop for " << normal_forms[loop_n_index][loop_index] << std::endl;
- Trace("strings-loop") << " ... (X)= " << normal_forms[other_n_index][other_index] << std::endl;
+ Trace("strings-loop") << " ... (X)= " << normal_forms[other_n_index][index] << std::endl;
Trace("strings-loop") << " ... T(Y.Z)= ";
std::vector< Node > vec_t;
Trace("strings-loop") << " (" << t_yz << ")" << std::endl;
Trace("strings-loop") << " ... S(Z.Y)= ";
std::vector< Node > vec_s;
- for(int lp=other_index+1; lp<(int)normal_forms[other_n_index].size(); ++lp) {
- if(lp != other_index+1) Trace("strings-loop") << " ++ ";
+ for(int lp=index+1; lp<(int)normal_forms[other_n_index].size(); ++lp) {
+ if(lp != index+1) Trace("strings-loop") << " ++ ";
Trace("strings-loop") << normal_forms[other_n_index][lp];
vec_s.push_back( normal_forms[other_n_index][lp] );
}
s_zy.getConst<String>().isRepeated()
) {
Node rep_c = NodeManager::currentNM()->mkConst( s_zy.getConst<String>().substr(0, 1) );
- Trace("strings-loop") << "Special case (X)=" << normal_forms[other_n_index][other_index] << " " << std::endl;
+ Trace("strings-loop") << "Special case (X)=" << normal_forms[other_n_index][index] << " " << std::endl;
Trace("strings-loop") << "... (C)=" << rep_c << " " << std::endl;
//special case
- str_in_re = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, normal_forms[other_n_index][other_index],
+ str_in_re = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, normal_forms[other_n_index][index],
NodeManager::currentNM()->mkNode( kind::REGEXP_STAR,
NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, rep_c ) ) );
conc = str_in_re;
if(cc == d_false) {
continue;
}
- Node conc2 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, normal_forms[other_n_index][other_index],
+ Node conc2 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, normal_forms[other_n_index][index],
NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT,
NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, y),
NodeManager::currentNM()->mkNode(kind::REGEXP_STAR,
vec_r.insert(vec_r.begin(), sk_y);
vec_r.insert(vec_r.begin(), sk_z);
Node conc2 = s_zy.eqNode( mkConcat( vec_r ) );
- Node conc3 = normal_forms[other_n_index][other_index].eqNode( mkConcat( sk_y, sk_w ) );
+ Node conc3 = normal_forms[other_n_index][index].eqNode( mkConcat( sk_y, sk_w ) );
Node restr = r == d_emptyString ? s_zy : mkConcat( sk_z, sk_y );
str_in_re = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, sk_w,
NodeManager::currentNM()->mkNode( kind::REGEXP_STAR,
void TheoryStrings::sendInference( std::vector< Node >& exp, std::vector< Node >& exp_n, Node eq, const char * c, bool asLemma ) {
eq = eq.isNull() ? d_false : Rewriter::rewrite( eq );
if( eq!=d_true ){
+ if( Trace.isOn("strings-infer-debug") ){
+ Trace("strings-infer-debug") << "infer : " << eq << " from: " << std::endl;
+ for( unsigned i=0; i<exp.size(); i++ ){
+ Trace("strings-infer-debug") << " " << exp[i] << std::endl;
+ }
+ for( unsigned i=0; i<exp_n.size(); i++ ){
+ Trace("strings-infer-debug") << " N:" << exp_n[i] << std::endl;
+ }
+ }
bool doSendLemma = ( asLemma || eq==d_false || eq.getKind()==kind::OR || options::stringInferAsLemmas() );
if( doSendLemma ){
Node eq_exp;
}
void TheoryStrings::sendInfer( Node eq_exp, Node eq, const char * c ) {
- Trace("strings-infer-debug") << "infer : " << eq << " from " << eq_exp << std::endl;
if( options::stringInferSym() ){
std::vector< Node > vars;
std::vector< Node > subs;
projects / cvc5.git / commitdiff