summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/bv/bv_subtheory_core.h1
-rw-r--r--src/theory/bv/theory_bv.cpp29
-rw-r--r--src/theory/bv/theory_bv.h4
-rw-r--r--src/theory/datatypes/theory_datatypes.cpp3
-rw-r--r--src/theory/datatypes/theory_datatypes.h6
-rw-r--r--src/theory/strings/theory_strings.cpp425
-rw-r--r--src/theory/strings/theory_strings.h13
-rw-r--r--src/theory/theory.cpp141
-rw-r--r--src/theory/theory.h57
9 files changed, 437 insertions, 242 deletions
diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h
index 643093327..93a938cc0 100644
--- a/src/theory/bv/bv_subtheory_core.h
+++ b/src/theory/bv/bv_subtheory_core.h
@@ -117,6 +117,7 @@ public:
bool hasTerm(TNode node) const { return d_equalityEngine.hasTerm(node); }
void addTermToEqualityEngine(TNode node) { d_equalityEngine.addTerm(node); }
void enableSlicer();
+ eq::EqualityEngine * getEqualityEngine() { return &d_equalityEngine; }
};
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index fec93e033..f0981044b 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -495,7 +495,36 @@ void TheoryBV::propagate(Effort e) {
}
}
+eq::EqualityEngine * TheoryBV::getEqualityEngine() {
+ return NULL;
+}
+bool TheoryBV::getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp ) {
+#if 0
+ CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
+ if( core ){
+ //get the constant equivalence classes
+ bool retVal = false;
+ for( unsigned i=0; i<vars.size(); i++ ){
+ Node n = vars[i];
+ if( core->getEqualityEngine()->hasTerm( n ) ){
+ Node nr = core->getEqualityEngine()->getRepresenative( n );
+ if( nr.isConst() ){
+ subs.push_back( nr );
+ exp[n].push_back( n.eqNode( nr ) );
+ retVal = true;
+ }else{
+ subs.push_back( n );
+ }
+ }
+ }
+ //return true if the substitution is non-trivial
+ return retVal;
+ }
+#endif
+ return false;
+}
+
Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
switch(in.getKind()) {
case kind::EQUAL:
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index ba2a4fc2a..0709ca427 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -79,6 +79,10 @@ public:
std::string identify() const { return std::string("TheoryBV"); }
+ /** equality engine */
+ eq::EqualityEngine * getEqualityEngine();
+ bool getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp );
+
PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
void enableCoreTheorySlicer();
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index dc39183b5..59b9f1d96 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -2095,6 +2095,9 @@ TNode TheoryDatatypes::getRepresentative( TNode a ){
}
}
+bool TheoryDatatypes::getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp ) {
+ return false;
+}
void TheoryDatatypes::printModelDebug( const char* c ){
if(! (Trace.isOn(c))) {
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 5722e7822..49c45590c 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -266,6 +266,9 @@ public:
void collectModelInfo( TheoryModel* m, bool fullModel );
void shutdown() { }
std::string identify() const { return std::string("TheoryDatatypes"); }
+ /** equality engine */
+ eq::EqualityEngine * getEqualityEngine() { return &d_equalityEngine; }
+ bool getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp );
/** debug print */
void printModelDebug( const char* c );
/** entailment check */
@@ -313,9 +316,6 @@ private:
bool areEqual( TNode a, TNode b );
bool areDisequal( TNode a, TNode b );
TNode getRepresentative( TNode a );
-public:
- /** get equality engine */
- eq::EqualityEngine* getEqualityEngine() { return &d_equalityEngine; }
};/* class TheoryDatatypes */
}/* CVC4::theory::datatypes namespace */
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 09b5d00eb..7caa1cbb1 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -82,7 +82,6 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u,
d_proxy_var(u),
d_proxy_var_to_length(u),
d_functionsTerms(c),
- d_ext_func_terms(c),
d_has_extf(c, false ),
d_regexp_memberships(c),
d_regexp_ucached(u),
@@ -98,6 +97,19 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u,
d_cardinality_lits(u),
d_curr_cardinality(c, 0)
{
+ d_extt = new ExtTheory( this );
+ d_extt->addFunctionKind( kind::STRING_SUBSTR );
+ d_extt->addFunctionKind( kind::STRING_STRIDOF );
+ d_extt->addFunctionKind( kind::STRING_ITOS );
+ d_extt->addFunctionKind( kind::STRING_U16TOS );
+ d_extt->addFunctionKind( kind::STRING_U32TOS );
+ d_extt->addFunctionKind( kind::STRING_STOI );
+ d_extt->addFunctionKind( kind::STRING_STOU16 );
+ d_extt->addFunctionKind( kind::STRING_STOU32 );
+ d_extt->addFunctionKind( kind::STRING_STRREPL );
+ d_extt->addFunctionKind( kind::STRING_STRCTN );
+ d_extt->addFunctionKind( kind::STRING_IN_REGEXP );
+
// The kinds we are treating as function application in congruence
d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP);
d_equalityEngine.addFunctionKind(kind::STRING_LENGTH);
@@ -130,6 +142,7 @@ TheoryStrings::~TheoryStrings() {
for( std::map< Node, EqcInfo* >::iterator it = d_eqc_info.begin(); it != d_eqc_info.end(); ++it ){
delete it->second;
}
+ delete d_extt;
}
Node TheoryStrings::getRepresentative( Node t ) {
@@ -158,23 +171,6 @@ bool TheoryStrings::areDisequal( Node a, Node b ){
if( a==b ){
return false;
}else{
- /*
- if( a.getType().isString() ) {
- for( unsigned i=0; i<2; i++ ) {
- Node ac = a.getKind()==kind::STRING_CONCAT ? a[i==0 ? 0 : a.getNumChildren()-1] : a;
- Node bc = b.getKind()==kind::STRING_CONCAT ? b[i==0 ? 0 : b.getNumChildren()-1] : b;
- if( ac.isConst() && bc.isConst() ){
- CVC4::String as = ac.getConst<String>();
- CVC4::String bs = bc.getConst<String>();
- int slen = as.size() > bs.size() ? bs.size() : as.size();
- bool flag = i == 1 ? as.rstrncmp(bs, slen): as.strncmp(bs, slen);
- if(!flag) {
- return true;
- }
- }
- }
- }
- */
if( hasTerm( a ) && hasTerm( b ) ) {
Node ar = d_equalityEngine.getRepresentative( a );
Node br = d_equalityEngine.getRepresentative( b );
@@ -291,6 +287,50 @@ Node TheoryStrings::explain( TNode literal ){
}
}
+bool TheoryStrings::getCurrentSubstitution( int effort, std::vector< Node >& vars,
+ std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp ) {
+ Trace("strings-subs") << "getCurrentSubstitution, effort = " << effort << std::endl;
+ for( unsigned i=0; i<vars.size(); i++ ){
+ Node n = vars[i];
+ Trace("strings-subs") << " get subs for " << n << "..." << std::endl;
+ if( effort>=3 ){
+ //model values
+ Node mv = d_valuation.getModel()->getRepresentative( n );
+ Trace("strings-subs") << " model val : " << mv << std::endl;
+ subs.push_back( mv );
+ }else{
+ Node nr = getRepresentative( n );
+ std::map< Node, Node >::iterator itc = d_eqc_to_const.find( nr );
+ if( itc!=d_eqc_to_const.end() ){
+ //constant equivalence classes
+ Trace("strings-subs") << " constant eqc : " << d_eqc_to_const_exp[nr] << " " << d_eqc_to_const_base[nr] << " " << nr << std::endl;
+ subs.push_back( itc->second );
+ if( !d_eqc_to_const_exp[nr].isNull() ){
+ exp[n].push_back( d_eqc_to_const_exp[nr] );
+ }
+ if( !d_eqc_to_const_base[nr].isNull() ){
+ addToExplanation( n, d_eqc_to_const_base[nr], exp[n] );
+ }
+ }else if( effort>=1 && effort<3 && n.getType().isString() ){
+ //normal forms
+ Node ns = getNormalString( d_normal_forms_base[nr], exp[n] );
+ subs.push_back( ns );
+ Trace("strings-subs") << " normal eqc : " << ns << " " << d_normal_forms_base[nr] << " " << nr << std::endl;
+ if( !d_normal_forms_base[nr].isNull() ) {
+ addToExplanation( n, d_normal_forms_base[nr], exp[n] );
+ }
+ }else{
+ //representative?
+ //Trace("strings-subs") << " representative : " << nr << std::endl;
+ //addToExplanation( n, nr, exp[n] );
+ //subs.push_back( nr );
+ subs.push_back( n );
+ }
+ }
+ }
+ return true;
+}
+
/////////////////////////////////////////////////////////////////////////////
// NOTIFICATIONS
/////////////////////////////////////////////////////////////////////////////
@@ -652,13 +692,15 @@ bool TheoryStrings::needsCheckLastEffort() {
}
void TheoryStrings::checkExtfReductions( int effort ) {
- Trace("strings-process-debug") << "Checking preprocess at effort " << effort << ", #to process=" << d_ext_func_terms.size() << "..." << std::endl;
- for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){
- Node n = (*it).first;
- Trace("strings-process-debug2") << n << ", active=" << (*it).second << ", model active=" << d_extf_info_tmp[n].d_model_active << std::endl;
- if( (*it).second && d_extf_info_tmp[n].d_model_active ){
+ std::vector< Node > extf;
+ d_extt->getActive( extf );
+ for( unsigned i=0; i<extf.size(); i++ ){
+ Node n = extf[i];
+ if( d_extf_info_tmp[n].d_model_active ){
Assert( d_extf_info_tmp.find( n )!=d_extf_info_tmp.end() );
- checkExtfReduction( n, d_extf_info_tmp[n].d_pol, effort );
+ if( checkExtfReduction( n, d_extf_info_tmp[n].d_pol, effort ) ){
+ d_extt->markReduced( n );
+ }
if( hasProcessed() ){
return;
}
@@ -666,7 +708,7 @@ void TheoryStrings::checkExtfReductions( int effort ) {
}
}
-void TheoryStrings::checkExtfReduction( Node atom, int pol, int effort ) {
+bool TheoryStrings::checkExtfReduction( Node atom, int pol, int effort ) {
//determine the effort level to process the extf at
// 0 - at assertion time, 1+ - after no other reduction is applicable
int r_effort = -1;
@@ -683,7 +725,6 @@ void TheoryStrings::checkExtfReduction( Node atom, int pol, int effort ) {
Node lens = getLength( s, lexp );
if( areEqual( lenx, lens ) ){
Trace("strings-extf-debug") << " resolve extf : " << atom << " based on equal lengths disequality." << std::endl;
- d_ext_func_terms[atom] = false;
//we can reduce to disequality when lengths are equal
if( !areDisequal( x, s ) ){
lexp.push_back( lenx.eqNode(lens) );
@@ -691,6 +732,7 @@ void TheoryStrings::checkExtfReduction( Node atom, int pol, int effort ) {
Node xneqs = x.eqNode(s).negate();
sendInference( lexp, xneqs, "NEG-CTN-EQL", true );
}
+ return true;
}else if( !areDisequal( lenx, lens ) ){
//split on their lenths
sendSplit( lenx, lens, "NEG-CTN-SP" );
@@ -724,8 +766,8 @@ void TheoryStrings::checkExtfReduction( Node atom, int pol, int effort ) {
exp_vec.push_back( atom );
sendInference( d_empty_vec, exp_vec, eq, "POS-CTN", true );
//we've reduced this atom
- d_ext_func_terms[ atom ] = false;
Trace("strings-extf-debug") << " resolve extf : " << atom << " based on positive contain reduction." << std::endl;
+ return true;
}else{
// for STRING_SUBSTR, STRING_STRCTN with pol=-1,
// STRING_STRIDOF, STRING_ITOS, STRING_U16TOS, STRING_U32TOS, STRING_STOI, STRING_STOU16, STRING_STOU32, STRING_STRREPL
@@ -739,11 +781,12 @@ void TheoryStrings::checkExtfReduction( Node atom, int pol, int effort ) {
Trace("strings-red-lemma") << "...from " << atom << std::endl;
sendInference( d_empty_vec, nnlem, "Reduction", true );
//we've reduced this atom
- d_ext_func_terms[ atom ] = false;
Trace("strings-extf-debug") << " resolve extf : " << atom << " based on reduction." << std::endl;
+ return true;
}
}
}
+ return false;
}
TheoryStrings::EqcInfo::EqcInfo( context::Context* c ) : d_const_term(c), d_length_term(c), d_cardinality_lem_k(c), d_normalized_length(c) {
@@ -945,7 +988,7 @@ void TheoryStrings::assertPendingFact(Node atom, bool polarity, Node exp) {
d_equalityEngine.assertPredicate( atom, polarity, exp );
//process extf
if( atom.getKind()==kind::STRING_IN_REGEXP ){
- addExtendedFuncTerm( atom );
+ d_extt->registerTerm( atom );
if( polarity && atom[1].getKind()==kind::REGEXP_RANGE ){
if( d_extf_infer_cache_u.find( atom )==d_extf_infer_cache_u.end() ){
d_extf_infer_cache_u.insert( atom );
@@ -1044,15 +1087,15 @@ void TheoryStrings::checkInit() {
eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
while( !eqc_i.isFinished() ) {
Node n = *eqc_i;
- if( tn.isInteger() ){
+ if( n.isConst() ){
+ d_eqc_to_const[eqc] = n;
+ d_eqc_to_const_base[eqc] = n;
+ d_eqc_to_const_exp[eqc] = Node::null();
+ }else if( tn.isInteger() ){
if( n.getKind()==kind::STRING_LENGTH ){
Node nr = getRepresentative( n[0] );
d_eqc_to_len_term[nr] = n[0];
}
- }else if( n.isConst() ){
- d_eqc_to_const[eqc] = n;
- d_eqc_to_const_base[eqc] = n;
- d_eqc_to_const_exp[eqc] = Node::null();
}else if( n.getNumChildren()>0 ){
Kind k = n.getKind();
if( k!=kind::EQUAL ){
@@ -1089,16 +1132,8 @@ void TheoryStrings::checkInit() {
//infer the equality
sendInference( exp, n.eqNode( nc ), "I_Norm" );
}else{
- //update the extf map : only process if neither has been reduced
- NodeBoolMap::const_iterator it = d_ext_func_terms.find( n );
- if( it!=d_ext_func_terms.end() ){
- if( d_ext_func_terms.find( nc )==d_ext_func_terms.end() ){
- d_ext_func_terms[nc] = (*it).second;
- }else{
- d_ext_func_terms[nc] = d_ext_func_terms[nc] && (*it).second;
- }
- d_ext_func_terms[n] = false;
- }
+ //mark as congruent : only process if neither has been reduced
+ d_extt->markCongruent( nc, n );
}
//this node is congruent to another one, we can ignore it
Trace("strings-process-debug") << " congruent term : " << n << std::endl;
@@ -1255,179 +1290,126 @@ void TheoryStrings::checkExtfEval( int effort ) {
Trace("strings-extf-list") << "Active extended functions, effort=" << effort << " : " << std::endl;
d_extf_info_tmp.clear();
bool has_nreduce = false;
- Trace("strings-extf-debug") << "Checking " << d_ext_func_terms.size() << " extended functions." << std::endl;
- for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){
- //if not already reduced
- if( (*it).second ){
- Node n = (*it).first;
-
- //setup information about extf
- std::map< Node, ExtfInfo >::iterator iti = d_extf_info.find( n );
- Assert( iti!=d_extf_info.end() );
- d_extf_info_tmp[n].init();
- std::map< Node, ExtfInfoTmp >::iterator itit = d_extf_info_tmp.find( n );
- //get polarity
- if( n.getType().isBoolean() ){
- if( areEqual( n, d_true ) ){
- itit->second.d_pol = 1;
- }else if( areEqual( n, d_false ) ){
- itit->second.d_pol = -1;
- }
+ std::vector< Node > terms;
+ std::vector< Node > sterms;
+ std::vector< std::vector< Node > > exp;
+ d_extt->getInferences( effort, terms, sterms, exp );
+ for( unsigned i=0; i<terms.size(); i++ ){
+ Node n = terms[i];
+ Node sn = sterms[i];
+ //setup information about extf
+ d_extf_info_tmp[n].init();
+ std::map< Node, ExtfInfoTmp >::iterator itit = d_extf_info_tmp.find( n );
+ if( n.getType().isBoolean() ){
+ if( areEqual( n, d_true ) ){
+ itit->second.d_pol = 1;
+ }else if( areEqual( n, d_false ) ){
+ itit->second.d_pol = -1;
}
- //compute rep vars map
- for( unsigned j=0; j<iti->second.d_vars.size(); j++ ){
- Node nr = getRepresentative( iti->second.d_vars[j] );
- itit->second.d_rep_vars[nr].push_back( iti->second.d_vars[j] );
- }
-
- Trace("strings-extf-debug") << "Check extf " << n << ", pol = " << itit->second.d_pol << ", effort=" << effort << "..." << std::endl;
- //build up a best current substitution for the variables in the term, exp is explanation for substitution
- std::vector< Node > var;
- std::vector< Node > sub;
- for( std::map< Node, std::vector< Node > >::iterator itv = itit->second.d_rep_vars.begin(); itv != itit->second.d_rep_vars.end(); ++itv ){
- Node nr = itv->first;
- Node s;
- Node b;
- Node e;
- if( effort>=3 ){
- //model values
- s = d_valuation.getModel()->getRepresentative( nr );
- }else{
- std::map< Node, Node >::iterator itc = d_eqc_to_const.find( nr );
- if( itc!=d_eqc_to_const.end() ){
- //constant equivalence classes
- b = d_eqc_to_const_base[nr];
- s = itc->second;
- e = d_eqc_to_const_exp[nr];
- }else if( effort>=1 && effort<3 ){
- //normal forms
- b = d_normal_forms_base[nr];
- std::vector< Node > expt;
- s = getNormalString( b, expt );
- e = mkAnd( expt );
- }
- }
- if( !s.isNull() ){
- bool added = false;
- for( unsigned i=0; i<itv->second.size(); i++ ){
- if( itv->second[i]!=s ){
- var.push_back( itv->second[i] );
- sub.push_back( s );
- if( !b.isNull() ){
- addToExplanation( itv->second[i], b, itit->second.d_exp );
- }
- Trace("strings-extf-debug") << " " << itv->second[i] << " --> " << s << std::endl;
- added = true;
+ }
+ Trace("strings-extf-debug") << "Check extf " << n << " == " << sn << ", pol = " << itit->second.d_pol << ", effort=" << effort << "..." << std::endl;
+ //do the inference
+ Node to_reduce;
+ if( n!=sn ){
+ itit->second.d_exp.insert( itit->second.d_exp.end(), exp[i].begin(), exp[i].end() );
+ // inference is rewriting the substituted node
+ Node nrc = Rewriter::rewrite( sn );
+ //if rewrites to a constant, then do the inference and mark as reduced
+ if( nrc.isConst() ){
+ if( effort<3 ){
+ d_extt->markReduced( n );
+ Trace("strings-extf-debug") << " resolvable by evaluation..." << std::endl;
+ std::vector< Node > exps;
+ Trace("strings-extf-debug") << " get symbolic definition..." << std::endl;
+ Node nrs = getSymbolicDefinition( sn, exps );
+ if( !nrs.isNull() ){
+ Trace("strings-extf-debug") << " rewrite " << nrs << "..." << std::endl;
+ nrs = Rewriter::rewrite( nrs );
+ //ensure the symbolic form is non-trivial
+ if( nrs.isConst() ){
+ Trace("strings-extf-debug") << " symbolic definition is trivial..." << std::endl;
+ nrs = Node::null();
}
+ }else{
+ Trace("strings-extf-debug") << " could not infer symbolic definition." << std::endl;
}
- if( added && !e.isNull() ){
- addToExplanation( e, itit->second.d_exp );
- }
- }
- }
- Node to_reduce;
- if( !var.empty() ){
- //do substitution, evaluate
- Node nr = n.substitute( var.begin(), var.end(), sub.begin(), sub.end() );
- Node nrc = Rewriter::rewrite( nr );
- //if rewrites to a constant, then do the inference and mark as reduced
- if( nrc.isConst() ){
- if( effort<3 ){
- d_ext_func_terms[n] = false;
- Trace("strings-extf-debug") << " resolvable by evaluation..." << std::endl;
- std::vector< Node > exps;
- Trace("strings-extf-debug") << " get symbolic definition..." << std::endl;
- Node nrs = getSymbolicDefinition( nr, exps );
- if( !nrs.isNull() ){
- Trace("strings-extf-debug") << " rewrite " << nrs << "..." << std::endl;
- nrs = Rewriter::rewrite( nrs );
- //ensure the symbolic form is non-trivial
- if( nrs.isConst() ){
- Trace("strings-extf-debug") << " symbolic definition is trivial..." << std::endl;
- nrs = Node::null();
+ Node conc;
+ if( !nrs.isNull() ){
+ Trace("strings-extf-debug") << " symbolic def : " << nrs << std::endl;
+ if( !areEqual( nrs, nrc ) ){
+ //infer symbolic unit
+ if( n.getType().isBoolean() ){
+ conc = nrc==d_true ? nrs : nrs.negate();
+ }else{
+ conc = nrs.eqNode( nrc );
}
- }else{
- Trace("strings-extf-debug") << " could not infer symbolic definition." << std::endl;
+ itit->second.d_exp.clear();
}
- Node conc;
- if( !nrs.isNull() ){
- Trace("strings-extf-debug") << " symbolic def : " << nrs << std::endl;
- if( !areEqual( nrs, nrc ) ){
- //infer symbolic unit
- if( n.getType().isBoolean() ){
- conc = nrc==d_true ? nrs : nrs.negate();
- }else{
- conc = nrs.eqNode( nrc );
- }
- itit->second.d_exp.clear();
- }
- }else{
- if( !areEqual( n, nrc ) ){
- if( n.getType().isBoolean() ){
- if( areEqual( n, nrc==d_true ? d_false : d_true ) ){
- itit->second.d_exp.push_back( nrc==d_true ? n.negate() : n );
- conc = d_false;
- }else{
- conc = nrc==d_true ? n : n.negate();
- }
+ }else{
+ if( !areEqual( n, nrc ) ){
+ if( n.getType().isBoolean() ){
+ if( areEqual( n, nrc==d_true ? d_false : d_true ) ){
+ itit->second.d_exp.push_back( nrc==d_true ? n.negate() : n );
+ conc = d_false;
}else{
- conc = n.eqNode( nrc );
+ conc = nrc==d_true ? n : n.negate();
}
+ }else{
+ conc = n.eqNode( nrc );
}
}
- if( !conc.isNull() ){
- Trace("strings-extf") << " resolve extf : " << nr << " -> " << nrc << std::endl;
- sendInference( itit->second.d_exp, conc, effort==0 ? "EXTF" : "EXTF-N", true );
- if( d_conflict ){
- Trace("strings-extf-debug") << " conflict, return." << std::endl;
- return;
- }
- }
- }else{
- //check if it is already equal, if so, mark as reduced. Otherwise, do nothing.
- if( areEqual( n, nrc ) ){
- Trace("strings-extf") << " resolved extf, since satisfied by model: " << n << std::endl;
- itit->second.d_model_active = false;
- }
}
- //if it reduces to a conjunction, infer each and reduce
- }else if( ( nrc.getKind()==kind::OR && itit->second.d_pol==-1 ) || ( nrc.getKind()==kind::AND && itit->second.d_pol==1 ) ){
- Assert( effort<3 );
- d_ext_func_terms[n] = false;
- itit->second.d_exp.push_back( itit->second.d_pol==-1 ? n.negate() : n );
- Trace("strings-extf-debug") << " decomposable..." << std::endl;
- Trace("strings-extf") << " resolve extf : " << nr << " -> " << nrc << ", pol = " << itit->second.d_pol << std::endl;
- for( unsigned i=0; i<nrc.getNumChildren(); i++ ){
- sendInference( itit->second.d_exp, itit->second.d_pol==-1 ? nrc[i].negate() : nrc[i], effort==0 ? "EXTF_d" : "EXTF_d-N" );
+ if( !conc.isNull() ){
+ Trace("strings-extf") << " resolve extf : " << sn << " -> " << nrc << std::endl;
+ sendInference( itit->second.d_exp, conc, effort==0 ? "EXTF" : "EXTF-N", true );
+ if( d_conflict ){
+ Trace("strings-extf-debug") << " conflict, return." << std::endl;
+ return;
+ }
}
}else{
- to_reduce = nrc;
+ //check if it is already equal, if so, mark as reduced. Otherwise, do nothing.
+ if( areEqual( n, nrc ) ){
+ Trace("strings-extf") << " resolved extf, since satisfied by model: " << n << std::endl;
+ itit->second.d_model_active = false;
+ }
+ }
+ //if it reduces to a conjunction, infer each and reduce
+ }else if( ( nrc.getKind()==kind::OR && itit->second.d_pol==-1 ) || ( nrc.getKind()==kind::AND && itit->second.d_pol==1 ) ){
+ Assert( effort<3 );
+ d_extt->markReduced( n );
+ itit->second.d_exp.push_back( itit->second.d_pol==-1 ? n.negate() : n );
+ Trace("strings-extf-debug") << " decomposable..." << std::endl;
+ Trace("strings-extf") << " resolve extf : " << sn << " -> " << nrc << ", pol = " << itit->second.d_pol << std::endl;
+ for( unsigned i=0; i<nrc.getNumChildren(); i++ ){
+ sendInference( itit->second.d_exp, itit->second.d_pol==-1 ? nrc[i].negate() : nrc[i], effort==0 ? "EXTF_d" : "EXTF_d-N" );
}
}else{
- to_reduce = n;
+ to_reduce = nrc;
}
- if( !to_reduce.isNull() ){
- Assert( effort<3 );
- if( effort==1 ){
- Trace("strings-extf") << " cannot rewrite extf : " << to_reduce << std::endl;
+ }else{
+ to_reduce = sterms[i];
+ }
+ //if not reduced
+ if( !to_reduce.isNull() ){
+ Assert( effort<3 );
+ if( effort==1 ){
+ Trace("strings-extf") << " cannot rewrite extf : " << to_reduce << std::endl;
+ }
+ checkExtfInference( n, to_reduce, itit->second, effort );
+ if( Trace.isOn("strings-extf-list") ){
+ Trace("strings-extf-list") << " * " << to_reduce;
+ if( itit->second.d_pol!=0 ){
+ Trace("strings-extf-list") << ", pol = " << itit->second.d_pol;
}
- checkExtfInference( n, to_reduce, itit->second, effort );
- if( Trace.isOn("strings-extf-list") ){
- Trace("strings-extf-list") << " * " << to_reduce;
- if( itit->second.d_pol!=0 ){
- Trace("strings-extf-list") << ", pol = " << itit->second.d_pol;
- }
- if( n!=to_reduce ){
- Trace("strings-extf-list") << ", from " << n;
- }
- Trace("strings-extf-list") << std::endl;
+ if( n!=to_reduce ){
+ Trace("strings-extf-list") << ", from " << n;
}
- }
- if( d_ext_func_terms[n] && itit->second.d_model_active ){
+ Trace("strings-extf-list") << std::endl;
+ }
+ if( d_extt->isActive( n ) && itit->second.d_model_active ){
has_nreduce = true;
}
- }else{
- Trace("strings-extf-debug") << " already reduced " << (*it).first << std::endl;
}
}
d_has_extf = has_nreduce;
@@ -1457,7 +1439,7 @@ void TheoryStrings::checkExtfInference( Node n, Node nr, ExtfInfoTmp& in, int ef
children[index] = nr[index][i];
Node conc = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, children );
//can mark as reduced, since model for n => model for conc
- d_ext_func_terms[conc] = false;
+ d_extt->markReduced( conc );
sendInference( in.d_exp, in.d_pol==1 ? conc : conc.negate(), "CTN_Decompose" );
}
@@ -1494,7 +1476,7 @@ void TheoryStrings::checkExtfInference( Node n, Node nr, ExtfInfoTmp& in, int ef
}
}else{
Trace("strings-extf-debug") << " redundant." << std::endl;
- d_ext_func_terms[n] = false;
+ d_extt->markReduced( n );
}
}
}
@@ -3897,29 +3879,13 @@ Node TheoryStrings::ppRewrite(TNode atom) {
void TheoryStrings::collectExtendedFuncTerms( Node n, std::map< Node, bool >& visited ) {
if( visited.find( n )==visited.end() ){
visited[n] = true;
- if( n.getKind()==kind::STRING_SUBSTR || n.getKind()==kind::STRING_STRIDOF ||
- n.getKind() == kind::STRING_ITOS || n.getKind() == kind::STRING_U16TOS || n.getKind() == kind::STRING_U32TOS ||
- n.getKind() == kind::STRING_STOI || n.getKind() == kind::STRING_STOU16 || n.getKind() == kind::STRING_STOU32 ||
- n.getKind() == kind::STRING_STRREPL || n.getKind() == kind::STRING_STRCTN ){
- addExtendedFuncTerm( n );
- }
+ d_extt->registerTerm( n );
for( unsigned i=0; i<n.getNumChildren(); i++ ){
collectExtendedFuncTerms( n[i], visited );
}
}
}
-void TheoryStrings::addExtendedFuncTerm( Node n ) {
- if( d_ext_func_terms.find( n )==d_ext_func_terms.end() ){
- Trace("strings-extf-debug2") << "Found extended function : " << n << std::endl;
- Assert( n.getKind()==kind::STRING_IN_REGEXP || options::stringLazyPreproc() );
- d_ext_func_terms[n] = true;
- d_has_extf = true;
- std::map< Node, bool > visited;
- collectVars( n, d_extf_info[n].d_vars, visited );
- }
-}
-
// Stats
TheoryStrings::Statistics::Statistics():
d_splits("TheoryStrings::NumOfSplitOnDemands", 0),
@@ -4291,7 +4257,7 @@ bool TheoryStrings::checkMemberships2() {
} else {
//TODO: split
}
- */
+ */
}
Assert(false); //TODO:tmp
}
@@ -4302,20 +4268,17 @@ bool TheoryStrings::checkMemberships2() {
void TheoryStrings::checkMemberships() {
//add the memberships
- for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){
- if( (*it).second ){
- Node n = (*it).first;
- if( n.getKind()==kind::STRING_IN_REGEXP ) {
- Assert( d_extf_info_tmp.find( n )!=d_extf_info_tmp.end() );
- Assert( d_extf_info_tmp[n].d_pol==1 || d_extf_info_tmp[n].d_pol==-1 );
- bool pol = d_extf_info_tmp[n].d_pol==1;
- Trace("strings-process-debug") << " add membership : " << n << ", pol = " << pol << std::endl;
- addMembership( pol ? n : n.negate() );
- }
- }
+ std::vector< Node > mems;
+ d_extt->getActive( mems, kind::STRING_IN_REGEXP );
+ for( unsigned i=0; i<mems.size(); i++ ){
+ Node n = mems[i];
+ Assert( d_extf_info_tmp.find( n )!=d_extf_info_tmp.end() );
+ Assert( d_extf_info_tmp[n].d_pol==1 || d_extf_info_tmp[n].d_pol==-1 );
+ bool pol = d_extf_info_tmp[n].d_pol==1;
+ Trace("strings-process-debug") << " add membership : " << n << ", pol = " << pol << std::endl;
+ addMembership( pol ? n : n.negate() );
}
-
bool addedLemma = false;
bool changed = false;
std::vector< Node > processed;
@@ -4826,7 +4789,7 @@ void TheoryStrings::addMembership(Node assertion) {
}
}
-Node TheoryStrings::getNormalString( Node x, std::vector<Node> &nf_exp ){
+Node TheoryStrings::getNormalString( Node x, std::vector< Node >& nf_exp ){
if( !x.isConst() ){
Node xr = getRepresentative( x );
if( d_normal_forms.find( xr ) != d_normal_forms.end() ){
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 3cab81a70..fe72bd8e7 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -70,8 +70,9 @@ public:
bool propagate(TNode literal);
void explain( TNode literal, std::vector<TNode>& assumptions );
Node explain( TNode literal );
-
-
+ eq::EqualityEngine * getEqualityEngine() { return &d_equalityEngine; }
+ bool getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp );
+
// NotifyClass for equality engine
class NotifyClass : public eq::EqualityEngineNotify {
TheoryStrings& d_str;
@@ -251,8 +252,6 @@ private:
/** All the function terms that the theory has seen */
context::CDList<TNode> d_functionsTerms;
private:
- //extended string terms, map to whether they are active
- NodeBoolMap d_ext_func_terms;
//any non-reduced extended functions exist
context::CDO< bool > d_has_extf;
// static information about extf
@@ -276,15 +275,13 @@ private:
//explanation
std::vector< Node > d_exp;
//reps -> list of variables
- std::map< Node, std::vector< Node > > d_rep_vars;
+ //std::map< Node, std::vector< Node > > d_rep_vars;
//false if it is reduced in the model
bool d_model_active;
};
- std::map< Node, ExtfInfo > d_extf_info;
std::map< Node, ExtfInfoTmp > d_extf_info_tmp;
//collect extended operator terms
void collectExtendedFuncTerms( Node n, std::map< Node, bool >& visited );
- void addExtendedFuncTerm( Node n );
private:
class InferInfo {
public:
@@ -324,7 +321,7 @@ private:
Node getSymbolicDefinition( Node n, std::vector< Node >& exp );
//check extf reduction
void checkExtfReductions( int effort );
- void checkExtfReduction( Node atom, int pol, int effort );
+ bool checkExtfReduction( Node atom, int pol, int effort );
//flat forms check
void checkFlatForms();
Node checkCycles( Node eqc, std::vector< Node >& curr, std::vector< Node >& exp );
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 7e2b6df55..7fa74df6a 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -66,6 +66,7 @@ Theory::Theory(TheoryId id, context::Context* satContext,
, d_sharedTermsIndex(satContext, 0)
, d_careGraph(NULL)
, d_quantEngine(NULL)
+ , d_extt(NULL)
, d_checkTime(getFullInstanceName() + "::checkTime")
, d_computeCareGraphTime(getFullInstanceName() + "::computeCareGraphTime")
, d_sharedTerms(satContext)
@@ -311,5 +312,145 @@ TheoryId EntailmentCheckSideEffects::getTheoryId() const {
EntailmentCheckSideEffects::~EntailmentCheckSideEffects() {
}
+
+ExtTheory::ExtTheory( Theory * p ) : d_parent( p ),
+d_ext_func_terms( p->getSatContext() ), d_has_extf( p->getSatContext() ){
+
+}
+
+void ExtTheory::collectVars( Node n, std::vector< Node >& vars, std::map< Node, bool >& visited ) {
+ if( !n.isConst() ){
+ if( visited.find( n )==visited.end() ){
+ visited[n] = true;
+ if( n.getNumChildren()>0 ){
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ collectVars( n[i], vars, visited );
+ }
+ }else{
+ vars.push_back( n );
+ }
+ }
+ }
+}
+
+//do inferences
+void ExtTheory::getInferences( int effort, std::vector< Node >& terms, std::vector< Node >& sterms, std::vector< std::vector< Node > >& exp ) {
+ //all variables we need to find a substitution for
+ std::vector< Node > vars;
+ std::vector< Node > sub;
+ std::map< Node, std::vector< Node > > expc;
+ Trace("extt-debug") << "Checking " << d_ext_func_terms.size() << " extended functions." << std::endl;
+ for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){
+ //if not already reduced
+ if( (*it).second ){
+ Node n = (*it).first;
+ terms.push_back( n );
+ std::map< Node, ExtfInfo >::iterator iti = d_extf_info.find( n );
+ Assert( iti!=d_extf_info.end() );
+ for( unsigned i=0; i<iti->second.d_vars.size(); i++ ){
+ if( std::find( vars.begin(), vars.end(), iti->second.d_vars[i] )==vars.end() ){
+ vars.push_back( iti->second.d_vars[i] );
+ }
+ }
+ }
+ }
+ Trace("extt-debug") << "..." << terms.size() << " unreduced." << std::endl;
+ if( !terms.empty() ){
+ //get the current substitution
+ if( d_parent->getCurrentSubstitution( effort, vars, sub, expc ) ){
+ for( unsigned i=0; i<terms.size(); i++ ){
+ //do substitution, rewrite
+ Node n = terms[i];
+ Node ns = n.substitute( vars.begin(), vars.end(), sub.begin(), sub.end() );
+ std::vector< Node > expn;
+ if( ns!=n ){
+ //build explanation: explanation vars = sub for each vars in FV( n )
+ std::map< Node, ExtfInfo >::iterator iti = d_extf_info.find( n );
+ Assert( iti!=d_extf_info.end() );
+ for( unsigned j=0; j<iti->second.d_vars.size(); j++ ){
+ Node v = iti->second.d_vars[j];
+ std::map< Node, std::vector< Node > >::iterator itx = expc.find( v );
+ if( itx!=expc.end() ){
+ for( unsigned k=0; k<itx->second.size(); k++ ){
+ if( std::find( expn.begin(), expn.end(), itx->second[k] )==expn.end() ){
+ expn.push_back( itx->second[k] );
+ }
+ }
+ }
+ }
+ }
+ Trace("extt-debug") << " have " << n << " == " << ns << ", exp size=" << expn.size() << "." << std::endl;
+ //add to vector
+ sterms.push_back( ns );
+ exp.push_back( expn );
+ }
+ }else{
+ for( unsigned i=0; i<terms.size(); i++ ){
+ sterms.push_back( terms[i] );
+ }
+ }
+ }
+}
+
+//register term
+void ExtTheory::registerTerm( Node n ) {
+ if( d_extf_kind.find( n.getKind() )!=d_extf_kind.end() ){
+ if( d_ext_func_terms.find( n )==d_ext_func_terms.end() ){
+ Trace("extt-debug") << "Found extended function : " << n << " in " << d_parent->getId() << std::endl;
+ d_ext_func_terms[n] = true;
+ d_has_extf = true;
+ std::map< Node, bool > visited;
+ collectVars( n, d_extf_info[n].d_vars, visited );
+ }
+ }
+}
+
+//mark reduced
+void ExtTheory::markReduced( Node n ) {
+ d_ext_func_terms[n] = false;
+ //TODO update has_extf
+}
+
+//mark congruent
+void ExtTheory::markCongruent( Node a, Node b ) {
+ NodeBoolMap::const_iterator it = d_ext_func_terms.find( b );
+ if( it!=d_ext_func_terms.end() ){
+ if( d_ext_func_terms.find( a )==d_ext_func_terms.end() ){
+ d_ext_func_terms[a] = (*it).second;
+ }else{
+ d_ext_func_terms[a] = d_ext_func_terms[a] && (*it).second;
+ }
+ d_ext_func_terms[b] = false;
+ }
+}
+
+//is active
+bool ExtTheory::isActive( Node n ) {
+ NodeBoolMap::const_iterator it = d_ext_func_terms.find( n );
+ if( it!=d_ext_func_terms.end() ){
+ return (*it).second;
+ }else{
+ return false;
+ }
+}
+//get active
+void ExtTheory::getActive( std::vector< Node >& active ) {
+ for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){
+ //if not already reduced
+ if( (*it).second ){
+ active.push_back( (*it).first );
+ }
+ }
+}
+
+void ExtTheory::getActive( std::vector< Node >& active, Kind k ) {
+ for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){
+ //if not already reduced
+ if( (*it).second && (*it).first.getKind()==k ){
+ active.push_back( (*it).first );
+ }
+ }
+}
+
}/* CVC4::theory namespace */
}/* CVC4 namespace */
diff --git a/src/theory/theory.h b/src/theory/theory.h
index b5a5d4e6d..ede06fd2d 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -48,6 +48,7 @@ namespace theory {
class QuantifiersEngine;
class TheoryModel;
class SubstitutionMap;
+class ExtTheory;
class EntailmentCheckParameters;
class EntailmentCheckSideEffects;
@@ -201,6 +202,9 @@ private:
protected:
+ /** extended theory */
+ ExtTheory * d_extt;
+
// === STATISTICS ===
/** time spent in check calls */
TimerStat d_checkTime;
@@ -881,6 +885,16 @@ public:
*/
virtual std::pair<bool, Node> entailmentCheck(TNode lit, const EntailmentCheckParameters* params = NULL, EntailmentCheckSideEffects* out = NULL);
+ /* equality engine */
+ virtual eq::EqualityEngine * getEqualityEngine() { return NULL; }
+
+ /* get current substitution at an effort
+ * input : vars
+ * output : subs, exp
+ * where ( exp[vars[i]] => vars[i] = subs[i] ) holds for all i
+ */
+ virtual bool getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp ) { return false; }
+
/**
* Turn on proof-production mode.
*/
@@ -950,6 +964,49 @@ public:
virtual ~EntailmentCheckSideEffects();
};/* class EntailmentCheckSideEffects */
+
+class ExtTheory {
+ friend class Theory;
+ typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
+protected:
+ Theory * d_parent;
+ //extended string terms, map to whether they are active
+ NodeBoolMap d_ext_func_terms;
+ //any non-reduced extended functions exist
+ context::CDO< bool > d_has_extf;
+ //extf kind
+ std::map< Kind, bool > d_extf_kind;
+ //information for extf
+ class ExtfInfo {
+ public:
+ //all variables in this term
+ std::vector< Node > d_vars;
+ };
+ std::map< Node, ExtfInfo > d_extf_info;
+ //collect variables
+ void collectVars( Node n, std::vector< Node >& vars, std::map< Node, bool >& visited );
+public:
+ ExtTheory( Theory * p );
+ virtual ~ExtTheory(){}
+ //add extf kind
+ void addFunctionKind( Kind k ) { d_extf_kind[k] = true; }
+ //do inferences
+ // input : effort
+ // output : terms, sterms, exp, where ( exp[i] => terms[i] = sterms[i] ) for all i
+ void getInferences( int effort, std::vector< Node >& terms, std::vector< Node >& sterms, std::vector< std::vector< Node > >& exp );
+ //register term
+ void registerTerm( Node n );
+ //mark reduced
+ void markReduced( Node n );
+ //mark congruent
+ void markCongruent( Node a, Node b );
+ //is active
+ bool isActive( Node n );
+ //get active
+ void getActive( std::vector< Node >& active );
+ void getActive( std::vector< Node >& active, Kind k );
+};
+
}/* CVC4::theory namespace */
}/* CVC4 namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback