From 59c96a073e34f51b415863ece51c3242c953acc4 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 8 Oct 2013 09:01:13 -0500 Subject: Optimizations for datatypes theory. There seems to be a bug in trans_closure, currently implemented a work around. --- src/theory/datatypes/theory_datatypes.cpp | 135 +++++++++++++++++++----------- src/theory/datatypes/theory_datatypes.h | 2 +- src/util/datatype.cpp | 5 ++ src/util/datatype.h | 7 +- src/util/trans_closure.cpp | 28 +++++-- src/util/trans_closure.h | 13 +-- 6 files changed, 122 insertions(+), 68 deletions(-) (limited to 'src') diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index c827a8f07..fb0ac5923 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -118,6 +118,12 @@ void TheoryDatatypes::check(Effort e) { } if( e == EFFORT_FULL ) { + //check for cycles + checkCycles(); + if( d_conflict ){ + return; + } + //check for splits Debug("datatypes-split") << "Check for splits " << e << endl; bool addedFact = false; do { @@ -159,20 +165,19 @@ void TheoryDatatypes::check(Effort e) { } } } + /* if( !needSplit && mustSpecifyAssignment() ){ - // && //for the sake of termination, we must choose the constructor of a ground term //NEED GUARENTEE: groundTerm should not contain any subterms of the same type - //** TODO: this is probably not good enough, actually need fair enumeration strategy - /* + // TODO: this is probably not good enough, actually need fair enumeration strategy Node groundTerm = n.getType().mkGroundTerm(); int index = Datatype::indexOf( groundTerm.getOperator().toExpr() ); if( pcons[index] ){ consIndex = index; } needSplit = true; - */ } + */ if( needSplit && consIndex!=-1 ) { Node test = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[consIndex].getTester() ), n ); Trace("dt-split") << "*************Split for possible constructor " << dt[consIndex] << " for " << n << endl; @@ -446,10 +451,16 @@ void TheoryDatatypes::explain(TNode literal, std::vector& assumptions){ Debug("datatypes-explain") << "Explain " << literal << std::endl; bool polarity = literal.getKind() != kind::NOT; TNode atom = polarity ? literal : literal[0]; + std::vector tassumptions; if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) { - d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions); + d_equalityEngine.explainEquality(atom[0], atom[1], polarity, tassumptions); } else { - d_equalityEngine.explainPredicate(atom, polarity, assumptions); + d_equalityEngine.explainPredicate(atom, polarity, tassumptions); + } + for( unsigned i=0; iconflict( d_conflictNode ); d_conflict = true; } @@ -523,7 +534,7 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ if( cons1.getOperator()!=cons2.getOperator() ){ //check for clash d_conflictNode = explain( cons1.eqNode( cons2 ) ); - Debug("datatypes-conflict") << "CONFLICT: Clash conflict : " << d_conflictNode << std::endl; + Trace("dt-conflict") << "CONFLICT: Clash conflict : " << d_conflictNode << std::endl; d_out->conflict( d_conflictNode ); d_conflict = true; return; @@ -559,8 +570,7 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ explain( *i, assumptions ); explain( cons2.eqNode( (*i)[0][0] ), assumptions ); d_conflictNode = NodeManager::currentNM()->mkNode( AND, assumptions ); - Debug("datatypes-conflict") << "CONFLICT: Tester merge eq conflict : " << d_conflictNode << std::endl; - Debug("datatypes-conflict-temp") << "CONFLICT: Tester merge eq conflict : " << d_conflictNode << std::endl; + Trace("dt-conflict") << "CONFLICT: Tester merge eq conflict : " << d_conflictNode << std::endl; d_out->conflict( d_conflictNode ); d_conflict = true; return; @@ -615,12 +625,16 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ newRep = trep2; } bool result = d_cycle_check.addEdgeNode( oldRep, newRep ); - d_hasSeenCycle.set( d_hasSeenCycle.get() || result ); - Debug("datatypes-cycles") << "DtCyc: Equal " << oldRep << " -> " << newRep << " " << d_hasSeenCycle.get() << endl; - if( d_hasSeenCycle.get() ){ + //d_hasSeenCycle.set( d_hasSeenCycle.get() || result ); + Debug("datatypes-cycles") << "DtCyc: Equal " << oldRep << " -> " << newRep << " " << result << " " << d_hasSeenCycle.get() << endl; + if( result ){ checkCycles(); if( d_conflict ){ + Debug("datatypes-cycles-find") << "Cycle found." << std::endl; return; + }else{ + Debug("datatypes-cycles-find") << "WARNING : no cycle found." << std::endl; + d_cycle_check.debugPrint(); } } } @@ -694,7 +708,7 @@ void TheoryDatatypes::addTester( Node t, EqcInfo* eqc, Node n ){ explain( t, assumptions ); explain( eqc->d_constructor.get().eqNode( tt[0] ), assumptions ); d_conflictNode = NodeManager::currentNM()->mkNode( AND, assumptions ); - Debug("datatypes-conflict") << "CONFLICT: Tester eq conflict : " << d_conflictNode << std::endl; + Trace("dt-conflict") << "CONFLICT: Tester eq conflict : " << d_conflictNode << std::endl; d_out->conflict( d_conflictNode ); return; }else{ @@ -775,7 +789,7 @@ void TheoryDatatypes::addTester( Node t, EqcInfo* eqc, Node n ){ explain( t, assumptions ); explain( jt[0].eqNode( tt[0] ), assumptions ); d_conflictNode = NodeManager::currentNM()->mkNode( AND, assumptions ); - Debug("datatypes-conflict") << "CONFLICT: Tester conflict : " << d_conflictNode << std::endl; + Trace("dt-conflict") << "CONFLICT: Tester conflict : " << d_conflictNode << std::endl; d_out->conflict( d_conflictNode ); } } @@ -912,8 +926,11 @@ void TheoryDatatypes::collectTerms( Node n ) { if( n.getKind() == APPLY_CONSTRUCTOR ){ //we must take into account subterm relation when checking for cycles for( int i=0; i<(int)n.getNumChildren(); i++ ) { - Debug("datatypes-cycles") << "DtCyc: Subterm " << n << " -> " << n[i] << endl; bool result = d_cycle_check.addEdgeNode( n, n[i] ); + Debug("datatypes-cycles") << "DtCyc: Subterm " << n << " -> " << n[i] << " " << result << endl; + if( result && !d_hasSeenCycle.get() ){ + Debug("datatypes-cycles") << "FOUND CYCLE" << std::endl; + } d_hasSeenCycle.set( d_hasSeenCycle.get() || result ); } }else if( n.getKind() == APPLY_SELECTOR ){ @@ -941,7 +958,7 @@ void TheoryDatatypes::processNewTerm( Node n ){ Trace("dt-terms") << "Created term : " << n << std::endl; //see if it is rewritten to be something different Node rn = Rewriter::rewrite( n ); - if( rn!=n ){ + if( rn!=n && !areEqual( rn, n ) ){ Node eq = n.getType().isBoolean() ? rn.iffNode( n ) : rn.eqNode( n ); d_pending.push_back( eq ); d_pending_exp[ eq ] = NodeManager::currentNM()->mkConst( true ); @@ -1059,21 +1076,21 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){ int index = getLabelIndex( eqc, n ); const Datatype& dt = ((DatatypeType)(tt.getType()).toType()).getDatatype(); //must be finite or have a selector - //if( eqc->d_selectors || dt[ index ].isFinite() || mustSpecifyAssignment() ){ - //instantiate this equivalence class - eqc->d_inst = true; - Node tt_cons = getInstantiateCons( tt, dt, index ); - Node eq; - if( tt!=tt_cons ){ - eq = tt.eqNode( tt_cons ); - Debug("datatypes-inst") << "DtInstantiate : " << eqc << " " << eq << std::endl; - d_pending.push_back( eq ); - d_pending_exp[ eq ] = exp; - Trace("datatypes-infer") << "DtInfer : " << eq << " by " << exp << std::endl; - //eqc->d_inst.set( eq ); - d_infer.push_back( eq ); - d_infer_exp.push_back( exp ); - } + //if( eqc->d_selectors || dt[ index ].isFinite() ){ // || mustSpecifyAssignment() + //instantiate this equivalence class + eqc->d_inst = true; + Node tt_cons = getInstantiateCons( tt, dt, index ); + Node eq; + if( tt!=tt_cons ){ + eq = tt.eqNode( tt_cons ); + Debug("datatypes-inst") << "DtInstantiate : " << eqc << " " << eq << std::endl; + d_pending.push_back( eq ); + d_pending_exp[ eq ] = exp; + Trace("datatypes-infer") << "DtInfer : " << eq << " by " << exp << std::endl; + //eqc->d_inst.set( eq ); + d_infer.push_back( eq ); + d_infer_exp.push_back( exp ); + } //} //else{ // Debug("datatypes-inst") << "Do not instantiate" << std::endl; @@ -1086,26 +1103,38 @@ void TheoryDatatypes::checkCycles() { eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); while( !eqcs_i.isFinished() ){ Node eqc = (*eqcs_i); - map< Node, bool > visited; - std::vector< TNode > expl; - if( searchForCycle( eqc, eqc, visited, expl ) ) { - Assert( expl.size()>0 ); - if( expl.size() == 1 ){ - d_conflictNode = expl[ 0 ]; - }else{ - d_conflictNode = NodeManager::currentNM()->mkNode( AND, expl ); + if( eqc.getType().isDatatype() ) { + map< Node, bool > visited; + std::vector< TNode > expl; + Node cn = searchForCycle( eqc, eqc, visited, expl ); + //if we discovered a different cycle while searching this one + if( !cn.isNull() && cn!=eqc ){ + visited.clear(); + expl.clear(); + Node prev = cn; + cn = searchForCycle( cn, cn, visited, expl ); + Assert( prev==cn ); + } + + if( !cn.isNull() ) { + Assert( expl.size()>0 ); + if( expl.size() == 1 ){ + d_conflictNode = expl[ 0 ]; + }else{ + d_conflictNode = NodeManager::currentNM()->mkNode( AND, expl ); + } + Trace("dt-conflict") << "CONFLICT: Cycle conflict : " << d_conflictNode << std::endl; + d_out->conflict( d_conflictNode ); + d_conflict = true; + return; } - Debug("datatypes-conflict") << "CONFLICT: Cycle conflict : " << d_conflictNode << std::endl; - d_out->conflict( d_conflictNode ); - d_conflict = true; - return; } ++eqcs_i; } } //postcondition: if cycle detected, explanation is why n is a subterm of on -bool TheoryDatatypes::searchForCycle( Node n, Node on, +Node TheoryDatatypes::searchForCycle( Node n, Node on, map< Node, bool >& visited, std::vector< TNode >& explanation, bool firstTime ) { Debug("datatypes-cycle-check") << "Search for cycle " << n << " " << on << endl; @@ -1116,19 +1145,20 @@ bool TheoryDatatypes::searchForCycle( Node n, Node on, if( nn==on ){ Node lit = NodeManager::currentNM()->mkNode( EQUAL, n, nn ); explain( lit, explanation ); - return true; + return on; } }else{ nn = n; } if( visited.find( nn ) == visited.end() ) { visited[nn] = true; - EqcInfo* eqc = getOrMakeEqcInfo( nn ); + EqcInfo* eqc = getOrMakeEqcInfo( nn, false ); if( eqc ){ Node ncons = eqc->d_constructor.get(); if( !ncons.isNull() ) { for( int i=0; i<(int)ncons.getNumChildren(); i++ ) { - if( searchForCycle( ncons[i], on, visited, explanation, false ) ) { + Node cn = searchForCycle( ncons[i], on, visited, explanation, false ); + if( cn==on ) { if( Debug.isOn("datatypes-cycles") && !d_cycle_check.isConnectedNode( n, ncons[i] ) ){ Debug("datatypes-cycles") << "Cycle subterm: " << n << " is not -> " << ncons[i] << "!!!!" << std::endl; } @@ -1137,13 +1167,18 @@ bool TheoryDatatypes::searchForCycle( Node n, Node on, Node lit = NodeManager::currentNM()->mkNode( EQUAL, n, ncons ); explain( lit, explanation ); } - return true; + return on; + }else if( !cn.isNull() ){ + return cn; } } } } + visited.erase( nn ); + return Node::null(); + }else{ + return nn; } - return false; } bool TheoryDatatypes::mustSpecifyAssignment(){ diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 203782a79..225139b2d 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -219,7 +219,7 @@ private: void merge( Node t1, Node t2 ); /** for checking if cycles exist */ void checkCycles(); - bool searchForCycle( Node n, Node on, + Node searchForCycle( Node n, Node on, std::map< Node, bool >& visited, std::vector< TNode >& explanation, bool firstTime = true ); /** collect terms */ diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp index 96e8692f5..8db91da69 100644 --- a/src/util/datatype.cpp +++ b/src/util/datatype.cpp @@ -107,6 +107,7 @@ void Datatype::resolve(ExprManager* em, Node::fromExpr((*i).d_tester).setAttribute(DatatypeIndexAttr(), index++); } d_self = self; + //d_card = getCardinality(); } void Datatype::addConstructor(const DatatypeConstructor& c) { @@ -125,6 +126,10 @@ Cardinality Datatype::getCardinality() const throw(IllegalArgumentException) { for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { c += (*i).getCardinality(); } + //if( d_card!=c ){ + //std::cout << "Bad card " << std::endl; + //} + return c; } diff --git a/src/util/datatype.h b/src/util/datatype.h index c46c10c97..01558fd30 100644 --- a/src/util/datatype.h +++ b/src/util/datatype.h @@ -404,6 +404,7 @@ private: std::vector d_constructors; bool d_resolved; Type d_self; + Cardinality d_card; /** * Datatypes refer to themselves, recursively, and we have a @@ -616,7 +617,8 @@ inline Datatype::Datatype(std::string name) : d_params(), d_constructors(), d_resolved(false), - d_self() { + d_self(), + d_card(1) { } inline Datatype::Datatype(std::string name, const std::vector& params) : @@ -624,7 +626,8 @@ inline Datatype::Datatype(std::string name, const std::vector& params) : d_params(params), d_constructors(), d_resolved(false), - d_self() { + d_self(), + d_card(1) { } inline std::string Datatype::getName() const throw() { diff --git a/src/util/trans_closure.cpp b/src/util/trans_closure.cpp index 90b069485..970d2542e 100644 --- a/src/util/trans_closure.cpp +++ b/src/util/trans_closure.cpp @@ -37,16 +37,22 @@ TransitiveClosure::~TransitiveClosure() { bool TransitiveClosure::addEdge(unsigned i, unsigned j) { + Debug("trans-closure") << "Add edge " << i << " -> " << j << std::endl; // Check for loops Assert(i != j, "Cannot add self-loop"); - if (adjMatrix.size() > j && adjMatrix[j] != NULL && adjMatrix[j]->read(i)) { + if (adjIndex.get() > j && adjMatrix[j] != NULL && adjMatrix[j]->read(i)) { return true; } // Grow matrix if necessary unsigned maxSize = ((i > j) ? i : j) + 1; - while (maxSize > adjMatrix.size()) { - adjMatrix.push_back(NULL); + while (maxSize > adjIndex.get()) { + if( maxSize > adjMatrix.size() ){ + adjMatrix.push_back(NULL); + }else if( adjMatrix[adjIndex.get()]!=NULL ){ + adjMatrix[adjIndex.get()]->clear(); + } + adjIndex.set( adjIndex.get() + 1 ); } // Add edge from i to j and everything j can reach @@ -60,7 +66,7 @@ bool TransitiveClosure::addEdge(unsigned i, unsigned j) // Add edges from everything that can reach i to j and everything that j can reach unsigned k; - for (k = 0; k < adjMatrix.size(); ++k) { + for (k = 0; k < adjIndex.get(); ++k) { if (adjMatrix[k] != NULL && adjMatrix[k]->read(i)) { adjMatrix[k]->write(j); if (adjMatrix[j] != NULL) { @@ -74,7 +80,7 @@ bool TransitiveClosure::addEdge(unsigned i, unsigned j) bool TransitiveClosure::isConnected(unsigned i, unsigned j) { - if( i>=adjMatrix.size() || j>adjMatrix.size() ){ + if( i>=adjIndex.get() || j>adjIndex.get() ){//adjMatrix.size() ){ return false; }else{ return adjMatrix[i] != NULL && adjMatrix[i]->read(j); @@ -84,15 +90,15 @@ bool TransitiveClosure::isConnected(unsigned i, unsigned j) void TransitiveClosure::debugPrintMatrix() { unsigned i,j; - for (i = 0; i < adjMatrix.size(); ++i) { - for (j = 0; j < adjMatrix.size(); ++j) { + for (i = 0; i < adjIndex.get(); ++i) { + for (j = 0; j < adjIndex.get(); ++j) { if (adjMatrix[i] != NULL && adjMatrix[i]->read(j)) { Debug("trans-closure") << "1 "; } else Debug("trans-closure") << "0 "; } Debug("trans-closure") << endl; - } + } } unsigned TransitiveClosureNode::getId( Node i ){ @@ -108,10 +114,14 @@ unsigned TransitiveClosureNode::getId( Node i ){ void TransitiveClosureNode::debugPrint(){ for( int i=0; i<(int)currEdges.size(); i++ ){ - Debug("trans-closure") << "currEdges[ " << i << " ] = " + Debug("trans-closure") << "currEdges[ " << i << " ] = " << currEdges[i].first << " -> " << currEdges[i].second; + int id1 = getId( currEdges[i].first ); + int id2 = getId( currEdges[i].second ); + Debug("trans-closure") << " { " << id1 << " -> " << id2 << " } "; Debug("trans-closure") << std::endl; } + debugPrintMatrix(); } diff --git a/src/util/trans_closure.h b/src/util/trans_closure.h index ce846637d..14e7ab95f 100644 --- a/src/util/trans_closure.h +++ b/src/util/trans_closure.h @@ -57,17 +57,17 @@ protected: CDBV* next() { return d_next; } public: - CDBV(context::Context* context) : + CDBV(context::Context* context) : ContextObj(context), d_data(0), d_next(NULL) {} - ~CDBV() { + ~CDBV() { if (d_next != NULL) { d_next->deleteSelf(); } destroy(); } - + void clear() { d_data = 0; if( d_next ) d_next->clear(); } bool read(unsigned index) { if (index < 64) return (d_data & (uint64_t(1) << index)) != 0; else if (d_next == NULL) return false; @@ -88,7 +88,7 @@ public: makeCurrent(); d_next = new(true) CDBV(getContext()); d_next->write(index - 64); - } + } } void merge(CDBV* pcdbv) { @@ -108,9 +108,10 @@ public: class TransitiveClosure { context::Context* d_context; std::vector adjMatrix; + context::CDO adjIndex; public: - TransitiveClosure(context::Context* context) : d_context(context) {} + TransitiveClosure(context::Context* context) : d_context(context), adjIndex(context,0) {} virtual ~TransitiveClosure(); /* Add an edge from node i to node j. Return false if successful, true if this edge would create a cycle */ @@ -130,7 +131,7 @@ class TransitiveClosureNode : public TransitiveClosure{ //for debugging context::CDList< std::pair< Node, Node > > currEdges; public: - TransitiveClosureNode(context::Context* context) : + TransitiveClosureNode(context::Context* context) : TransitiveClosure(context), d_counter( context, 0 ), nodeMap( context ), currEdges(context) {} ~TransitiveClosureNode(){} -- cgit v1.2.3 From 29923ecc0467f52a8eb6e318b874269054b956e5 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 9 Oct 2013 12:26:11 -0500 Subject: More improvements to datatypes, eager selector collapsing, improved collect model info. Also fix bug in model post-processor. --- src/smt/model_postprocessor.cpp | 7 +- src/theory/datatypes/theory_datatypes.cpp | 663 +++++++++++++++++------------- src/theory/datatypes/theory_datatypes.h | 18 +- 3 files changed, 388 insertions(+), 300 deletions(-) (limited to 'src') diff --git a/src/smt/model_postprocessor.cpp b/src/smt/model_postprocessor.cpp index cbabc9542..c61a61940 100644 --- a/src/smt/model_postprocessor.cpp +++ b/src/smt/model_postprocessor.cpp @@ -9,9 +9,9 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief + ** \brief + ** ** - ** **/ #include "smt/model_postprocessor.h" @@ -92,6 +92,9 @@ Node ModelPostprocessor::rewriteAs(TNode n, TypeNode asType) { return n; } NodeBuilder<> b(n.getKind()); + if (n.getMetaKind() == kind::metakind::PARAMETERIZED) { + b << n.getOperator(); + } TypeNode::iterator t = asType.begin(); for(TNode::iterator i = n.begin(); i != n.end(); ++i, ++t) { Assert(t != asType.end()); diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index fb0ac5923..797445e7e 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -47,8 +47,8 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, d_infer_exp(c), d_notify( *this ), d_equalityEngine(d_notify, c, "theory::datatypes::TheoryDatatypes"), - d_selector_apps( c ), d_labels( c ), + d_selector_apps( c ), d_conflict( c, false ), d_collectTermsCache( c ){ @@ -83,6 +83,10 @@ TheoryDatatypes::EqcInfo* TheoryDatatypes::getOrMakeEqcInfo( Node n, bool doMake if( n.getKind()==APPLY_CONSTRUCTOR ){ ei->d_constructor = n; } + //add to selectors + NodeList* sel = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false, + ContextMemoryAllocator(getSatContext()->getCMM()) ); + d_selector_apps.insertDataFromContextMemory( n, sel ); return ei; }else{ return NULL; @@ -201,6 +205,7 @@ void TheoryDatatypes::check(Effort e) { Trace("datatypes-debug") << "Flush pending facts..." << std::endl; addedFact = !d_pending.empty() || !d_pending_merge.empty(); flushPendingFacts(); + /* if( !d_conflict ){ if( options::dtRewriteErrorSel() ){ bool innerAddedFact = false; @@ -211,6 +216,7 @@ void TheoryDatatypes::check(Effort e) { }while( !d_conflict && innerAddedFact ); } } + */ }while( !d_conflict && addedFact ); Trace("datatypes-debug") << "Finished. " << d_conflict << std::endl; if( !d_conflict ){ @@ -467,13 +473,7 @@ void TheoryDatatypes::explain(TNode literal, std::vector& assumptions){ Node TheoryDatatypes::explain( TNode literal ){ std::vector< TNode > assumptions; explain( literal, assumptions ); - if( assumptions.empty() ){ - return NodeManager::currentNM()->mkConst( true ); - }else if( assumptions.size()==1 ){ - return assumptions[0]; - }else{ - return NodeManager::currentNM()->mkNode( kind::AND, assumptions ); - } + return mkAnd( assumptions ); } /** Conflict when merging two constants */ @@ -519,9 +519,6 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ trep2 = eqc2->d_constructor.get(); } EqcInfo* eqc1 = getOrMakeEqcInfo( t1 ); - - - if( eqc1 ){ if( !eqc1->d_constructor.get().isNull() ){ trep1 = eqc1->d_constructor.get(); @@ -529,6 +526,7 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ //check for clash Node cons1 = eqc1->d_constructor; Node cons2 = eqc2->d_constructor; + //if both have constructor, then either clash or unification if( !cons1.isNull() && !cons2.isNull() ){ Debug("datatypes-debug") << "Constructors : " << cons1 << " " << cons2 << std::endl; if( cons1.getOperator()!=cons2.getOperator() ){ @@ -558,29 +556,11 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ } if( cons1.isNull() && !cons2.isNull() ){ Debug("datatypes-debug") << "Must check if it is okay to set the constructor." << std::endl; - NodeListMap::iterator lbl_i = d_labels.find( t1 ); - if( lbl_i != d_labels.end() ){ - size_t constructorIndex = Datatype::indexOf(cons2.getOperator().toExpr()); - NodeList* lbl = (*lbl_i).second; - for( NodeList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) { - if( (*i).getKind()==NOT ){ - if( Datatype::indexOf( (*i)[0].getOperator().toExpr() )==constructorIndex ){ - Node n = *i; - std::vector< TNode > assumptions; - explain( *i, assumptions ); - explain( cons2.eqNode( (*i)[0][0] ), assumptions ); - d_conflictNode = NodeManager::currentNM()->mkNode( AND, assumptions ); - Trace("dt-conflict") << "CONFLICT: Tester merge eq conflict : " << d_conflictNode << std::endl; - d_out->conflict( d_conflictNode ); - d_conflict = true; - return; - } - } - } - } - checkInst = true; - eqc1->d_constructor.set( eqc2->d_constructor ); + addConstructor( eqc2->d_constructor.get(), eqc1, t1 ); + if( d_conflict ){ + return; + } } }else{ Debug("datatypes-debug") << "No eqc info for " << t1 << ", must create" << std::endl; @@ -588,10 +568,10 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ eqc1 = getOrMakeEqcInfo( t1, true ); eqc1->d_inst.set( eqc2->d_inst ); eqc1->d_constructor.set( eqc2->d_constructor ); + eqc1->d_selectors.set( eqc2->d_selectors ); } - //merge labels NodeListMap::iterator lbl_i = d_labels.find( t2 ); if( lbl_i != d_labels.end() ){ @@ -610,6 +590,14 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ eqc1->d_selectors = true; checkInst = true; } + NodeListMap::iterator sel_i = d_selector_apps.find( t2 ); + if( sel_i != d_selector_apps.end() ){ + Debug("datatypes-debug") << "Merge selectors from " << eqc2 << " " << t2 << std::endl; + NodeList* sel = (*sel_i).second; + for( NodeList::const_iterator j = sel->begin(); j != sel->end(); ++j ){ + addSelector( *j, eqc1, t1, eqc2->d_constructor.get().isNull() ); + } + } if( checkInst ){ instantiate( eqc1, t1 ); if( d_conflict ){ @@ -691,107 +679,184 @@ void TheoryDatatypes::getPossibleCons( EqcInfo* eqc, Node n, std::vector< bool > } void TheoryDatatypes::addTester( Node t, EqcInfo* eqc, Node n ){ - if( !d_conflict ){ - Debug("datatypes-labels") << "Add tester " << t << " " << n << " " << eqc << std::endl; - bool tpolarity = t.getKind()!=NOT; - Node tt = ( t.getKind() == NOT ) ? t[0] : t; - int ttindex = Datatype::indexOf( tt.getOperator().toExpr() ); - Node j, jt; - if( hasLabel( eqc, n ) ){ - //if we already know the constructor type, check whether it is in conflict or redundant - int jtindex = getLabelIndex( eqc, n ); - if( (jtindex==ttindex)!=tpolarity ){ - d_conflict = true; - if( !eqc->d_constructor.get().isNull() ){ - //conflict because equivalence class contains a constructor - std::vector< TNode > assumptions; - explain( t, assumptions ); - explain( eqc->d_constructor.get().eqNode( tt[0] ), assumptions ); - d_conflictNode = NodeManager::currentNM()->mkNode( AND, assumptions ); - Trace("dt-conflict") << "CONFLICT: Tester eq conflict : " << d_conflictNode << std::endl; - d_out->conflict( d_conflictNode ); - return; - }else{ - //conflict because the existing label is contradictory - j = getLabel( n ); - jt = j; - } - }else{ + Debug("datatypes-debug") << "Add tester : " << t << " to eqc(" << n << ")" << std::endl; + Debug("datatypes-labels") << "Add tester " << t << " " << n << " " << eqc << std::endl; + bool tpolarity = t.getKind()!=NOT; + Node tt = ( t.getKind() == NOT ) ? t[0] : t; + int ttindex = Datatype::indexOf( tt.getOperator().toExpr() ); + Node j, jt; + if( hasLabel( eqc, n ) ){ + //if we already know the constructor type, check whether it is in conflict or redundant + int jtindex = getLabelIndex( eqc, n ); + if( (jtindex==ttindex)!=tpolarity ){ + d_conflict = true; + if( !eqc->d_constructor.get().isNull() ){ + //conflict because equivalence class contains a constructor + std::vector< TNode > assumptions; + explain( t, assumptions ); + explain( eqc->d_constructor.get().eqNode( tt[0] ), assumptions ); + d_conflictNode = mkAnd( assumptions ); + Trace("dt-conflict") << "CONFLICT: Tester eq conflict : " << d_conflictNode << std::endl; + d_out->conflict( d_conflictNode ); return; + }else{ + //conflict because the existing label is contradictory + j = getLabel( n ); + jt = j; } }else{ - //otherwise, scan list of labels - NodeListMap::iterator lbl_i = d_labels.find( n ); - Assert( lbl_i != d_labels.end() ); - NodeList* lbl = (*lbl_i).second; - for( NodeList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) { - Assert( (*i).getKind()==NOT ); - j = *i; - jt = j[0]; - int jtindex = Datatype::indexOf( jt.getOperator().toExpr() ); - if( jtindex==ttindex ){ - if( tpolarity ){ //we are in conflict - d_conflict = true; - break; - }else{ //it is redundant - return; - } + return; + } + }else{ + //otherwise, scan list of labels + NodeListMap::iterator lbl_i = d_labels.find( n ); + Assert( lbl_i != d_labels.end() ); + NodeList* lbl = (*lbl_i).second; + for( NodeList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) { + Assert( (*i).getKind()==NOT ); + j = *i; + jt = j[0]; + int jtindex = Datatype::indexOf( jt.getOperator().toExpr() ); + if( jtindex==ttindex ){ + if( tpolarity ){ //we are in conflict + d_conflict = true; + break; + }else{ //it is redundant + return; } } - if( !d_conflict ){ - Debug("datatypes-labels") << "Add to labels " << t << std::endl; - lbl->push_back( t ); - const Datatype& dt = ((DatatypeType)(tt[0].getType()).toType()).getDatatype(); - Debug("datatypes-labels") << "Labels at " << lbl->size() << " / " << dt.getNumConstructors() << std::endl; - if( tpolarity ){ - instantiate( eqc, n ); - }else{ - //check if we have reached the maximum number of testers - // in this case, add the positive tester - if( lbl->size()==dt.getNumConstructors()-1 ){ - std::vector< bool > pcons; - getPossibleCons( eqc, n, pcons ); - int testerIndex = -1; - for( int i=0; i<(int)pcons.size(); i++ ) { - if( pcons[i] ){ - testerIndex = i; - break; - } + } + if( !d_conflict ){ + Debug("datatypes-labels") << "Add to labels " << t << std::endl; + lbl->push_back( t ); + const Datatype& dt = ((DatatypeType)(tt[0].getType()).toType()).getDatatype(); + Debug("datatypes-labels") << "Labels at " << lbl->size() << " / " << dt.getNumConstructors() << std::endl; + if( tpolarity ){ + instantiate( eqc, n ); + }else{ + //check if we have reached the maximum number of testers + // in this case, add the positive tester + if( lbl->size()==dt.getNumConstructors()-1 ){ + std::vector< bool > pcons; + getPossibleCons( eqc, n, pcons ); + int testerIndex = -1; + for( int i=0; i<(int)pcons.size(); i++ ) { + if( pcons[i] ){ + testerIndex = i; + break; } - Assert( testerIndex!=-1 ); - //we must explain why each term in the set of testers for this equivalence class is equal - std::vector< Node > eq_terms; - NodeBuilder<> nb(kind::AND); - for( NodeList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) { - nb << (*i); - if( std::find( eq_terms.begin(), eq_terms.end(), (*i)[0][0] )==eq_terms.end() ){ - eq_terms.push_back( (*i)[0][0] ); - if( (*i)[0][0]!=tt[0] ){ - nb << (*i)[0][0].eqNode( tt[0] ); - } + } + Assert( testerIndex!=-1 ); + //we must explain why each term in the set of testers for this equivalence class is equal + std::vector< Node > eq_terms; + NodeBuilder<> nb(kind::AND); + for( NodeList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) { + nb << (*i); + if( std::find( eq_terms.begin(), eq_terms.end(), (*i)[0][0] )==eq_terms.end() ){ + eq_terms.push_back( (*i)[0][0] ); + if( (*i)[0][0]!=tt[0] ){ + nb << (*i)[0][0].eqNode( tt[0] ); } } - Node t_concl = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[unsigned(testerIndex)].getTester() ), tt[0] ); - Node t_concl_exp = ( nb.getNumChildren() == 1 ) ? nb.getChild( 0 ) : nb; - d_pending.push_back( t_concl ); - d_pending_exp[ t_concl ] = t_concl_exp; - Trace("datatypes-infer") << "DtInfer : " << t_concl << " by " << t_concl_exp << std::endl; - d_infer.push_back( t_concl ); - d_infer_exp.push_back( t_concl_exp ); - return; } + Node t_concl = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[unsigned(testerIndex)].getTester() ), tt[0] ); + Node t_concl_exp = ( nb.getNumChildren() == 1 ) ? nb.getChild( 0 ) : nb; + d_pending.push_back( t_concl ); + d_pending_exp[ t_concl ] = t_concl_exp; + Trace("datatypes-infer") << "DtInfer : " << t_concl << " by " << t_concl_exp << std::endl; + d_infer.push_back( t_concl ); + d_infer_exp.push_back( t_concl_exp ); + return; } } } - if( d_conflict ){ - std::vector< TNode > assumptions; - explain( j, assumptions ); - explain( t, assumptions ); - explain( jt[0].eqNode( tt[0] ), assumptions ); - d_conflictNode = NodeManager::currentNM()->mkNode( AND, assumptions ); - Trace("dt-conflict") << "CONFLICT: Tester conflict : " << d_conflictNode << std::endl; - d_out->conflict( d_conflictNode ); + } + if( d_conflict ){ + std::vector< TNode > assumptions; + explain( j, assumptions ); + explain( t, assumptions ); + explain( jt[0].eqNode( tt[0] ), assumptions ); + d_conflictNode = mkAnd( assumptions ); + Trace("dt-conflict") << "CONFLICT: Tester conflict : " << d_conflictNode << std::endl; + d_out->conflict( d_conflictNode ); + } +} + +void TheoryDatatypes::addSelector( Node s, EqcInfo* eqc, Node n, bool assertFacts ) { + Debug("datatypes-debug") << "Add selector : " << s << " to eqc(" << n << ")" << std::endl; + //check to see if it is redundant + NodeListMap::iterator sel_i = d_selector_apps.find( n ); + Assert( sel_i != d_selector_apps.end() ); + if( sel_i != d_selector_apps.end() ){ + NodeList* sel = (*sel_i).second; + for( NodeList::const_iterator j = sel->begin(); j != sel->end(); ++j ){ + Node ss = *j; + if( s.getOperator()==ss.getOperator() ){ + return; + } } + //add it to the vector + sel->push_back( s ); + eqc->d_selectors = true; + } + if( assertFacts && !eqc->d_constructor.get().isNull() ){ + //conclude the collapsed merge + collapseSelector( s, eqc->d_constructor.get() ); + } +} + +void TheoryDatatypes::addConstructor( Node c, EqcInfo* eqc, Node n ){ + Debug("datatypes-debug") << "Add constructor : " << c << " to eqc(" << n << ")" << std::endl; + Assert( eqc->d_constructor.get().isNull() ); + //check labels + NodeListMap::iterator lbl_i = d_labels.find( n ); + if( lbl_i != d_labels.end() ){ + size_t constructorIndex = Datatype::indexOf(c.getOperator().toExpr()); + NodeList* lbl = (*lbl_i).second; + for( NodeList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) { + if( (*i).getKind()==NOT ){ + if( Datatype::indexOf( (*i)[0].getOperator().toExpr() )==constructorIndex ){ + Node n = *i; + std::vector< TNode > assumptions; + explain( *i, assumptions ); + explain( c.eqNode( (*i)[0][0] ), assumptions ); + d_conflictNode = mkAnd( assumptions ); + Trace("dt-conflict") << "CONFLICT: Tester merge eq conflict : " << d_conflictNode << std::endl; + d_out->conflict( d_conflictNode ); + d_conflict = true; + return; + } + } + } + } + //check selectors + NodeListMap::iterator sel_i = d_selector_apps.find( n ); + if( sel_i != d_selector_apps.end() ){ + NodeList* sel = (*sel_i).second; + for( NodeList::const_iterator j = sel->begin(); j != sel->end(); ++j ){ + //collapse the selector + collapseSelector( *j, c ); + } + } + eqc->d_constructor.set( c ); +} + +void TheoryDatatypes::collapseSelector( Node s, Node c ) { + Node r = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR, s.getOperator(), c ); + Node rr = Rewriter::rewrite( r ); + //if( r!=rr ){ + //Node eq_exp = NodeManager::currentNM()->mkConst(true); + //Node eq = r.getType().isBoolean() ? r.iffNode( rr ) : r.eqNode( rr ); + if( s!=rr ){ + Node eq_exp = c.eqNode( s[0] ); + Node eq = rr.getType().isBoolean() ? s.iffNode( rr ) : s.eqNode( rr ); + + + d_pending.push_back( eq ); + d_pending_exp[ eq ] = eq_exp; + Trace("datatypes-infer") << "DtInfer : " << eq << " by " << eq_exp << " (collapse selector)" << std::endl; + d_infer.push_back( eq ); + d_infer_exp.push_back( eq_exp ); } } @@ -816,12 +881,13 @@ void TheoryDatatypes::computeCareGraph(){ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ Trace("dt-model") << std::endl; printModelDebug( "dt-model" ); + Trace("dt-model") << std::endl; m->assertEqualityEngine( &d_equalityEngine ); - + Trace("dt-cmi") << "Datatypes : Collect model info " << std::endl; +/* std::vector< TypeEnumerator > vec; std::map< TypeNode, int > tes; - Trace("dt-cmi") << "Datatypes : Collect model info " << std::endl; - + */ //get all constructors eq::EqClassesIterator eqccs_i = eq::EqClassesIterator( &d_equalityEngine ); std::vector< Node > cons; @@ -830,90 +896,139 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ //for all equivalence classes that are datatypes if( DatatypesRewriter::isTermDatatype( eqc ) ){ EqcInfo* ei = getOrMakeEqcInfo( eqc ); - if( ei ){ - if( !ei->d_constructor.get().isNull() ){ - cons.push_back( ei->d_constructor.get() ); - } + if( !ei->d_constructor.get().isNull() ){ + cons.push_back( ei->d_constructor.get() ); } } ++eqccs_i; } //must choose proper representatives + std::vector< Node > nodes; eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); while( !eqcs_i.isFinished() ){ Node eqc = (*eqcs_i); //for all equivalence classes that are datatypes if( DatatypesRewriter::isTermDatatype( eqc ) ){ EqcInfo* ei = getOrMakeEqcInfo( eqc ); - if( ei ){ - if( !ei->d_constructor.get().isNull() ){ - //specify that we should use the constructor as the representative - //m->assertRepresentative( ei->d_constructor.get() ); - }else{ - Trace("dt-cmi") << "NOTICE : Datatypes: no constructor in equivalence class " << eqc << std::endl; - Trace("dt-cmi") << " Type : " << eqc.getType() << std::endl; - - std::vector< bool > pcons; - getPossibleCons( ei, eqc, pcons ); - Trace("dt-cmi") << "Possible constructors : "; - for( unsigned i=0; id_constructor.get().isNull() ){ + //specify that we should use the constructor as the representative + //m->assertRepresentative( ei->d_constructor.get() ); + }else{ + nodes.push_back( eqc ); + } + } + ++eqcs_i; + } + unsigned index = 0; + while( indexareEqual( cons[i][j], neqc[j] ) ){ + diff = true; + break; + } + } + if( !diff ){ + Trace("dt-cmi-debug") << "...Already equivalent modulo equality to " << cons[i] << std::endl; + success = false; + break; + } } - Trace("dt-cmi") << std::endl; - - if( tes.find( eqc.getType() )==tes.end() ){ - tes[eqc.getType()]=vec.size(); - vec.push_back( TypeEnumerator( eqc.getType() ) ); + } + }while( !success ); + }else{ + Trace("dt-cmi") << "NOTICE : Datatypes: no constructor in equivalence class " << eqc << std::endl; + Trace("dt-cmi") << " Type : " << eqc.getType() << std::endl; + EqcInfo* ei = getOrMakeEqcInfo( eqc ); + std::vector< bool > pcons; + getPossibleCons( ei, eqc, pcons ); + Trace("dt-cmi") << "Possible constructors : "; + for( unsigned i=0; iareEqual( cons[i][j], n[j] ) ){ + diff = true; + break; + } + } + if( !diff ){ + Trace("dt-cmi-debug") << "...Already equivalent modulo equality to " << cons[i] << std::endl; + success = false; + break; + } + } } - bool success; - Node n; - do { - success = true; - Assert( !vec[tes[eqc.getType()]].isFinished() ); - n = *vec[tes[eqc.getType()]]; - ++vec[tes[eqc.getType()]]; - - //applyTypeAscriptions( n, eqc.getType() ); - - Trace("dt-cmi-debug") << "Try " << n << "..." << std::endl; - //check if it is consistent with labels - size_t constructorIndex = Datatype::indexOf(n.getOperator().toExpr()); - if( constructorIndexareEqual( cons[i][j], n[j] ) ){ - diff = true; - break; - } - } - if( !diff ){ - Trace("dt-cmi-debug") << "...Already equivalent modulo equality to " << cons[i] << std::endl; - success = false; - break; - } + }else{ + Trace("dt-cmi-debug") << "...Not consistent with labels" << std::endl; + success = false; + } + }while( !success ); + */ + const Datatype& dt = ((DatatypeType)(eqc.getType()).toType()).getDatatype(); + for( unsigned r=0; r<2; r++ ){ + if( neqc.isNull() ){ + for( unsigned i=0; iassertRepresentative( n ); - m->assertEquality( eqc, n, true ); - + } } - }else{ - Trace("model-warn") << "WARNING: Datatypes: no equivalence class info for " << eqc << std::endl; - Trace("model-warn") << " Type : " << eqc.getType() << std::endl; } } - ++eqcs_i; + Assert( !neqc.isNull() ); + Trace("dt-cmi") << "Assign : " << neqc << std::endl; + m->assertEquality( eqc, neqc, true ); + //m->assertRepresentative( neqc ); + cons.push_back( neqc ); + ++index; } + } @@ -932,24 +1047,23 @@ void TheoryDatatypes::collectTerms( Node n ) { Debug("datatypes-cycles") << "FOUND CYCLE" << std::endl; } d_hasSeenCycle.set( d_hasSeenCycle.get() || result ); + //Node r = getRepresentative( n[i] ); + //EqcInfo* eqc = getOrMakeEqcInfo( r, true ); + //eqc->d_selectors = true; } }else if( n.getKind() == APPLY_SELECTOR ){ - if( d_selector_apps.find( n )==d_selector_apps.end() ){ - d_selector_apps[n] = false; - //we must also record which selectors exist - Debug("datatypes") << " Found selector " << n << endl; - if (n.getType().isBoolean()) { - d_equalityEngine.addTriggerPredicate( n ); - }else{ - d_equalityEngine.addTerm( n ); - } - Node rep = getRepresentative( n[0] ); - EqcInfo* eqc = getOrMakeEqcInfo( rep, true ); - if( !eqc->d_selectors ){ - eqc->d_selectors = true; - instantiate( eqc, rep ); - } + //we must also record which selectors exist + Debug("datatypes") << " Found selector " << n << endl; + if (n.getType().isBoolean()) { + d_equalityEngine.addTriggerPredicate( n ); + }else{ + d_equalityEngine.addTerm( n ); } + Node rep = getRepresentative( n[0] ); + //record it in the selectors + EqcInfo* eqc = getOrMakeEqcInfo( rep, true ); + //add it to the eqc info + addSelector( n, eqc, rep ); } } } @@ -967,20 +1081,35 @@ void TheoryDatatypes::processNewTerm( Node n ){ } } -Node TheoryDatatypes::getInstantiateCons( Node n, const Datatype& dt, int index ){ +Node TheoryDatatypes::getInstantiateCons( Node n, const Datatype& dt, int index, bool mkVar, bool isActive ){ //if( !d_inst_map[n][index].isNull() ){ // return d_inst_map[n][index]; //}else{ //add constructor to equivalence class + Type tspec; + if( dt.isParametric() ){ + tspec = dt[index].getSpecializedConstructorType(n.getType().toType()); + } std::vector< Node > children; children.push_back( Node::fromExpr( dt[index].getConstructor() ) ); for( int i=0; i<(int)dt[index].getNumArgs(); i++ ){ Node nc = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, Node::fromExpr( dt[index][i].getSelector() ), n ); + if( mkVar ){ + TypeNode tn = nc.getType(); + if( dt.isParametric() ){ + tn = TypeNode::fromType( tspec )[i]; + } + nc = NodeManager::currentNM()->mkSkolem( "m_$$", tn, "created during model gen" ); + } children.push_back( nc ); - processNewTerm( nc ); + if( isActive ){ + processNewTerm( nc ); + } } Node n_ic = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children ); - collectTerms( n_ic ); + if( isActive ){ + collectTerms( n_ic ); + } //add type ascription for ambiguous constructor types if(!n_ic.getType().isComparableTo(n.getType())) { Assert( dt.isParametric() ); @@ -994,72 +1123,11 @@ Node TheoryDatatypes::getInstantiateCons( Node n, const Datatype& dt, int index Assert( n_ic.getType()==n.getType() ); } n_ic = Rewriter::rewrite( n_ic ); + Debug("dt-enum") << "Made instantiate cons " << n_ic << std::endl; //d_inst_map[n][index] = n_ic; return n_ic; //} } -/* -Node TheoryDatatypes::applyTypeAscriptions( Node n, TypeNode tn ){ - Debug("dt-ta-debug") << "Apply type ascriptions " << n << " " << tn << std::endl; - if( n.getKind()==APPLY_CONSTRUCTOR ){ - //add type ascription for ambiguous constructor types - if(!n.getType().isComparableTo(tn)) { - size_t constructorIndex = Datatype::indexOf(n.getOperator().toExpr()); - const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - Assert( dt.isParametric() ); - Debug("dt-ta-debug") << "Ambiguous type for " << n << ", ascribe to " << tn << std::endl; - Debug("dt-ta-debug") << "Constructor is " << dt[constructorIndex] << std::endl; - Type tspec = dt[constructorIndex].getSpecializedConstructorType(tn.toType()); - Debug("dt-ta-debug") << "Type specification is " << tspec << std::endl; - Node op = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, - NodeManager::currentNM()->mkConst(AscriptionType(tspec)), n.getOperator() ); - std::vector< Node > children; - children.push_back( op ); - for( unsigned i=0; imkNode( APPLY_CONSTRUCTOR, children ) ); - Assert( n.getType()==tn ); - return n; - } - }else{ - if( n.getType()!=tn ){ - Debug("dt-ta-debug") << "Bad type : " << n.getType() << std::endl; - } - } - return n; -} -*/ -void TheoryDatatypes::collapseSelectors(){ - //must check incorrect applications of selectors - for( BoolMap::iterator it = d_selector_apps.begin(); it != d_selector_apps.end(); ++it ){ - if( !(*it).second ){ - Node n = getRepresentative( (*it).first[0] ); - Trace("datatypes-collapse") << "Datatypes collapse selector? : " << n << std::endl; - EqcInfo* ei = getOrMakeEqcInfo( n, true ); - if( ei ){ - if( !ei->d_constructor.get().isNull() ){ - Node op = (*it).first.getOperator(); - Node cons = ei->d_constructor; - Node sn = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR, op, cons ); - Node s = Rewriter::rewrite( sn ); - if( sn!=s ){ - Node eq = s.getType().isBoolean() ? s.iffNode( sn ) : s.eqNode( sn ); - d_pending.push_back( eq ); - d_pending_exp[ eq ] = NodeManager::currentNM()->mkConst( true ); - Trace("datatypes-infer") << "DtInfer : " << eq << ", by rewrite" << std::endl; - d_infer.push_back( eq ); - } - d_selector_apps[ (*it).first ] = true; - }else{ - Trace("datatypes-collapse") << "No constructor." << std::endl; - } - }else{ - Trace("datatypes-collapse") << "No e info." << std::endl; - } - } - } -} void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){ //add constructor to equivalence class if not done so already @@ -1103,7 +1171,7 @@ void TheoryDatatypes::checkCycles() { eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); while( !eqcs_i.isFinished() ){ Node eqc = (*eqcs_i); - if( eqc.getType().isDatatype() ) { + if( DatatypesRewriter::isTermDatatype( eqc ) ) { map< Node, bool > visited; std::vector< TNode > expl; Node cn = searchForCycle( eqc, eqc, visited, expl ); @@ -1118,11 +1186,7 @@ void TheoryDatatypes::checkCycles() { if( !cn.isNull() ) { Assert( expl.size()>0 ); - if( expl.size() == 1 ){ - d_conflictNode = expl[ 0 ]; - }else{ - d_conflictNode = NodeManager::currentNM()->mkNode( AND, expl ); - } + d_conflictNode = mkAnd( expl ); Trace("dt-conflict") << "CONFLICT: Cycle conflict : " << d_conflictNode << std::endl; d_out->conflict( d_conflictNode ); d_conflict = true; @@ -1290,30 +1354,45 @@ void TheoryDatatypes::printModelDebug( const char* c ){ EqcInfo* ei = getOrMakeEqcInfo( eqc ); if( ei ){ Trace( c ) << " Instantiated : " << ei->d_inst.get() << std::endl; - if( ei->d_constructor.get().isNull() ){ - Trace("debug-model-warn") << eqc << " has no constructor in equivalence class!" << std::endl; - Trace("debug-model-warn") << " Type : " << eqc.getType() << std::endl; - Trace( c ) << " Constructor : " << std::endl; - Trace( c ) << " Labels : "; - if( hasLabel( ei, eqc ) ){ - Trace( c ) << getLabel( eqc ); - }else{ - NodeListMap::iterator lbl_i = d_labels.find( eqc ); - if( lbl_i != d_labels.end() ){ - NodeList* lbl = (*lbl_i).second; - for( NodeList::const_iterator j = lbl->begin(); j != lbl->end(); j++ ){ - Trace( c ) << *j << " "; - } + Trace( c ) << " Constructor : "; + if( !ei->d_constructor.get().isNull() ){ + Trace( c )<< ei->d_constructor.get(); + } + Trace( c ) << std::endl << " Labels : "; + if( hasLabel( ei, eqc ) ){ + Trace( c ) << getLabel( eqc ); + }else{ + NodeListMap::iterator lbl_i = d_labels.find( eqc ); + if( lbl_i != d_labels.end() ){ + NodeList* lbl = (*lbl_i).second; + for( NodeList::const_iterator j = lbl->begin(); j != lbl->end(); j++ ){ + Trace( c ) << *j << " "; } } - Trace( c ) << std::endl; - }else{ - Trace( c ) << " Constructor : " << ei->d_constructor.get() << std::endl; } - Trace( c ) << " Selectors : " << ( ei->d_selectors ? "yes" : "no" ) << std::endl; + Trace( c ) << std::endl; + Trace( c ) << " Selectors : " << ( ei->d_selectors ? "yes, " : "no " ); + NodeListMap::iterator sel_i = d_selector_apps.find( eqc ); + if( sel_i != d_selector_apps.end() ){ + NodeList* sel = (*sel_i).second; + for( NodeList::const_iterator j = sel->begin(); j != sel->end(); j++ ){ + Trace( c ) << *j << " "; + } + } + Trace( c ) << std::endl; } } } ++eqcs_i; } } + +Node TheoryDatatypes::mkAnd( std::vector< TNode >& assumptions ) { + if( assumptions.empty() ){ + return NodeManager::currentNM()->mkConst( true ); + }else if( assumptions.size()==1 ){ + return assumptions[0]; + }else{ + return NodeManager::currentNM()->mkNode( AND, assumptions ); + } +} \ No newline at end of file diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 225139b2d..4f061507c 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -51,6 +51,8 @@ private: NodeList d_infer; NodeList d_infer_exp; + /** mkAnd */ + Node mkAnd( std::vector< TNode >& assumptions ); private: //notification class for equality engine class NotifyClass : public eq::EqualityEngineNotify { @@ -137,7 +139,7 @@ private: /** information necessary for equivalence classes */ std::map< Node, EqcInfo* > d_eqc_info; /** selector applications */ - BoolMap d_selector_apps; + //BoolMap d_selector_apps; /** map from nodes to their instantiated equivalent for each constructor type */ std::map< Node, std::map< int, Node > > d_inst_map; /** which instantiation lemmas we have sent */ @@ -152,6 +154,8 @@ private: * is_[constructor_(n+1)]( t ), each of which is a unique tester. */ NodeListMap d_labels; + /** selector apps for eqch equivalence class */ + NodeListMap d_selector_apps; /** Are we in conflict */ context::CDO d_conflict; /** The conflict node */ @@ -215,8 +219,14 @@ public: private: /** add tester to equivalence class info */ void addTester( Node t, EqcInfo* eqc, Node n ); + /** add selector to equivalence class info */ + void addSelector( Node s, EqcInfo* eqc, Node n, bool assertFacts = true ); + /** add constructor */ + void addConstructor( Node c, EqcInfo* eqc, Node n ); /** merge the equivalence class info of t1 and t2 */ void merge( Node t1, Node t2 ); + /** collapse selector, s is of the form sel( n ) where n = c */ + void collapseSelector( Node s, Node c ); /** for checking if cycles exist */ void checkCycles(); Node searchForCycle( Node n, Node on, @@ -225,15 +235,11 @@ private: /** collect terms */ void collectTerms( Node n ); /** get instantiate cons */ - Node getInstantiateCons( Node n, const Datatype& dt, int index ); - /** apply type ascriptions */ - //Node applyTypeAscriptions( Node n, TypeNode tn ); + Node getInstantiateCons( Node n, const Datatype& dt, int index, bool mkVar = false, bool isActive = true ); /** process new term that was created internally */ void processNewTerm( Node n ); /** check instantiate */ void instantiate( EqcInfo* eqc, Node n ); - /** collapse selectors */ - void collapseSelectors(); /** must specify model * This returns true when the datatypes theory is expected to specify the constructor * type for all equivalence classes. -- cgit v1.2.3 From 04eca05be8e0bd603508169057f19712c925bb8b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 10 Oct 2013 12:36:24 -0500 Subject: Minor bug fix to datatypes. --- src/theory/datatypes/theory_datatypes.cpp | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) (limited to 'src') diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 797445e7e..686695f98 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -685,11 +685,11 @@ void TheoryDatatypes::addTester( Node t, EqcInfo* eqc, Node n ){ Node tt = ( t.getKind() == NOT ) ? t[0] : t; int ttindex = Datatype::indexOf( tt.getOperator().toExpr() ); Node j, jt; + bool makeConflict = false; if( hasLabel( eqc, n ) ){ //if we already know the constructor type, check whether it is in conflict or redundant int jtindex = getLabelIndex( eqc, n ); if( (jtindex==ttindex)!=tpolarity ){ - d_conflict = true; if( !eqc->d_constructor.get().isNull() ){ //conflict because equivalence class contains a constructor std::vector< TNode > assumptions; @@ -698,8 +698,10 @@ void TheoryDatatypes::addTester( Node t, EqcInfo* eqc, Node n ){ d_conflictNode = mkAnd( assumptions ); Trace("dt-conflict") << "CONFLICT: Tester eq conflict : " << d_conflictNode << std::endl; d_out->conflict( d_conflictNode ); + d_conflict = true; return; }else{ + makeConflict = true; //conflict because the existing label is contradictory j = getLabel( n ); jt = j; @@ -719,14 +721,14 @@ void TheoryDatatypes::addTester( Node t, EqcInfo* eqc, Node n ){ int jtindex = Datatype::indexOf( jt.getOperator().toExpr() ); if( jtindex==ttindex ){ if( tpolarity ){ //we are in conflict - d_conflict = true; + makeConflict = true; break; }else{ //it is redundant return; } } } - if( !d_conflict ){ + if( !makeConflict ){ Debug("datatypes-labels") << "Add to labels " << t << std::endl; lbl->push_back( t ); const Datatype& dt = ((DatatypeType)(tt[0].getType()).toType()).getDatatype(); @@ -771,7 +773,9 @@ void TheoryDatatypes::addTester( Node t, EqcInfo* eqc, Node n ){ } } } - if( d_conflict ){ + if( makeConflict ){ + d_conflict = true; + Debug("datatypes-labels") << "Explain " << j << " " << t << std::endl; std::vector< TNode > assumptions; explain( j, assumptions ); explain( t, assumptions ); @@ -879,11 +883,11 @@ void TheoryDatatypes::computeCareGraph(){ } void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ + Trace("dt-cmi") << "Datatypes : Collect model info " << d_equalityEngine.consistent() << std::endl; Trace("dt-model") << std::endl; printModelDebug( "dt-model" ); Trace("dt-model") << std::endl; m->assertEqualityEngine( &d_equalityEngine ); - Trace("dt-cmi") << "Datatypes : Collect model info " << std::endl; /* std::vector< TypeEnumerator > vec; std::map< TypeNode, int > tes; -- cgit v1.2.3 From f35d6f650e3face2b7e96c1efff67ad9325d02b3 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Thu, 10 Oct 2013 12:06:25 -0500 Subject: adds native regexp. --- src/theory/strings/theory_strings_preprocess.cpp | 44 +++++++------ src/theory/strings/theory_strings_preprocess.h | 1 + src/util/regexp.h | 78 ------------------------ 3 files changed, 28 insertions(+), 95 deletions(-) (limited to 'src') diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index f303fd333..64425ea03 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -58,16 +58,6 @@ void StringsPreprocess::simplifyRegExp( Node s, Node r, std::vector< Node > &ret simplifyRegExp( s, r[i], ret ); } break; - case kind::REGEXP_STAR: - { - Node sk = NodeManager::currentNM()->mkSkolem( "ressym_$$", s.getType(), "created for regular expression star" ); - Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, - NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk, s ), - NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, s, sk )); - ret.push_back( eq ); - simplifyRegExp( sk, r[0], ret ); - } - break; case kind::REGEXP_OPT: { Node eq_empty = NodeManager::currentNM()->mkNode( kind::EQUAL, s, NodeManager::currentNM()->mkConst( ::CVC4::String("") ) ); @@ -77,13 +67,27 @@ void StringsPreprocess::simplifyRegExp( Node s, Node r, std::vector< Node > &ret ret.push_back( NodeManager::currentNM()->mkNode( kind::OR, eq_empty, nrr) ); } break; + //TODO: + case kind::REGEXP_STAR: + case kind::REGEXP_PLUS: + Assert( false ); + break; default: - //TODO:case kind::REGEXP_PLUS: //TODO: special sym: sigma, none, all break; } } +bool StringsPreprocess::checkStarPlus( Node t ) { + if( t.getKind() != kind::REGEXP_STAR && t.getKind() != kind::REGEXP_PLUS ) { + for( unsigned i = 0; i &new_nodes ) { std::hash_map::const_iterator i = d_cache.find(t); @@ -94,13 +98,19 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { if( t.getKind() == kind::STRING_IN_REGEXP ){ // t0 in t1 Node t0 = simplify( t[0], new_nodes ); - //rewrite it - std::vector< Node > ret; - simplifyRegExp( t0, t[1], ret ); + + if(!checkStarPlus( t[1] )) { + //rewrite it + std::vector< Node > ret; + simplifyRegExp( t0, t[1], ret ); - Node n = ret.size() == 1 ? ret[0] : NodeManager::currentNM()->mkNode( kind::AND, ret ); - d_cache[t] = (t == n) ? Node::null() : n; - return n; + Node n = ret.size() == 1 ? ret[0] : NodeManager::currentNM()->mkNode( kind::AND, ret ); + d_cache[t] = (t == n) ? Node::null() : n; + return n; + } else { + // TODO + return (t0 == t[0]) ? t : NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, t0, t[1] ); + } }else if( t.getKind() == kind::STRING_SUBSTR ){ Node sk1 = NodeManager::currentNM()->mkSkolem( "st1sym_$$", t.getType(), "created for substr" ); Node sk2 = NodeManager::currentNM()->mkSkolem( "st2sym_$$", t.getType(), "created for substr" ); diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h index d07249a02..ce00a75ce 100644 --- a/src/theory/strings/theory_strings_preprocess.h +++ b/src/theory/strings/theory_strings_preprocess.h @@ -31,6 +31,7 @@ class StringsPreprocess { // NOTE: this class is NOT context-dependent std::hash_map d_cache; private: + bool checkStarPlus( Node t ); void simplifyRegExp( Node s, Node r, std::vector< Node > &ret ); Node simplify( Node t, std::vector< Node > &new_nodes ); public: diff --git a/src/util/regexp.h b/src/util/regexp.h index 58f58a40f..d4ad38b0f 100644 --- a/src/util/regexp.h +++ b/src/util/regexp.h @@ -28,81 +28,6 @@ namespace CVC4 { -class CVC4_PUBLIC Char { - -private: - unsigned int d_char; - -public: - Char() {} - - Char(const unsigned int c) - : d_char(c) {} - - ~Char() {} - - Char& operator =(const Char& y) { - if(this != &y) d_char = y.d_char; - return *this; - } - - bool operator ==(const Char& y) const { - return d_char == y.d_char ; - } - - bool operator !=(const Char& y) const { - return d_char != y.d_char ; - } - - bool operator <(const Char& y) const { - return d_char < y.d_char; - } - - bool operator >(const Char& y) const { - return d_char > y.d_char ; - } - - bool operator <=(const Char& y) const { - return d_char <= y.d_char; - } - - bool operator >=(const Char& y) const { - return d_char >= y.d_char ; - } - - /* - * Convenience functions - */ - std::string toString() const { - std::string str = "1"; - str[0] = (char) d_char; - return str; - } - - unsigned size() const { - return 1; - } - - const char* c_str() const { - return toString().c_str(); - } -};/* class Char */ - -namespace strings { - -struct CharHashFunction { - size_t operator()(const ::CVC4::Char& c) const { - return __gnu_cxx::hash()(c.toString().c_str()); - } -};/* struct CharHashFunction */ - -} - -inline std::ostream& operator <<(std::ostream& os, const Char& c) CVC4_PUBLIC; -inline std::ostream& operator <<(std::ostream& os, const Char& c) { - return os << "\"" << c.toString() << "\""; -} - class CVC4_PUBLIC String { private: @@ -330,9 +255,6 @@ public: return d_str; } - unsigned size() const { - return d_str.size(); - } };/* class String */ /** -- cgit v1.2.3 From 857244b23ad9a8a53de7a3bbe1424d585a0a90f2 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Fri, 11 Oct 2013 03:32:33 -0500 Subject: add constant membership --- src/theory/strings/theory_strings.cpp | 44 ++++- src/theory/strings/theory_strings.h | 4 + src/theory/strings/theory_strings_preprocess.cpp | 23 ++- src/theory/strings/theory_strings_rewriter.cpp | 199 +++++++++++++++++++++-- src/theory/strings/theory_strings_rewriter.h | 5 +- src/util/regexp.h | 11 +- 6 files changed, 260 insertions(+), 26 deletions(-) (limited to 'src') diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index a0058954d..f01da389b 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -49,6 +49,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu d_ind_map_lemma(c), //d_lit_to_decide_index( c, 0 ), //d_lit_to_decide( c ), + d_reg_exp_mem( c ), d_lit_to_unroll( c ) { // The kinds we are treating as function application in congruence @@ -374,6 +375,11 @@ void TheoryStrings::check(Effort e) { } else { d_equalityEngine.assertPredicate(atom, polarity, fact); } + if ( atom.getKind() == kind::STRING_IN_REGEXP ) { + if(fact[0].getKind() != kind::CONST_STRING) { + d_reg_exp_mem.push_back( assertion ); + } + } #ifdef STR_UNROLL_INDUCTION //check if it is a literal to unroll? if( d_lit_to_unroll.find( atom )!=d_lit_to_unroll.end() ){ @@ -400,6 +406,10 @@ void TheoryStrings::check(Effort e) { if( !d_conflict && !addedLemma ){ addedLemma = checkInductiveEquations(); Trace("strings-process") << "Done check inductive equations, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; + if( !d_conflict && !addedLemma ){ + addedLemma = checkMemberships(); + Trace("strings-process") << "Done check membership constraints, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; + } } } } @@ -1851,14 +1861,14 @@ bool TheoryStrings::checkInductiveEquations() { ++i2; ++ie; //++il; - if( !d_equalityEngine.hasTerm( d_emptyString ) || !d_equalityEngine.areEqual( y, d_emptyString ) || !d_equalityEngine.areEqual( x, d_emptyString ) ){ + if( !areEqual( y, d_emptyString ) || !areEqual( x, d_emptyString ) ){ hasEq = true; } } } } if( hasEq ){ - Trace("strings-ind") << "It is incomplete." << std::endl; + Trace("strings-ind") << "Induction is incomplete." << std::endl; d_out->setIncomplete(); }else{ Trace("strings-ind") << "We can answer SAT." << std::endl; @@ -1956,6 +1966,36 @@ void TheoryStrings::printConcat( std::vector< Node >& n, const char * c ) { } } + +bool TheoryStrings::checkMemberships() { + for( unsigned i=0; isetIncomplete(); + } + } + return false; +} + /* Node TheoryStrings::getNextDecisionRequest() { if( d_lit_to_decide_index.get() &ret simplifyRegExp( s, r[i], ret ); } break; + /* case kind::REGEXP_OPT: { Node eq_empty = NodeManager::currentNM()->mkNode( kind::EQUAL, s, NodeManager::currentNM()->mkConst( ::CVC4::String("") ) ); @@ -67,10 +68,13 @@ void StringsPreprocess::simplifyRegExp( Node s, Node r, std::vector< Node > &ret ret.push_back( NodeManager::currentNM()->mkNode( kind::OR, eq_empty, nrr) ); } break; - //TODO: + //case kind::REGEXP_PLUS: + */ case kind::REGEXP_STAR: - case kind::REGEXP_PLUS: - Assert( false ); + { + Node eq = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, s, r ); + ret.push_back( eq ); + } break; default: //TODO: special sym: sigma, none, all @@ -95,11 +99,12 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { return (*i).second.isNull() ? t : (*i).second; } + /* if( t.getKind() == kind::STRING_IN_REGEXP ){ // t0 in t1 Node t0 = simplify( t[0], new_nodes ); - if(!checkStarPlus( t[1] )) { + //if(!checkStarPlus( t[1] )) { //rewrite it std::vector< Node > ret; simplifyRegExp( t0, t[1], ret ); @@ -107,11 +112,13 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node n = ret.size() == 1 ? ret[0] : NodeManager::currentNM()->mkNode( kind::AND, ret ); d_cache[t] = (t == n) ? Node::null() : n; return n; - } else { + //} else { // TODO - return (t0 == t[0]) ? t : NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, t0, t[1] ); - } - }else if( t.getKind() == kind::STRING_SUBSTR ){ + // return (t0 == t[0]) ? t : NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, t0, t[1] ); + //} + }else + */ + if( t.getKind() == kind::STRING_SUBSTR ){ Node sk1 = NodeManager::currentNM()->mkSkolem( "st1sym_$$", t.getType(), "created for substr" ); Node sk2 = NodeManager::currentNM()->mkSkolem( "st2sym_$$", t.getType(), "created for substr" ); Node sk3 = NodeManager::currentNM()->mkSkolem( "st3sym_$$", t.getType(), "created for substr" ); diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 3a7ad1ee0..29e35981d 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -53,7 +53,7 @@ Node TheoryStringsRewriter::rewriteConcatString(TNode node) { } if(!tmpNode.isConst()) { if(preNode != Node::null()) { - if(preNode.getKind() == kind::CONST_STRING && preNode.getConst().toString()=="" ) { + if(preNode.getKind() == kind::CONST_STRING && preNode.getConst().isEmptyString() ) { preNode = Node::null(); } else { node_vec.push_back( preNode ); @@ -81,6 +81,179 @@ Node TheoryStringsRewriter::rewriteConcatString(TNode node) { return retNode; } +void TheoryStringsRewriter::simplifyRegExp( Node s, Node r, std::vector< Node > &ret ) { + int k = r.getKind(); + switch( k ) { + case kind::STRING_TO_REGEXP: + { + Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, s, r[0] ); + ret.push_back( eq ); + } + break; + case kind::REGEXP_CONCAT: + { + std::vector< Node > cc; + for(unsigned i=0; imkSkolem( "recsym_$$", s.getType(), "created for regular expression concat" ); + simplifyRegExp( sk, r[i], ret ); + cc.push_back( sk ); + } + Node cc_eq = NodeManager::currentNM()->mkNode( kind::EQUAL, s, + NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, cc ) ); + ret.push_back( cc_eq ); + } + break; + case kind::REGEXP_OR: + { + std::vector< Node > c_or; + for(unsigned i=0; imkNode( kind::OR, c_or ); + ret.push_back( eq ); + } + break; + case kind::REGEXP_INTER: + for(unsigned i=0; imkNode( kind::STRING_IN_REGEXP, s, r ); + ret.push_back( eq ); + } + break; + default: + //TODO: special sym: sigma, none, all + Trace("strings-prerewrite") << "Unsupported term: " << r << " in simplifyRegExp." << std::endl; + Assert( false ); + break; + } +} +bool TheoryStringsRewriter::testConstStringInRegExp( CVC4::String &s, unsigned int index_start, Node r ) { + Assert( index_start <= s.size() ); + int k = r.getKind(); + switch( k ) { + case kind::STRING_TO_REGEXP: + { + CVC4::String s2 = s.substr( index_start, s.size() - index_start ); + CVC4::String t = r[0].getConst(); + return s2 == r[0].getConst(); + } + case kind::REGEXP_CONCAT: + { + if( s.size() != index_start ) { + std::vector vec_k( r.getNumChildren(), -1 ); + int start = 0; + int left = (int) s.size(); + int i=0; + while( i<(int) r.getNumChildren() ) { + bool flag = true; + if( i == (int) r.getNumChildren() - 1 ) { + if( testConstStringInRegExp( s, index_start + start, r[i] ) ) { + return true; + } + } else if( i == -1 ) { + return false; + } else { + for(vec_k[i] = vec_k[i] + 1; vec_k[i] <= left; ++vec_k[i]) { + CVC4::String t = s.substr(index_start + start, vec_k[i]); + if( testConstStringInRegExp( t, 0, r[i] ) ) { + start += vec_k[i]; left -= vec_k[i]; flag = false; + ++i; vec_k[i] = -1; + break; + } + } + } + + if(flag) { + --i; + if(i >= 0) { + start -= vec_k[i]; left += vec_k[i]; + } + } + } + return false; + } else { + return true; + } + } + case kind::REGEXP_OR: + { + for(unsigned i=0; i0; --k) { + CVC4::String t = s.substr(index_start, k); + if( testConstStringInRegExp( t, 0, r[0] ) ) { + if( index_start + k == s.size() || testConstStringInRegExp( s, index_start + k, r[0] ) ) { + return true; + } + } + } + return false; + } else { + return true; + } + } + default: + //TODO: special sym: sigma, none, all + Trace("strings-postrewrite") << "Unsupported term: " << r << " in testConstStringInRegExp." << std::endl; + Assert( false ); + return false; + } +} +Node TheoryStringsRewriter::rewriteMembership(TNode node) { + Node retNode; + + //Trace("strings-postrewrite") << "Strings::rewriteMembership start " << node << std::endl; + + Node x; + if(node[0].getKind() == kind::STRING_CONCAT) { + x = rewriteConcatString(node[0]); + } else { + x = node[0]; + } + + if( x.getKind() == kind::CONST_STRING ) { + //test whether x in node[1] + CVC4::String s = x.getConst(); + retNode = NodeManager::currentNM()->mkConst( testConstStringInRegExp( s, 0, node[1] ) ); + } else { + if( node[1].getKind() == kind::REGEXP_STAR ) { + if( x == node[0] ) { + retNode = node; + } else { + retNode = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, x, node[1] ); + } + } else { + std::vector node_vec; + simplifyRegExp( x, node[1], node_vec ); + + if(node_vec.size() > 1) { + retNode = NodeManager::currentNM()->mkNode(kind::AND, node_vec); + } else { + retNode = node_vec[0]; + } + } + } + //Trace("strings-prerewrite") << "Strings::rewriteMembership end " << retNode << std::endl; + return retNode; +} + RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { Trace("strings-postrewrite") << "Strings::postRewrite start " << node << std::endl; Node retNode = node; @@ -106,17 +279,6 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { } else if( leftNode != node[0] || rightNode != node[1]) { retNode = NodeManager::currentNM()->mkNode(kind::EQUAL, leftNode, rightNode); } - } else if(node.getKind() == kind::STRING_IN_REGEXP) { - Node leftNode = node[0]; - if(node[0].getKind() == kind::STRING_CONCAT) { - leftNode = rewriteConcatString(node[0]); - } - // TODO: right part - Node rightNode = node[1]; - // merge - if( leftNode != node[0] || rightNode != node[1]) { - retNode = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, leftNode, rightNode); - } } else if(node.getKind() == kind::STRING_LENGTH) { if(node[0].isConst()) { retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( node[0].getConst().size() ) ); @@ -150,9 +312,11 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { } else { //handled by preprocess } + } else if(node.getKind() == kind::STRING_IN_REGEXP) { + retNode = rewriteMembership(node); } - Trace("strings-postrewrite") << "Strings::postRewrite returning " << node << std::endl; + Trace("strings-postrewrite") << "Strings::postRewrite returning " << retNode << std::endl; return RewriteResponse(REWRITE_DONE, retNode); } @@ -162,7 +326,14 @@ RewriteResponse TheoryStringsRewriter::preRewrite(TNode node) { if(node.getKind() == kind::STRING_CONCAT) { retNode = rewriteConcatString(node); - } + } else if(node.getKind() == kind::REGEXP_PLUS) { + retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT, node[0], + NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, node[0])); + } else if(node.getKind() == kind::REGEXP_OPT) { + retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_OR, + NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst( ::CVC4::String("") ) ), + node[0]); + } Trace("strings-prerewrite") << "Strings::preRewrite returning " << retNode << std::endl; return RewriteResponse(REWRITE_DONE, retNode); diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h index 3bccd91de..ecc863a75 100644 --- a/src/theory/strings/theory_strings_rewriter.h +++ b/src/theory/strings/theory_strings_rewriter.h @@ -29,9 +29,12 @@ namespace theory { namespace strings { class TheoryStringsRewriter { - public: + static bool testConstStringInRegExp( CVC4::String &s, unsigned int index_start, Node r ); + static void simplifyRegExp( Node s, Node r, std::vector< Node > &ret ); + static Node rewriteConcatString(TNode node); + static Node rewriteMembership(TNode node); static RewriteResponse postRewrite(TNode node); diff --git a/src/util/regexp.h b/src/util/regexp.h index d4ad38b0f..31a39e6f9 100644 --- a/src/util/regexp.h +++ b/src/util/regexp.h @@ -22,7 +22,7 @@ #include #include -//#include "util/exception.h" +//#include "util/cvc4_assert.h" //#include "util/integer.h" #include "util/hash.h" @@ -126,6 +126,15 @@ public: return true; } + + bool isEmptyString() const { + return ( d_str.size() == 0 ); + } + + unsigned int operator[] (const unsigned int i) const { + //Assert( i < d_str.size() && i >= 0); + return d_str[i]; + } /* * Convenience functions */ -- cgit v1.2.3 From c388e89e5253aa6fbde7685fc53126872f578f0b Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Fri, 11 Oct 2013 16:54:22 -0500 Subject: Adds regular expression support, it is actually CFL because of variables. --- src/theory/strings/options | 3 + src/theory/strings/theory_strings.cpp | 368 +++++++------------------ src/theory/strings/theory_strings.h | 16 +- src/theory/strings/theory_strings_rewriter.cpp | 33 ++- src/theory/strings/theory_strings_rewriter.h | 1 + src/theory/strings/theory_strings_type_rules.h | 6 +- test/regress/regress0/strings/Makefile.am | 4 +- test/regress/regress0/strings/loop005.smt2 | 10 +- test/regress/regress0/strings/loop007.smt2 | 5 +- test/regress/regress0/strings/loop008.smt2 | 9 + test/regress/regress0/strings/regexp001.smt2 | 12 + 11 files changed, 169 insertions(+), 298 deletions(-) create mode 100644 test/regress/regress0/strings/loop008.smt2 create mode 100644 test/regress/regress0/strings/regexp001.smt2 (limited to 'src') diff --git a/src/theory/strings/options b/src/theory/strings/options index 9226f9999..3fceb06d4 100644 --- a/src/theory/strings/options +++ b/src/theory/strings/options @@ -8,4 +8,7 @@ module STRINGS "theory/strings/options.h" Strings theory option stringCharCardinality str-alphabet-card --str-alphabet-card=N int16_t :default 256 :read-write the cardinality of the characters used by the theory of string, default 256 +option stringRegExpUnrollDepth str-regexp-depth --str-regexp-depth=N int16_t :default 10 :read-write + the depth of unrolloing regular expression used by the theory of string, default 10 + endmodule diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index f01da389b..9f33e9191 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -26,8 +26,6 @@ #include "theory/strings/type_enumerator.h" #include -#define STR_UNROLL_INDUCTION - using namespace std; using namespace CVC4::context; @@ -43,17 +41,16 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu 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_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_reg_exp_mem( c ), - d_lit_to_unroll( c ) + d_reg_exp_mem( c ) { // The kinds we are treating as function application in congruence - d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP); + //d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP); d_equalityEngine.addFunctionKind(kind::STRING_LENGTH); d_equalityEngine.addFunctionKind(kind::STRING_CONCAT); @@ -61,6 +58,9 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu d_emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") ); d_true = NodeManager::currentNM()->mkConst( true ); d_false = NodeManager::currentNM()->mkConst( false ); + + //option + d_regexp_unroll_depth = options::stringRegExpUnrollDepth(); } TheoryStrings::~TheoryStrings() { @@ -328,7 +328,7 @@ void TheoryStrings::preRegisterTerm(TNode n) { d_equalityEngine.addTriggerEquality(n); break; case kind::STRING_IN_REGEXP: - d_equalityEngine.addTriggerPredicate(n); + //d_equalityEngine.addTriggerPredicate(n); break; default: if(n.getKind() == kind::VARIABLE || n.getKind()==kind::SKOLEM) { @@ -370,22 +370,16 @@ void TheoryStrings::check(Effort e) { polarity = fact.getKind() != kind::NOT; atom = polarity ? fact : fact[0]; - if (atom.getKind() == kind::EQUAL) { + //must record string in regular expressions + if ( atom.getKind() == kind::STRING_IN_REGEXP ) { + //if(fact[0].getKind() != kind::CONST_STRING) { + d_reg_exp_mem.push_back( assertion ); + //} + }else if (atom.getKind() == kind::EQUAL) { d_equalityEngine.assertEquality(atom, polarity, fact); } else { d_equalityEngine.assertPredicate(atom, polarity, fact); } - if ( atom.getKind() == kind::STRING_IN_REGEXP ) { - if(fact[0].getKind() != kind::CONST_STRING) { - d_reg_exp_mem.push_back( assertion ); - } - } -#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(); @@ -404,12 +398,8 @@ void TheoryStrings::check(Effort e) { 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; - if( !d_conflict && !addedLemma ){ - addedLemma = checkMemberships(); - Trace("strings-process") << "Done check membership constraints, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; - } + addedLemma = checkMemberships(); + Trace("strings-process") << "Done check membership constraints, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl; } } } @@ -447,7 +437,7 @@ void TheoryStrings::conflict(TNode a, TNode b){ } else { conflictNode = explain( a.eqNode(b) ); } - Debug("strings-conflict") << "CONFLICT: Eq engine conflict : " << conflictNode << std::endl; + Trace("strings-conflict") << "CONFLICT: Eq engine conflict : " << conflictNode << std::endl; d_out->conflict( conflictNode ); d_conflict = true; } @@ -883,7 +873,7 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v 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") << "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") << " ... T(Y.Z)= "; @@ -914,8 +904,9 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v 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" ); + Node sk_y= NodeManager::currentNM()->mkSkolem( "y_loop_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); + Node sk_z= NodeManager::currentNM()->mkSkolem( "z_loop_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); + Node sk_w= NodeManager::currentNM()->mkSkolem( "w_loop_$$", 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 @@ -953,6 +944,11 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v } Node conc2 = NodeManager::currentNM()->mkNode( kind::EQUAL, left2, mkConcat( c3c ) ); + Node conc3 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[other_n_index][other_index], mkConcat( sk_y, sk_w ) ); + Node conc4 = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, sk_w, + NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, + NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, mkConcat( sk_z, sk_y ) ) ) ); + unrollStar( conc4 ); Node sk_y_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_y ); //Node sk_z_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_z ); @@ -966,7 +962,7 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v // 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 + conc = NodeManager::currentNM()->mkNode( kind::AND, conc1, conc2, conc3, conc4 );//, 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 ); @@ -974,7 +970,6 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v //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 true; }else{ Trace("strings-solve-debug") << "No loops detected." << std::endl; @@ -1013,7 +1008,7 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v Node firstChar = const_str.getConst().size() == 1 ? const_str : NodeManager::currentNM()->mkConst( const_str.getConst().substr(0, 1) ); //split the string - Node sk = NodeManager::currentNM()->mkSkolem( "ssym_$$", normal_forms[i][index_i].getType(), "created for v/c split" ); + Node sk = NodeManager::currentNM()->mkSkolem( "c_split_$$", normal_forms[i][index_i].getType(), "created for v/c split" ); Node eq1 = NodeManager::currentNM()->mkNode( kind::EQUAL, other_str, d_emptyString ); Node eq2 = NodeManager::currentNM()->mkNode( kind::EQUAL, other_str, @@ -1034,7 +1029,7 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v }else{ antec_new_lits.push_back(ldeq); } - Node sk = NodeManager::currentNM()->mkSkolem( "ssym_$$", normal_forms[i][index_i].getType(), "created for v/v split" ); + Node sk = NodeManager::currentNM()->mkSkolem( "v_split_$$", normal_forms[i][index_i].getType(), "created for v/v 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], @@ -1158,9 +1153,9 @@ bool TheoryStrings::normalizeDisequality( Node ni, Node nj ) { antec.push_back( ni.eqNode( nj ).negate() ); antec_new_lits.push_back( li.eqNode( lj ).negate() ); std::vector< Node > conc; - Node sk1 = NodeManager::currentNM()->mkSkolem( "xpdsym_$$", ni.getType(), "created for disequality normalization" ); - Node sk2 = NodeManager::currentNM()->mkSkolem( "ypdsym_$$", ni.getType(), "created for disequality normalization" ); - Node sk3 = NodeManager::currentNM()->mkSkolem( "zpdsym_$$", ni.getType(), "created for disequality normalization" ); + Node sk1 = NodeManager::currentNM()->mkSkolem( "x_dsplit_$$", ni.getType(), "created for disequality normalization" ); + Node sk2 = NodeManager::currentNM()->mkSkolem( "y_dsplit_$$", ni.getType(), "created for disequality normalization" ); + Node sk3 = NodeManager::currentNM()->mkSkolem( "z_dsplit_$$", ni.getType(), "created for disequality normalization" ); Node lsk1 = getLength( sk1 ); conc.push_back( lsk1.eqNode( li ) ); Node lsk2 = getLength( sk2 ); @@ -1168,30 +1163,6 @@ bool TheoryStrings::normalizeDisequality( Node ni, Node nj ) { conc.push_back( NodeManager::currentNM()->mkNode( kind::OR, j.eqNode( mkConcat( sk1, sk3 ) ), i.eqNode( mkConcat( sk2, sk3 ) ) ) ); - /* - 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 c = NodeManager::currentNM()->mkNode( kind::AND, conc ); - */ - //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( areEqual( li, lj ) ){ @@ -1269,81 +1240,6 @@ bool TheoryStrings::isNormalFormPair2( Node n1, Node n2 ) { 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(getSatContext()->getCMM()) ); - d_ind_map1.insertDataFromContextMemory( x, lst1 ); - // add x->z - lst2 = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false, - ContextMemoryAllocator(getSatContext()->getCMM()) ); - d_ind_map2.insertDataFromContextMemory( x, lst2 ); - // add x->exp - lste = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false, - ContextMemoryAllocator(getSatContext()->getCMM()) ); - d_ind_map_exp.insertDataFromContextMemory( x, lste ); - // add x->hasLemma false - lstl = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false, - ContextMemoryAllocator(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() || conc==d_false ){ d_out->conflict(ant); @@ -1517,6 +1413,7 @@ bool TheoryStrings::checkNormalForms() { 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; @@ -1532,6 +1429,7 @@ bool TheoryStrings::checkNormalForms() { ++i2; } } + */ bool addedFact; do { @@ -1757,125 +1655,6 @@ int TheoryStrings::gcd ( int a, int b ) { 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 co; - co.push_back(0); - for(unsigned int k=0; k().getNumerator().toUnsignedInt(); - co[0] += cols[k].size() * len; - } else { - co.push_back( cols[k].size() ); - } - } - int g_co = co[0]; - for(unsigned k=1; kmkNode( 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( !areEqual( y, d_emptyString ) || !areEqual( x, d_emptyString ) ){ - hasEq = true; - } - } - } - } - if( hasEq ){ - Trace("strings-ind") << "Induction 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() ) { @@ -1966,34 +1745,79 @@ void TheoryStrings::printConcat( std::vector< Node >& n, const char * c ) { } } +bool TheoryStrings::unrollStar( Node atom ) { + Node x = atom[0]; + Node r = atom[1]; + int depth = d_reg_exp_unroll_depth.find( atom )==d_reg_exp_unroll_depth.end() ? 0 : d_reg_exp_unroll_depth[atom]; + if( depth <= d_regexp_unroll_depth ){ + Trace("strings-regex") << "...unroll " << atom << " now." << std::endl; + d_reg_exp_unroll[atom] = true; + //add lemma? + Node xeqe = x.eqNode( d_emptyString ); + xeqe = Rewriter::rewrite( xeqe ); + d_pending_req_phase[xeqe] = true; + Node sk_s= NodeManager::currentNM()->mkSkolem( "s_unroll_$$", x.getType(), "created for unrolling" ); + Node sk_xp= NodeManager::currentNM()->mkSkolem( "x_unroll_$$", x.getType(), "created for unrolling" ); + Node unr0 = sk_s.eqNode( d_emptyString ).negate(); + Node unr1 = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, sk_s, r[0] ); + Node unr2 = x.eqNode( mkConcat( sk_s, sk_xp ) ); + Node unr3 = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, sk_xp, r ); + unr3 = Rewriter::rewrite( unr3 ); + d_reg_exp_unroll_depth[unr3] = depth + 1; + Node unr = NodeManager::currentNM()->mkNode( kind::AND, unr0, unr1, unr2, unr3 ); + Node lem = NodeManager::currentNM()->mkNode( kind::OR, xeqe, unr ); + sendLemma( atom, lem, "Unroll" ); + return true; + }else{ + return false; + } +} bool TheoryStrings::checkMemberships() { + bool is_unk = false; + bool addedLemma = false; for( unsigned i=0; isetIncomplete(); + Trace("strings-regex") << "SET INCOMPLETE" << std::endl; + d_out->setIncomplete(); } + return false; } - return false; } /* diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index c906d7f91..48bc28b05 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -37,6 +37,7 @@ class TheoryStrings : public Theory { typedef context::CDChunkList NodeList; typedef context::CDHashMap NodeListMap; typedef context::CDHashMap NodeBoolMap; + typedef context::CDHashMap NodeIntMap; public: TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe); @@ -124,6 +125,8 @@ class TheoryStrings : public Theory { Node d_true; Node d_false; Node d_zero; + // RegExp depth + int d_regexp_unroll_depth; //list of pairs of nodes to merge std::map< Node, Node > d_pending_exp; std::vector< Node > d_pending; @@ -142,18 +145,10 @@ class TheoryStrings : public Theory { bool isNormalFormPair( Node n1, Node n2 ); bool isNormalFormPair2( Node n1, Node n2 ); - //inductive equations - NodeListMap d_ind_map1; - NodeListMap d_ind_map2; - NodeListMap d_ind_map_exp; - NodeListMap d_ind_map_lemma; //regular expression memberships NodeList d_reg_exp_mem; - bool addInductiveEquation( Node x, Node y, Node z, Node exp, const char * c ); - - //for unrolling inductive equations - NodeBoolMap d_lit_to_unroll; - + std::map< Node, bool > d_reg_exp_unroll; + std::map< Node, int > d_reg_exp_unroll_depth; ///////////////////////////////////////////////////////////////////////////// // MODEL GENERATION @@ -200,6 +195,7 @@ class TheoryStrings : public Theory { std::vector< std::vector< Node > > &normal_forms, std::vector< std::vector< Node > > &normal_forms_exp, std::vector< Node > &normal_form_src); bool normalizeEquivalenceClass( Node n, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< Node > & nf_exp ); bool normalizeDisequality( Node n1, Node n2 ); + bool unrollStar( Node atom ); bool checkLengths(); bool checkNormalForms(); diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 29e35981d..31203b767 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -131,6 +131,21 @@ void TheoryStringsRewriter::simplifyRegExp( Node s, Node r, std::vector< Node > break; } } +bool TheoryStringsRewriter::checkConstRegExp( Node t ) { + if( t.getKind() != kind::STRING_TO_REGEXP ) { + for( unsigned i = 0; i(); - return s2 == r[0].getConst(); + if(r[0].getKind() == kind::CONST_STRING) { + return ( s2 == r[0].getConst() ); + } else { + Assert( false, "RegExp contains variable" ); + } } case kind::REGEXP_CONCAT: { @@ -199,7 +217,7 @@ bool TheoryStringsRewriter::testConstStringInRegExp( CVC4::String &s, unsigned i for(unsigned int k=s.size() - index_start; k>0; --k) { CVC4::String t = s.substr(index_start, k); if( testConstStringInRegExp( t, 0, r[0] ) ) { - if( index_start + k == s.size() || testConstStringInRegExp( s, index_start + k, r[0] ) ) { + if( index_start + k == s.size() || testConstStringInRegExp( s, index_start + k, r ) ) { return true; } } @@ -228,7 +246,8 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) { x = node[0]; } - if( x.getKind() == kind::CONST_STRING ) { + if( x.getKind() == kind::CONST_STRING && checkConstRegExp(node[1]) ) { + //TODO x \in R[y] //test whether x in node[1] CVC4::String s = x.getConst(); retNode = NodeManager::currentNM()->mkConst( testConstStringInRegExp( s, 0, node[1] ) ); @@ -257,6 +276,7 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) { RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { Trace("strings-postrewrite") << "Strings::postRewrite start " << node << std::endl; Node retNode = node; + Node orig = retNode; if(node.getKind() == kind::STRING_CONCAT) { retNode = rewriteConcatString(node); @@ -317,11 +337,12 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { } Trace("strings-postrewrite") << "Strings::postRewrite returning " << retNode << std::endl; - return RewriteResponse(REWRITE_DONE, retNode); + return RewriteResponse(orig==retNode ? REWRITE_DONE : REWRITE_AGAIN_FULL, retNode); } RewriteResponse TheoryStringsRewriter::preRewrite(TNode node) { Node retNode = node; + Node orig = retNode; Trace("strings-prerewrite") << "Strings::preRewrite start " << node << std::endl; if(node.getKind() == kind::STRING_CONCAT) { @@ -336,5 +357,5 @@ RewriteResponse TheoryStringsRewriter::preRewrite(TNode node) { } Trace("strings-prerewrite") << "Strings::preRewrite returning " << retNode << std::endl; - return RewriteResponse(REWRITE_DONE, retNode); + return RewriteResponse(orig==retNode ? REWRITE_DONE : REWRITE_AGAIN_FULL, retNode); } diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h index ecc863a75..9dcfb4ce5 100644 --- a/src/theory/strings/theory_strings_rewriter.h +++ b/src/theory/strings/theory_strings_rewriter.h @@ -30,6 +30,7 @@ namespace strings { class TheoryStringsRewriter { public: + static bool checkConstRegExp( Node t ); static bool testConstStringInRegExp( CVC4::String &s, unsigned int index_start, Node r ); static void simplifyRegExp( Node s, Node r, std::vector< Node > &ret ); diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h index ef8f58f80..f63cd32fc 100644 --- a/src/theory/strings/theory_strings_type_rules.h +++ b/src/theory/strings/theory_strings_type_rules.h @@ -203,9 +203,9 @@ public: if (!t.isString()) { throw TypeCheckingExceptionPrivate(n, "expecting string terms"); } - if( (*it).getKind() != kind::CONST_STRING ) { - throw TypeCheckingExceptionPrivate(n, "expecting constant string terms"); - } + //if( (*it).getKind() != kind::CONST_STRING ) { + // throw TypeCheckingExceptionPrivate(n, "expecting constant string terms"); + //} if(++it != it_end) { throw TypeCheckingExceptionPrivate(n, "too many terms"); } diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index 9b9fdef7a..daa817c4f 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -27,13 +27,15 @@ TESTS = \ str005.smt2 \ model001.smt2 \ substr001.smt2 \ + regexp001.smt2 \ loop001.smt2 \ loop002.smt2 \ loop003.smt2 \ loop004.smt2 \ loop005.smt2 \ loop006.smt2 \ - loop007.smt2 + loop007.smt2 \ + loop008.smt2 FAILING_TESTS = diff --git a/test/regress/regress0/strings/loop005.smt2 b/test/regress/regress0/strings/loop005.smt2 index 4401ef794..039409ea6 100644 --- a/test/regress/regress0/strings/loop005.smt2 +++ b/test/regress/regress0/strings/loop005.smt2 @@ -5,11 +5,13 @@ (declare-fun y () String) (declare-fun z () String) (declare-fun w () String) -(declare-fun w1 () String) -(declare-fun w2 () String) -(assert (= (str.++ x y z) (str.++ x z y))) -(assert (= (str.++ x w z) (str.++ x z w))) +;(assert (= (str.++ x y z) (str.++ x z y))) +;(assert (= (str.++ x w z) (str.++ x z w))) + +(assert (= (str.++ y z) (str.++ z y))) +(assert (= (str.++ w z) (str.++ z w))) + (assert (not (= y w))) (assert (> (str.len z) 0)) diff --git a/test/regress/regress0/strings/loop007.smt2 b/test/regress/regress0/strings/loop007.smt2 index bea4037d1..b292de512 100644 --- a/test/regress/regress0/strings/loop007.smt2 +++ b/test/regress/regress0/strings/loop007.smt2 @@ -5,6 +5,7 @@ (declare-fun y () String) (assert (= (str.++ x y "aa") (str.++ "aa" y x))) -(assert (= (str.len x) 1)) +(assert (= (str.len x) (* 2 (str.len y)))) +(assert (> (str.len x) 0)) -(check-sat) \ No newline at end of file +(check-sat) diff --git a/test/regress/regress0/strings/loop008.smt2 b/test/regress/regress0/strings/loop008.smt2 new file mode 100644 index 000000000..91ed8cdf0 --- /dev/null +++ b/test/regress/regress0/strings/loop008.smt2 @@ -0,0 +1,9 @@ +(set-logic QF_S) +(set-info :status sat) + +(declare-fun x () String) + +(assert (= (str.++ x "ab") (str.++ "ba" x))) +(assert (> (str.len x) 5)) + +(check-sat) diff --git a/test/regress/regress0/strings/regexp001.smt2 b/test/regress/regress0/strings/regexp001.smt2 new file mode 100644 index 000000000..41aefbd41 --- /dev/null +++ b/test/regress/regress0/strings/regexp001.smt2 @@ -0,0 +1,12 @@ +(set-logic QF_S) +(set-info :status sat) + +(declare-fun x () String) + +(assert (str.in.re x + (re.* (re.++ (re.* (str.to.re "a") ) (str.to.re "b") )) + )) + +(assert (= (str.len x) 3)) + +(check-sat) -- cgit v1.2.3 From 177f347c7db9ef276dbaebe166080abc78a2bf73 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Mon, 14 Oct 2013 16:27:33 -0500 Subject: Adds Regular Expression support. --- src/theory/strings/theory_strings.cpp | 138 +++++++++++++++-------- src/theory/strings/theory_strings.h | 1 + src/theory/strings/theory_strings_preprocess.cpp | 58 +++++----- src/theory/strings/theory_strings_preprocess.h | 4 +- src/theory/strings/theory_strings_rewriter.cpp | 79 ++++++++++++- src/theory/strings/theory_strings_rewriter.h | 5 +- src/theory/strings/theory_strings_type_rules.h | 12 +- test/regress/regress0/strings/regexp002.smt2 | 19 ++++ 8 files changed, 227 insertions(+), 89 deletions(-) create mode 100644 test/regress/regress0/strings/regexp002.smt2 (limited to 'src') diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 9f33e9191..cfc9fa77e 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -903,10 +903,7 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v // for some y,z,k Trace("strings-loop") << "Must add lemma." << std::endl; - //need to break - Node sk_y= NodeManager::currentNM()->mkSkolem( "y_loop_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); - Node sk_z= NodeManager::currentNM()->mkSkolem( "z_loop_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); - Node sk_w= NodeManager::currentNM()->mkSkolem( "w_loop_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); + Trace("strings-loop") << "Cache: " << normal_form_src[i] << " vs " << normal_form_src[j] << std::endl; antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); //require that x is non-empty @@ -920,55 +917,77 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v 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 conc3 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[other_n_index][other_index], mkConcat( sk_y, sk_w ) ); - Node conc4 = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, sk_w, - NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, - NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, mkConcat( sk_z, sk_y ) ) ) ); - unrollStar( conc4 ); - - 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 ); + //need to break + Node sk_w= NodeManager::currentNM()->mkSkolem( "w_loop_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); Node ant = mkExplain( antec, antec_new_lits ); - conc = NodeManager::currentNM()->mkNode( kind::AND, conc1, conc2, conc3, conc4 );//, 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 ); + if(index == loop_index - 1 && + other_index + 2 == (int) normal_forms[other_n_index].size() && + loop_index + 1 == (int) normal_forms[loop_n_index].size() && + normal_forms[loop_n_index][index] == normal_forms[other_n_index][other_index + 1] && + normal_forms[loop_n_index][index].isConst() ) { + Trace("strings-loop") << "Special case (X)=" << normal_forms[other_n_index][other_index] << " " << std::endl; + Trace("strings-loop") << "... (C)=" << normal_forms[loop_n_index][index] << " " << std::endl; + //special case + Node conc3 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[other_n_index][other_index], mkConcat( normal_forms[loop_n_index][index], sk_w ) ); + Node conc4 = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, sk_w, + NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, + NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, normal_forms[loop_n_index][index] ) ) ); + unrollStar( conc4 ); + conc = conc4; + } else { + Node sk_y= NodeManager::currentNM()->mkSkolem( "y_loop_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); + Node sk_z= NodeManager::currentNM()->mkSkolem( "z_loop_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); + //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 conc3 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[other_n_index][other_index], mkConcat( sk_y, sk_w ) ); + Node conc4 = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, sk_w, + NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, + NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, mkConcat( sk_z, sk_y ) ) ) ); + unrollStar( conc4 ); + + //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_z_gt_zero = NodeManager::currentNM()->mkNode( kind::GT, sk_z_len, d_zero ); + //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, sk_z.eqNode(d_emptyString), sk_y.eqNode(d_emptyString)); + + //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 ); + conc = NodeManager::currentNM()->mkNode( kind::AND, conc1, conc2, conc3, conc4 );//, 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 ); + } // normal case //we will be done addNormalFormPair( normal_form_src[i], normal_form_src[j] ); + //Assert( isNormalFormPair( normal_form_src[i], normal_form_src[j] ) ); sendLemma( ant, conc, "Loop" ); return true; }else{ @@ -1198,6 +1217,7 @@ bool TheoryStrings::normalizeDisequality( Node ni, Node nj ) { void TheoryStrings::addNormalFormPair( Node n1, Node n2 ) { if( !isNormalFormPair( n1, n2 ) ){ + //Assert( !isNormalFormPair( n1, n2 ) ); NodeList* lst; NodeListMap::iterator nf_i = d_nf_pairs.find( n1 ); if( nf_i == d_nf_pairs.end() ){ @@ -1759,12 +1779,30 @@ bool TheoryStrings::unrollStar( Node atom ) { Node sk_s= NodeManager::currentNM()->mkSkolem( "s_unroll_$$", x.getType(), "created for unrolling" ); Node sk_xp= NodeManager::currentNM()->mkSkolem( "x_unroll_$$", x.getType(), "created for unrolling" ); Node unr0 = sk_s.eqNode( d_emptyString ).negate(); + // must also call preprocessing on unr1 Node unr1 = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, sk_s, r[0] ); + + std::vector< Node > urc; + urc.push_back( unr1 ); + + StringsPreprocess spp; + spp.simplify( urc ); + for( unsigned i=1; imkNode( kind::STRING_IN_REGEXP, sk_xp, r ); unr3 = Rewriter::rewrite( unr3 ); d_reg_exp_unroll_depth[unr3] = depth + 1; - Node unr = NodeManager::currentNM()->mkNode( kind::AND, unr0, unr1, unr2, unr3 ); + + //|x|>|xp| + Node len_x_gt_len_xp = NodeManager::currentNM()->mkNode( kind::GT, + NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, x ), + NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_xp ) ); + + Node unr = NodeManager::currentNM()->mkNode( kind::AND, unr0, urc[0], unr2, unr3, len_x_gt_len_xp ); Node lem = NodeManager::currentNM()->mkNode( kind::OR, xeqe, unr ); sendLemma( atom, lem, "Unroll" ); return true; diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 48bc28b05..d059d8bba 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -21,6 +21,7 @@ #include "theory/theory.h" #include "theory/uf/equality_engine.h" +#include "theory/strings/theory_strings_preprocess.h" #include "context/cdchunk_list.h" diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 472a6d89c..378fa3428 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -21,7 +21,7 @@ namespace CVC4 { namespace theory { namespace strings { -void StringsPreprocess::simplifyRegExp( Node s, Node r, std::vector< Node > &ret ) { +void StringsPreprocess::simplifyRegExp( Node s, Node r, std::vector< Node > &ret, std::vector< Node > &nn ) { int k = r.getKind(); switch( k ) { case kind::STRING_TO_REGEXP: @@ -35,19 +35,19 @@ void StringsPreprocess::simplifyRegExp( Node s, Node r, std::vector< Node > &ret std::vector< Node > cc; for(unsigned i=0; imkSkolem( "recsym_$$", s.getType(), "created for regular expression concat" ); - simplifyRegExp( sk, r[i], ret ); + simplifyRegExp( sk, r[i], ret, nn ); cc.push_back( sk ); } Node cc_eq = NodeManager::currentNM()->mkNode( kind::EQUAL, s, NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, cc ) ); - ret.push_back( cc_eq ); + nn.push_back( cc_eq ); } break; case kind::REGEXP_OR: { std::vector< Node > c_or; for(unsigned i=0; imkNode( kind::OR, c_or ); ret.push_back( eq ); @@ -55,21 +55,9 @@ void StringsPreprocess::simplifyRegExp( Node s, Node r, std::vector< Node > &ret break; case kind::REGEXP_INTER: for(unsigned i=0; imkNode( kind::EQUAL, s, NodeManager::currentNM()->mkConst( ::CVC4::String("") ) ); - std::vector< Node > rr; - simplifyRegExp( s, r[0], rr ); - Node nrr = rr.size()==1 ? rr[0] : NodeManager::currentNM()->mkNode( kind::AND, rr ); - ret.push_back( NodeManager::currentNM()->mkNode( kind::OR, eq_empty, nrr) ); - } - break; - //case kind::REGEXP_PLUS: - */ case kind::REGEXP_STAR: { Node eq = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, s, r ); @@ -78,6 +66,8 @@ void StringsPreprocess::simplifyRegExp( Node s, Node r, std::vector< Node > &ret break; default: //TODO: special sym: sigma, none, all + Trace("strings-preprocess") << "Unsupported term: " << r << " in simplifyRegExp." << std::endl; + Assert( false ); break; } } @@ -99,26 +89,27 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { return (*i).second.isNull() ? t : (*i).second; } - /* - if( t.getKind() == kind::STRING_IN_REGEXP ){ + Trace("strings-preprocess") << "StringsPreprocess::simplify: " << t << std::endl; + Node retNode = t; + if( t.getKind() == kind::STRING_IN_REGEXP ) { // t0 in t1 Node t0 = simplify( t[0], new_nodes ); //if(!checkStarPlus( t[1] )) { //rewrite it std::vector< Node > ret; - simplifyRegExp( t0, t[1], ret ); + std::vector< Node > nn; + simplifyRegExp( t0, t[1], ret, nn ); + new_nodes.insert( new_nodes.end(), nn.begin(), nn.end() ); Node n = ret.size() == 1 ? ret[0] : NodeManager::currentNM()->mkNode( kind::AND, ret ); d_cache[t] = (t == n) ? Node::null() : n; - return n; + retNode = n; //} else { // TODO // return (t0 == t[0]) ? t : NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, t0, t[1] ); //} - }else - */ - if( t.getKind() == kind::STRING_SUBSTR ){ + } else if( t.getKind() == kind::STRING_SUBSTR ){ Node sk1 = NodeManager::currentNM()->mkSkolem( "st1sym_$$", t.getType(), "created for substr" ); Node sk2 = NodeManager::currentNM()->mkSkolem( "st2sym_$$", t.getType(), "created for substr" ); Node sk3 = NodeManager::currentNM()->mkSkolem( "st3sym_$$", t.getType(), "created for substr" ); @@ -134,7 +125,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { new_nodes.push_back( len_sk2_eq_j ); d_cache[t] = sk2; - return sk2; + retNode = sk2; } else if( t.getNumChildren()>0 ){ std::vector< Node > cc; if (t.getMetaKind() == kind::metakind::PARAMETERIZED) { @@ -149,15 +140,26 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { if(changed) { Node n = NodeManager::currentNM()->mkNode( t.getKind(), cc ); d_cache[t] = n; - return n; + retNode = n; } else { d_cache[t] = Node::null(); - return t; + retNode = t; } }else{ d_cache[t] = Node::null(); - return t; + retNode = t; } + + Trace("strings-preprocess") << "StringsPreprocess::simplify returns: " << retNode << std::endl; + if(!new_nodes.empty()) { + Trace("strings-preprocess") << " ... new nodes:"; + for(unsigned int i=0; i &vec_node) { diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h index ce00a75ce..7bc60c1a1 100644 --- a/src/theory/strings/theory_strings_preprocess.h +++ b/src/theory/strings/theory_strings_preprocess.h @@ -32,10 +32,10 @@ class StringsPreprocess { std::hash_map d_cache; private: bool checkStarPlus( Node t ); - void simplifyRegExp( Node s, Node r, std::vector< Node > &ret ); + void simplifyRegExp( Node s, Node r, std::vector< Node > &ret, std::vector< Node > &nn ); Node simplify( Node t, std::vector< Node > &new_nodes ); public: -void simplify(std::vector< Node > &vec_node); + void simplify(std::vector< Node > &vec_node); }; }/* CVC4::theory::strings namespace */ diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 31203b767..7b74a95ac 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -21,7 +21,7 @@ using namespace CVC4::kind; using namespace CVC4::theory; using namespace CVC4::theory::strings; -Node TheoryStringsRewriter::rewriteConcatString(TNode node) { +Node TheoryStringsRewriter::rewriteConcatString( TNode node ) { Trace("strings-prerewrite") << "Strings::rewriteConcatString start " << node << std::endl; Node retNode = node; std::vector node_vec; @@ -81,6 +81,70 @@ Node TheoryStringsRewriter::rewriteConcatString(TNode node) { return retNode; } +Node TheoryStringsRewriter::prerewriteConcatRegExp( TNode node ) { + Assert( node.getKind() == kind::REGEXP_CONCAT ); + Trace("strings-prerewrite") << "Strings::prerewriteConcatRegExp start " << node << std::endl; + Node retNode = node; + std::vector node_vec; + Node preNode = Node::null(); + for(unsigned int i=0; imkNode( kind::STRING_CONCAT, preNode, tmpNode[0][0] ) ); + node_vec.push_back( NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, preNode ) ); + preNode = Node::null(); + ++j; + } else { + node_vec.push_back( NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, preNode ) ); + preNode = Node::null(); + node_vec.push_back( tmpNode[0] ); + ++j; + } + } + for(; jmkNode( kind::STRING_CONCAT, preNode, tmpNode[0] ) ); + } + } else { + if(!preNode.isNull()) { + if(preNode.getKind() == kind::CONST_STRING && preNode.getConst().isEmptyString() ) { + preNode = Node::null(); + } else { + node_vec.push_back( NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, preNode ) ); + preNode = Node::null(); + } + } + node_vec.push_back( tmpNode ); + } + } + if(!preNode.isNull()) { + node_vec.push_back( NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, preNode ) ); + } + if(node_vec.size() > 1) { + retNode = NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, node_vec); + } else { + retNode = node_vec[0]; + } + Trace("strings-prerewrite") << "Strings::prerewriteConcatRegExp end " << retNode << std::endl; + return retNode; +} + void TheoryStringsRewriter::simplifyRegExp( Node s, Node r, std::vector< Node > &ret ) { int k = r.getKind(); switch( k ) { @@ -131,7 +195,7 @@ void TheoryStringsRewriter::simplifyRegExp( Node s, Node r, std::vector< Node > break; } } -bool TheoryStringsRewriter::checkConstRegExp( Node t ) { +bool TheoryStringsRewriter::checkConstRegExp( TNode t ) { if( t.getKind() != kind::STRING_TO_REGEXP ) { for( unsigned i = 0; i(); retNode = NodeManager::currentNM()->mkConst( testConstStringInRegExp( s, 0, node[1] ) ); } else { - if( node[1].getKind() == kind::REGEXP_STAR ) { + //if( node[1].getKind() == kind::REGEXP_STAR ) { if( x == node[0] ) { retNode = node; } else { retNode = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, x, node[1] ); } + /* } else { std::vector node_vec; simplifyRegExp( x, node[1], node_vec ); @@ -268,6 +332,7 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) { retNode = node_vec[0]; } } + */ } //Trace("strings-prerewrite") << "Strings::rewriteMembership end " << retNode << std::endl; return retNode; @@ -347,7 +412,9 @@ RewriteResponse TheoryStringsRewriter::preRewrite(TNode node) { if(node.getKind() == kind::STRING_CONCAT) { retNode = rewriteConcatString(node); - } else if(node.getKind() == kind::REGEXP_PLUS) { + } else if(node.getKind() == kind::REGEXP_CONCAT) { + retNode = prerewriteConcatRegExp(node); + } else if(node.getKind() == kind::REGEXP_PLUS) { retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT, node[0], NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, node[0])); } else if(node.getKind() == kind::REGEXP_OPT) { diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h index 9dcfb4ce5..c416abd69 100644 --- a/src/theory/strings/theory_strings_rewriter.h +++ b/src/theory/strings/theory_strings_rewriter.h @@ -30,11 +30,12 @@ namespace strings { class TheoryStringsRewriter { public: - static bool checkConstRegExp( Node t ); - static bool testConstStringInRegExp( CVC4::String &s, unsigned int index_start, Node r ); + static bool checkConstRegExp( TNode t ); + static bool testConstStringInRegExp( CVC4::String &s, unsigned int index_start, TNode r ); static void simplifyRegExp( Node s, Node r, std::vector< Node > &ret ); static Node rewriteConcatString(TNode node); + static Node prerewriteConcatRegExp(TNode node); static Node rewriteMembership(TNode node); static RewriteResponse postRewrite(TNode node); diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h index f63cd32fc..8af063284 100644 --- a/src/theory/strings/theory_strings_type_rules.h +++ b/src/theory/strings/theory_strings_type_rules.h @@ -37,12 +37,17 @@ public: throw (TypeCheckingExceptionPrivate, AssertionException) { TNode::iterator it = n.begin(); TNode::iterator it_end = n.end(); + int size = 0; for (; it != it_end; ++ it) { TypeNode t = (*it).getType(check); if (!t.isString()) { throw TypeCheckingExceptionPrivate(n, "expecting string terms in string concat"); } + ++size; } + if(size < 2) { + throw TypeCheckingExceptionPrivate(n, "expecting at least 2 terms in string concat"); + } return nodeManager->stringType(); } }; @@ -97,12 +102,17 @@ public: throw (TypeCheckingExceptionPrivate, AssertionException) { TNode::iterator it = n.begin(); TNode::iterator it_end = n.end(); + int size = 0; for (; it != it_end; ++ it) { TypeNode t = (*it).getType(check); if (!t.isRegExp()) { - throw TypeCheckingExceptionPrivate(n, "expecting regexp terms"); + throw TypeCheckingExceptionPrivate(n, "expecting regexp terms in regexp concat"); } + ++size; } + if(size < 2) { + throw TypeCheckingExceptionPrivate(n, "expecting at least 2 terms in regexp concat"); + } return nodeManager->regexpType(); } }; diff --git a/test/regress/regress0/strings/regexp002.smt2 b/test/regress/regress0/strings/regexp002.smt2 new file mode 100644 index 000000000..e2a44a9ab --- /dev/null +++ b/test/regress/regress0/strings/regexp002.smt2 @@ -0,0 +1,19 @@ +(set-logic QF_S) +(set-info :status sat) + +(declare-fun x () String) +(declare-fun y () String) + +(assert (str.in.re x + (re.* (re.++ (re.* (str.to.re "a") ) (str.to.re "b") )) + )) + +(assert (str.in.re y + (re.* (re.++ (re.* (str.to.re "a") ) (str.to.re "b") )) + )) + +(assert (not (= x y))) +(assert (= (str.len x) (str.len y))) +(assert (= (str.len y) 3)) + +(check-sat) -- cgit v1.2.3 From fb5fcafe43c1c7fc65c852dad2b7541df0b352c8 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Tue, 15 Oct 2013 13:16:03 -0500 Subject: bug fix: string cache cleaning --- src/theory/strings/theory_strings.cpp | 112 ++++++++++++++++++++---------- src/theory/strings/theory_strings.h | 2 + test/regress/regress0/strings/Makefile.am | 1 + test/regress/regress0/strings/str006.smt2 | 14 ++++ 4 files changed, 94 insertions(+), 35 deletions(-) create mode 100644 test/regress/regress0/strings/str006.smt2 (limited to 'src') diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index cfc9fa77e..4876b54e7 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -159,14 +159,19 @@ bool TheoryStrings::propagate(TNode literal) { /** explain */ void TheoryStrings::explain(TNode literal, std::vector& assumptions){ - Debug("strings-explain") << "Explain " << literal << std::endl; + Debug("strings-explain") << "Explain " << literal << " " << d_conflict << std::endl; bool polarity = literal.getKind() != kind::NOT; TNode atom = polarity ? literal : literal[0]; + unsigned ps = assumptions.size(); 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); } + Debug("strings-explain-debug") << "Explanation for " << literal << " was " << std::endl; + for( unsigned i=ps; iconflict( conflictNode ); } - Trace("strings-conflict") << "CONFLICT: Eq engine conflict : " << conflictNode << std::endl; - d_out->conflict( conflictNode ); - d_conflict = true; } /** called when a new equivalance class is created */ @@ -549,9 +561,9 @@ void TheoryStrings::doPendingLemmas() { 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(); } + d_lemma_cache.clear(); + d_pending_req_phase.clear(); } bool TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std::vector< Node > & nf, @@ -702,6 +714,18 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v Trace("strings-process") << "Return process equivalence class " << eqc << " : already visited." << std::endl; return false; } else if( areEqual( eqc, d_emptyString ) ){ + eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); + while( !eqc_i.isFinished() ) { + Node n = (*eqc_i); + if( n.getKind()==kind::STRING_CONCAT ){ + for( unsigned i=0; i & v //need to break Node sk_w= NodeManager::currentNM()->mkSkolem( "w_loop_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); Node ant = mkExplain( antec, antec_new_lits ); + Node str_in_re; if(index == loop_index - 1 && other_index + 2 == (int) normal_forms[other_n_index].size() && loop_index + 1 == (int) normal_forms[loop_n_index].size() && @@ -929,11 +954,10 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v Trace("strings-loop") << "... (C)=" << normal_forms[loop_n_index][index] << " " << std::endl; //special case Node conc3 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[other_n_index][other_index], mkConcat( normal_forms[loop_n_index][index], sk_w ) ); - Node conc4 = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, sk_w, - NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, - NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, normal_forms[loop_n_index][index] ) ) ); - unrollStar( conc4 ); - conc = conc4; + str_in_re = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, sk_w, + NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, + NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, normal_forms[loop_n_index][index] ) ) ); + conc = str_in_re; } else { Node sk_y= NodeManager::currentNM()->mkSkolem( "y_loop_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); Node sk_z= NodeManager::currentNM()->mkSkolem( "z_loop_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); @@ -962,10 +986,9 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v Node conc2 = NodeManager::currentNM()->mkNode( kind::EQUAL, left2, mkConcat( c3c ) ); Node conc3 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[other_n_index][other_index], mkConcat( sk_y, sk_w ) ); - Node conc4 = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, sk_w, + str_in_re = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, sk_w, NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, mkConcat( sk_z, sk_y ) ) ) ); - unrollStar( conc4 ); //Node sk_y_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_y ); //Node sk_z_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_z ); @@ -979,12 +1002,17 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v //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 ); - conc = NodeManager::currentNM()->mkNode( kind::AND, conc1, conc2, conc3, conc4 );//, x_eq_y_rest );// , z_neq_empty //, len_x_gt_len_y + conc = NodeManager::currentNM()->mkNode( kind::AND, conc1, conc2, conc3, str_in_re );//, 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 ); } // normal case + //set its antecedant to ant, to say when it is relevant + d_reg_exp_ant[str_in_re] = ant; + //unroll the str in re constraint once + unrollStar( str_in_re ); + //we will be done addNormalFormPair( normal_form_src[i], normal_form_src[j] ); //Assert( isNormalFormPair( normal_form_src[i], normal_form_src[j] ) ); @@ -1302,24 +1330,30 @@ Node TheoryStrings::mkExplain( std::vector< Node >& a ) { Node TheoryStrings::mkExplain( std::vector< Node >& a, std::vector< Node >& an ) { std::vector< TNode > antec_exp; for( unsigned i=0; i eqcs; @@ -1547,7 +1582,7 @@ bool TheoryStrings::checkNormalForms() { } //flush pending lemmas - if( !d_conflict && !d_lemma_cache.empty() ){ + if( !d_lemma_cache.empty() ){ doPendingLemmas(); return true; }else{ @@ -1796,6 +1831,9 @@ bool TheoryStrings::unrollStar( Node atom ) { Node unr3 = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, sk_xp, r ); unr3 = Rewriter::rewrite( unr3 ); d_reg_exp_unroll_depth[unr3] = depth + 1; + if( d_reg_exp_ant.find( atom )!=d_reg_exp_ant.end() ){ + d_reg_exp_ant[unr3] = d_reg_exp_ant[atom]; + } //|x|>|xp| Node len_x_gt_len_xp = NodeManager::currentNM()->mkNode( kind::GT, @@ -1804,7 +1842,11 @@ bool TheoryStrings::unrollStar( Node atom ) { Node unr = NodeManager::currentNM()->mkNode( kind::AND, unr0, urc[0], unr2, unr3, len_x_gt_len_xp ); Node lem = NodeManager::currentNM()->mkNode( kind::OR, xeqe, unr ); - sendLemma( atom, lem, "Unroll" ); + Node ant = atom; + if( d_reg_exp_ant.find( atom )!=d_reg_exp_ant.end() ){ + ant = d_reg_exp_ant[atom]; + } + sendLemma( ant, lem, "Unroll" ); return true; }else{ return false; @@ -1819,9 +1861,9 @@ bool TheoryStrings::checkMemberships() { Node assertion = d_reg_exp_mem[i]; Trace("strings-regex") << "We have regular expression assertion : " << assertion << std::endl; Node atom = assertion.getKind()==kind::NOT ? assertion[0] : assertion; - if( d_reg_exp_unroll.find(atom)==d_reg_exp_unroll.end() ){ - bool polarity = assertion.getKind()!=kind::NOT; - if( polarity ){ + bool polarity = assertion.getKind()!=kind::NOT; + if( polarity ){ + if( d_reg_exp_unroll.find(atom)==d_reg_exp_unroll.end() ){ Assert( atom.getKind()==kind::STRING_IN_REGEXP ); Node x = atom[0]; Node r = atom[1]; @@ -1838,12 +1880,12 @@ bool TheoryStrings::checkMemberships() { Trace("strings-regex") << "...is satisfied." << std::endl; } }else{ - //TODO: negative membership - Trace("strings-regex") << "RegEx is incomplete due to " << assertion << "." << std::endl; - is_unk = true; + Trace("strings-regex") << "...Already unrolled." << std::endl; } }else{ - Trace("strings-regex") << "...Already unrolled." << std::endl; + //TODO: negative membership + Trace("strings-regex") << "RegEx is incomplete due to " << assertion << "." << std::endl; + is_unk = true; } } if( addedLemma ){ diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index d059d8bba..d043f06ec 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -150,6 +150,8 @@ class TheoryStrings : public Theory { NodeList d_reg_exp_mem; std::map< Node, bool > d_reg_exp_unroll; std::map< Node, int > d_reg_exp_unroll_depth; + //antecedant for why reg exp membership must be true + std::map< Node, Node > d_reg_exp_ant; ///////////////////////////////////////////////////////////////////////////// // MODEL GENERATION diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index 66827b578..49a431796 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -25,6 +25,7 @@ TESTS = \ str003.smt2 \ str004.smt2 \ str005.smt2 \ + str006.smt2 \ model001.smt2 \ substr001.smt2 \ regexp001.smt2 \ diff --git a/test/regress/regress0/strings/str006.smt2 b/test/regress/regress0/strings/str006.smt2 new file mode 100644 index 000000000..592ef6a7f --- /dev/null +++ b/test/regress/regress0/strings/str006.smt2 @@ -0,0 +1,14 @@ +(set-logic QF_S) +(set-info :status sat) + +(declare-fun x () String) +(declare-fun y () String) +(declare-fun z () String) + +;plandowski p469 1 +(assert (= (str.++ x "ab" y) (str.++ y "ba" z))) +(assert (= z (str.++ x y))) +(assert (not (= (str.++ x "a") (str.++ "a" x)))) + +(check-sat) + -- cgit v1.2.3 From 933476285f9ff95278802a58645ba0b29f1d22af Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 15 Oct 2013 14:23:20 -0500 Subject: performance optimizations for quantifier instantiation --- src/theory/quantifiers_engine.cpp | 94 +++++++++++++++++++++++---------------- src/theory/quantifiers_engine.h | 10 ++--- 2 files changed, 59 insertions(+), 45 deletions(-) (limited to 'src') diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index c14ee01ce..07b0ebea3 100755 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -283,32 +283,32 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std d_temp_inst_debug[f]++; d_total_inst_count_debug++; Trace("inst") << "*** Instantiate " << f << " with " << std::endl; - uint64_t maxInstLevel = 0; - for( int i=0; i<(int)terms.size(); i++ ){ - if( quantifiers::TermDb::hasInstConstAttr(terms[i]) ){ - Debug("inst")<< "***& Bad Instantiate " << f << " with " << std::endl; - for( int i=0; i<(int)terms.size(); i++ ){ - Debug("inst") << " " << terms[i] << std::endl; - } - Unreachable("Bad instantiation"); - }else{ - Trace("inst") << " " << terms[i]; - //Debug("inst-engine") << " " << terms[i].getAttribute(InstLevelAttribute()); - Trace("inst") << std::endl; - if( terms[i].hasAttribute(InstLevelAttribute()) ){ - if( terms[i].getAttribute(InstLevelAttribute())>maxInstLevel ){ - maxInstLevel = terms[i].getAttribute(InstLevelAttribute()); + //uint64_t maxInstLevel = 0; + if( options::cbqi() ){ + for( int i=0; i<(int)terms.size(); i++ ){ + if( quantifiers::TermDb::hasInstConstAttr(terms[i]) ){ + Debug("inst")<< "***& Bad Instantiate " << f << " with " << std::endl; + for( int i=0; i<(int)terms.size(); i++ ){ + Debug("inst") << " " << terms[i] << std::endl; } + Unreachable("Bad instantiation"); }else{ - setInstantiationLevelAttr( terms[i], 0 ); + Trace("inst") << " " << terms[i]; + //Debug("inst-engine") << " " << terms[i].getAttribute(InstLevelAttribute()); + Trace("inst") << std::endl; + //if( terms[i].hasAttribute(InstLevelAttribute()) ){ + //if( terms[i].getAttribute(InstLevelAttribute())>maxInstLevel ){ + // maxInstLevel = terms[i].getAttribute(InstLevelAttribute()); + //} + //}else{ + //setInstantiationLevelAttr( terms[i], 0 ); + //} } } } Trace("inst-debug") << "*** Lemma is " << lem << std::endl; - setInstantiationLevelAttr( body, maxInstLevel+1 ); + //setInstantiationLevelAttr( body, maxInstLevel+1 ); ++(d_statistics.d_instantiations); - d_statistics.d_total_inst_var += (int)terms.size(); - d_statistics.d_max_instantiation_level.maxAssign( maxInstLevel+1 ); return true; }else{ ++(d_statistics.d_inst_duplicate); @@ -326,10 +326,32 @@ void QuantifiersEngine::setInstantiationLevelAttr( Node n, uint64_t level ){ } } +Node QuantifiersEngine::doSubstitute( Node n, std::vector< Node >& terms ){ + if( n.getKind()==INST_CONSTANT ){ + Debug("check-inst") << "Substitute inst constant : " << n << std::endl; + return terms[n.getAttribute(InstVarNumAttribute())]; + }else if( !quantifiers::TermDb::hasInstConstAttr( n ) ){ + Debug("check-inst") << "No inst const attr : " << n << std::endl; + return n; + }else{ + Debug("check-inst") << "Recurse on : " << n << std::endl; + std::vector< Node > cc; + if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ + cc.push_back( n.getOperator() ); + } + for( unsigned i=0; imkNode( n.getKind(), cc ); + } +} + + Node QuantifiersEngine::getInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ){ - Node body = f[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); + Node body; //process partial instantiation if necessary if( d_term_db->d_vars[f].size()!=vars.size() ){ + body = f[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); std::vector< Node > uninst_vars; //doing a partial instantiation, must add quantifier for all uninstantiated variables for( int i=0; i<(int)f[0].getNumChildren(); i++ ){ @@ -341,6 +363,16 @@ Node QuantifiersEngine::getInstantiation( Node f, std::vector< Node >& vars, std body = NodeManager::currentNM()->mkNode( FORALL, bvl, body ); Trace("partial-inst") << "Partial instantiation : " << f << std::endl; Trace("partial-inst") << " : " << body << std::endl; + }else{ + //do optimized version + Node icb = d_term_db->getInstConstantBody( f ); + body = doSubstitute( icb, terms ); + if( Debug.isOn("check-inst") ){ + Node body2 = f[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); + if( body!=body2 ){ + Debug("check-inst") << "Substitution is wrong : " << body << " " << body2 << std::endl; + } + } } return body; } @@ -440,11 +472,7 @@ bool QuantifiersEngine::addSplit( Node n, bool reqPhase, bool reqPhasePol ){ n = Rewriter::rewrite( n ); Node lem = NodeManager::currentNM()->mkNode( OR, n, n.notNode() ); if( addLemma( lem ) ){ - ++(d_statistics.d_splits); Debug("inst") << "*** Add split " << n<< std::endl; - //if( reqPhase ){ - // d_curr_out->requirePhase( n, reqPhasePol ); - //} return true; } return false; @@ -503,12 +531,8 @@ QuantifiersEngine::Statistics::Statistics(): d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0), d_instantiation_rounds_lc("QuantifiersEngine::Rounds_Instantiation_Last_Call", 0), d_instantiations("QuantifiersEngine::Instantiations_Total", 0), - d_max_instantiation_level("QuantifiersEngine::Max_Instantiation_Level", 0), - d_splits("QuantifiersEngine::Total_Splits", 0), - d_total_inst_var("QuantifiersEngine::Vars_Inst", 0), - d_total_inst_var_unspec("QuantifiersEngine::Vars_Inst_Unspecified", 0), - d_inst_unspec("QuantifiersEngine::Unspecified_Inst", 0), d_inst_duplicate("QuantifiersEngine::Duplicate_Inst", 0), + d_inst_duplicate_eq("QuantifiersEngine::Duplicate_Inst_Eq", 0), d_lit_phase_req("QuantifiersEngine::lit_phase_req", 0), d_lit_phase_nreq("QuantifiersEngine::lit_phase_nreq", 0), d_triggers("QuantifiersEngine::Triggers", 0), @@ -528,12 +552,8 @@ QuantifiersEngine::Statistics::Statistics(): StatisticsRegistry::registerStat(&d_instantiation_rounds); StatisticsRegistry::registerStat(&d_instantiation_rounds_lc); StatisticsRegistry::registerStat(&d_instantiations); - StatisticsRegistry::registerStat(&d_max_instantiation_level); - StatisticsRegistry::registerStat(&d_splits); - StatisticsRegistry::registerStat(&d_total_inst_var); - StatisticsRegistry::registerStat(&d_total_inst_var_unspec); - StatisticsRegistry::registerStat(&d_inst_unspec); StatisticsRegistry::registerStat(&d_inst_duplicate); + StatisticsRegistry::registerStat(&d_inst_duplicate_eq); StatisticsRegistry::registerStat(&d_lit_phase_req); StatisticsRegistry::registerStat(&d_lit_phase_nreq); StatisticsRegistry::registerStat(&d_triggers); @@ -555,12 +575,8 @@ QuantifiersEngine::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_instantiation_rounds); StatisticsRegistry::unregisterStat(&d_instantiation_rounds_lc); StatisticsRegistry::unregisterStat(&d_instantiations); - StatisticsRegistry::unregisterStat(&d_max_instantiation_level); - StatisticsRegistry::unregisterStat(&d_splits); - StatisticsRegistry::unregisterStat(&d_total_inst_var); - StatisticsRegistry::unregisterStat(&d_total_inst_var_unspec); - StatisticsRegistry::unregisterStat(&d_inst_unspec); StatisticsRegistry::unregisterStat(&d_inst_duplicate); + StatisticsRegistry::unregisterStat(&d_inst_duplicate_eq); StatisticsRegistry::unregisterStat(&d_lit_phase_req); StatisticsRegistry::unregisterStat(&d_lit_phase_nreq); StatisticsRegistry::unregisterStat(&d_triggers); diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 8f645afe7..6de13ff3c 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -111,7 +111,7 @@ private: /** list of all quantifiers seen */ std::vector< Node > d_quants; /** list of all lemmas produced */ - std::map< Node, bool > d_lemmas_produced; + //std::map< Node, bool > d_lemmas_produced; BoolMap d_lemmas_produced_c; /** lemmas waiting */ std::vector< Node > d_lemmas_waiting; @@ -187,6 +187,8 @@ private: bool addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ); /** set instantiation level attr */ void setInstantiationLevelAttr( Node n, uint64_t level ); + /** do substitution */ + Node doSubstitute( Node n, std::vector< Node >& terms ); public: /** get instantiation */ Node getInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ); @@ -234,12 +236,8 @@ public: IntStat d_instantiation_rounds; IntStat d_instantiation_rounds_lc; IntStat d_instantiations; - IntStat d_max_instantiation_level; - IntStat d_splits; - IntStat d_total_inst_var; - IntStat d_total_inst_var_unspec; - IntStat d_inst_unspec; IntStat d_inst_duplicate; + IntStat d_inst_duplicate_eq; IntStat d_lit_phase_req; IntStat d_lit_phase_nreq; IntStat d_triggers; -- cgit v1.2.3 From bd802fbda59ec07fe74c6843de21717843846610 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Tue, 15 Oct 2013 14:23:08 -0500 Subject: removes some junks --- src/theory/strings/theory_strings_preprocess.cpp | 10 ++- src/theory/strings/theory_strings_rewriter.cpp | 78 ++---------------------- src/theory/strings/theory_strings_rewriter.h | 1 - 3 files changed, 11 insertions(+), 78 deletions(-) (limited to 'src') diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 378fa3428..c54cbb3b2 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -34,9 +34,13 @@ void StringsPreprocess::simplifyRegExp( Node s, Node r, std::vector< Node > &ret { std::vector< Node > cc; for(unsigned i=0; imkSkolem( "recsym_$$", s.getType(), "created for regular expression concat" ); - simplifyRegExp( sk, r[i], ret, nn ); - cc.push_back( sk ); + if(r[i].getKind() == kind::STRING_TO_REGEXP) { + cc.push_back( r[i][0] ); + } else { + Node sk = NodeManager::currentNM()->mkSkolem( "recsym_$$", s.getType(), "created for regular expression concat" ); + simplifyRegExp( sk, r[i], ret, nn ); + cc.push_back( sk ); + } } Node cc_eq = NodeManager::currentNM()->mkNode( kind::EQUAL, s, NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, cc ) ); diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 7b74a95ac..5ba67c25f 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -145,56 +145,6 @@ Node TheoryStringsRewriter::prerewriteConcatRegExp( TNode node ) { return retNode; } -void TheoryStringsRewriter::simplifyRegExp( Node s, Node r, std::vector< Node > &ret ) { - int k = r.getKind(); - switch( k ) { - case kind::STRING_TO_REGEXP: - { - Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, s, r[0] ); - ret.push_back( eq ); - } - break; - case kind::REGEXP_CONCAT: - { - std::vector< Node > cc; - for(unsigned i=0; imkSkolem( "recsym_$$", s.getType(), "created for regular expression concat" ); - simplifyRegExp( sk, r[i], ret ); - cc.push_back( sk ); - } - Node cc_eq = NodeManager::currentNM()->mkNode( kind::EQUAL, s, - NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, cc ) ); - ret.push_back( cc_eq ); - } - break; - case kind::REGEXP_OR: - { - std::vector< Node > c_or; - for(unsigned i=0; imkNode( kind::OR, c_or ); - ret.push_back( eq ); - } - break; - case kind::REGEXP_INTER: - for(unsigned i=0; imkNode( kind::STRING_IN_REGEXP, s, r ); - ret.push_back( eq ); - } - break; - default: - //TODO: special sym: sigma, none, all - Trace("strings-prerewrite") << "Unsupported term: " << r << " in simplifyRegExp." << std::endl; - Assert( false ); - break; - } -} bool TheoryStringsRewriter::checkConstRegExp( TNode t ) { if( t.getKind() != kind::STRING_TO_REGEXP ) { for( unsigned i = 0; i(); retNode = NodeManager::currentNM()->mkConst( testConstStringInRegExp( s, 0, node[1] ) ); } else { - //if( node[1].getKind() == kind::REGEXP_STAR ) { - if( x == node[0] ) { - retNode = node; - } else { - retNode = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, x, node[1] ); - } - /* - } else { - std::vector node_vec; - simplifyRegExp( x, node[1], node_vec ); - - if(node_vec.size() > 1) { - retNode = NodeManager::currentNM()->mkNode(kind::AND, node_vec); - } else { - retNode = node_vec[0]; - } + if( x != node[0] ) { + retNode = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, x, node[1] ); } - */ } - //Trace("strings-prerewrite") << "Strings::rewriteMembership end " << retNode << std::endl; return retNode; } diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h index c416abd69..e7d7eccb5 100644 --- a/src/theory/strings/theory_strings_rewriter.h +++ b/src/theory/strings/theory_strings_rewriter.h @@ -32,7 +32,6 @@ class TheoryStringsRewriter { public: static bool checkConstRegExp( TNode t ); static bool testConstStringInRegExp( CVC4::String &s, unsigned int index_start, TNode r ); - static void simplifyRegExp( Node s, Node r, std::vector< Node > &ret ); static Node rewriteConcatString(TNode node); static Node prerewriteConcatRegExp(TNode node); -- cgit v1.2.3 From eac3a8fd34c34b083f26ca0491f89a2140f59115 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Tue, 15 Oct 2013 17:23:51 -0500 Subject: bug fix in strings : change from assert to alwaysassert --- src/theory/strings/kinds | 2 +- src/theory/strings/options | 7 +++++-- src/theory/strings/theory_strings.cpp | 29 +++++++++++++++++++---------- src/theory/strings/theory_strings.h | 4 ++++ 4 files changed, 29 insertions(+), 13 deletions(-) (limited to 'src') diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index fe7b9b3d9..f4fbd7194 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -3,7 +3,7 @@ theory THEORY_STRINGS ::CVC4::theory::strings::TheoryStrings "theory/strings/theory_strings.h" -properties check parametric propagate +properties check parametric propagate getNextDecisionRequest rewriter ::CVC4::theory::strings::TheoryStringsRewriter "theory/strings/theory_strings_rewriter.h" diff --git a/src/theory/strings/options b/src/theory/strings/options index 3fceb06d4..2832c7833 100644 --- a/src/theory/strings/options +++ b/src/theory/strings/options @@ -6,9 +6,12 @@ module STRINGS "theory/strings/options.h" Strings theory option stringCharCardinality str-alphabet-card --str-alphabet-card=N int16_t :default 256 :read-write - the cardinality of the characters used by the theory of string, default 256 + the cardinality of the characters used by the theory of strings, default 256 option stringRegExpUnrollDepth str-regexp-depth --str-regexp-depth=N int16_t :default 10 :read-write - the depth of unrolloing regular expression used by the theory of string, default 10 + the depth of unrolloing regular expression used by the theory of strings, default 10 + +option stringFMF fmf-strings --fmf-strings bool :default false + the finite model finding used by the theory of strings endmodule diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 4876b54e7..1aae55a83 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -61,6 +61,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu //option d_regexp_unroll_depth = options::stringRegExpUnrollDepth(); + d_fmf = options::stringFMF(); } TheoryStrings::~TheoryStrings() { @@ -343,6 +344,12 @@ void TheoryStrings::preRegisterTerm(TNode n) { Trace("strings-lemma") << "Strings: Add lemma " << n_len_geq_zero << std::endl; d_out->lemma(n_len_geq_zero); } + // FMF + if( d_fmf && n.getKind() == kind::VARIABLE ) { + if( std::find(d_in_vars.begin(), d_in_vars.end(), n) == d_in_vars.end() ) { + d_in_vars.push_back( n ); + } + } } if (n.getType().isBoolean()) { // Get triggered for both equal and dis-equal @@ -1343,7 +1350,7 @@ Node TheoryStrings::mkExplain( std::vector< Node >& a, std::vector< Node >& an ) } 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) ); + AlwaysAssert( d_equalityEngine.areDisequal(a[i][0][0], a[i][0][1], true) ); } if( exp ){ unsigned ps = antec_exp.size(); @@ -1900,18 +1907,20 @@ bool TheoryStrings::checkMemberships() { } } -/* Node TheoryStrings::getNextDecisionRequest() { - if( d_lit_to_decide_index.get()::iterator itr = d_in_vars.begin(); + itr != d_in_vars.end(); ++itr) { + Trace("strings-fmf-debug") << " " << (*itr) ; + } + Trace("strings-fmf-debug") << std::endl; } + + return Node::null(); } -*/ + }/* CVC4::theory::strings namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index d043f06ec..7f2dce5ae 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -60,6 +60,7 @@ class TheoryStrings : public Theory { bool propagate(TNode literal); void explain( TNode literal, std::vector& assumptions ); Node explain( TNode literal ); + Node getNextDecisionRequest(); // NotifyClass for equality engine @@ -126,6 +127,9 @@ class TheoryStrings : public Theory { Node d_true; Node d_false; Node d_zero; + // Finite Model Finding + bool d_fmf; + std::vector< Node > d_in_vars; // RegExp depth int d_regexp_unroll_depth; //list of pairs of nodes to merge -- cgit v1.2.3 From 04868401c51b7f29c2b43ebc508dea59769dae93 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Wed, 16 Oct 2013 10:16:59 -0500 Subject: renames for strings fmf --- src/theory/strings/options | 2 +- src/theory/strings/theory_strings.cpp | 4 +++- 2 files changed, 4 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/theory/strings/options b/src/theory/strings/options index 2832c7833..58cbbc1b1 100644 --- a/src/theory/strings/options +++ b/src/theory/strings/options @@ -11,7 +11,7 @@ option stringCharCardinality str-alphabet-card --str-alphabet-card=N int16_t :de option stringRegExpUnrollDepth str-regexp-depth --str-regexp-depth=N int16_t :default 10 :read-write the depth of unrolloing regular expression used by the theory of strings, default 10 -option stringFMF fmf-strings --fmf-strings bool :default false +option stringFMF strings-fmf --str-fmf bool :default false the finite model finding used by the theory of strings endmodule diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 1aae55a83..c4ecd02cf 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -1908,7 +1908,7 @@ bool TheoryStrings::checkMemberships() { } Node TheoryStrings::getNextDecisionRequest() { - if(d_fmf) { + if(d_fmf && !d_conflict) { Trace("strings-decide") << "Get next decision request." << std::endl; Trace("strings-fmf-debug") << "Input variables: "; for(std::vector< Node >::iterator itr = d_in_vars.begin(); @@ -1916,6 +1916,8 @@ Node TheoryStrings::getNextDecisionRequest() { Trace("strings-fmf-debug") << " " << (*itr) ; } Trace("strings-fmf-debug") << std::endl; + + } return Node::null(); -- cgit v1.2.3 From 7284a228b22fb82740faf2abdfe5cb3fc3894ae9 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Wed, 16 Oct 2013 13:24:56 -0500 Subject: adds fmf for strings --- src/theory/strings/options | 2 +- src/theory/strings/theory_strings.cpp | 64 +++++++++++++++++++++++++------ src/theory/strings/theory_strings.h | 18 ++++++--- test/regress/regress0/strings/Makefile.am | 1 + test/regress/regress0/strings/fmf001.smt2 | 19 +++++++++ 5 files changed, 87 insertions(+), 17 deletions(-) create mode 100644 test/regress/regress0/strings/fmf001.smt2 (limited to 'src') diff --git a/src/theory/strings/options b/src/theory/strings/options index 58cbbc1b1..2832c7833 100644 --- a/src/theory/strings/options +++ b/src/theory/strings/options @@ -11,7 +11,7 @@ option stringCharCardinality str-alphabet-card --str-alphabet-card=N int16_t :de option stringRegExpUnrollDepth str-regexp-depth --str-regexp-depth=N int16_t :default 10 :read-write the depth of unrolloing regular expression used by the theory of strings, default 10 -option stringFMF strings-fmf --str-fmf bool :default false +option stringFMF fmf-strings --fmf-strings bool :default false the finite model finding used by the theory of strings endmodule diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index c4ecd02cf..8bff4dddc 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -47,7 +47,8 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu //d_ind_map_lemma(c), //d_lit_to_decide_index( c, 0 ), //d_lit_to_decide( c ), - d_reg_exp_mem( c ) + d_reg_exp_mem( c ), + d_curr_cardinality( c, 0 ) { // The kinds we are treating as function application in congruence //d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP); @@ -61,7 +62,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu //option d_regexp_unroll_depth = options::stringRegExpUnrollDepth(); - d_fmf = options::stringFMF(); + //d_fmf = options::stringFMF(); } TheoryStrings::~TheoryStrings() { @@ -345,7 +346,7 @@ void TheoryStrings::preRegisterTerm(TNode n) { d_out->lemma(n_len_geq_zero); } // FMF - if( d_fmf && n.getKind() == kind::VARIABLE ) { + if( options::stringFMF() && n.getKind() == kind::VARIABLE ) { if( std::find(d_in_vars.begin(), d_in_vars.end(), n) == d_in_vars.end() ) { d_in_vars.push_back( n ); } @@ -1908,21 +1909,62 @@ bool TheoryStrings::checkMemberships() { } Node TheoryStrings::getNextDecisionRequest() { - if(d_fmf && !d_conflict) { - Trace("strings-decide") << "Get next decision request." << std::endl; - Trace("strings-fmf-debug") << "Input variables: "; - for(std::vector< Node >::iterator itr = d_in_vars.begin(); - itr != d_in_vars.end(); ++itr) { + if(options::stringFMF() && !d_conflict) { + //initialize the term we will minimize + if( d_in_var_lsum.isNull() && !d_in_vars.empty() ){ + Trace("strings-fmf-debug") << "Input variables: "; + std::vector< Node > ll; + for(std::vector< Node >::iterator itr = d_in_vars.begin(); + itr != d_in_vars.end(); ++itr) { Trace("strings-fmf-debug") << " " << (*itr) ; + ll.push_back( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, *itr ) ); } - Trace("strings-fmf-debug") << std::endl; - - + Trace("strings-fmf-debug") << std::endl; + d_in_var_lsum = ll.size()==1 ? ll[0] : NodeManager::currentNM()->mkNode( kind::PLUS, ll ); + d_in_var_lsum = Rewriter::rewrite( d_in_var_lsum ); + } + if( !d_in_var_lsum.isNull() ){ + //Trace("strings-fmf") << "Get next decision request." << std::endl; + //check if we need to decide on something + int decideCard = d_curr_cardinality.get(); + if( d_cardinality_lits.find( decideCard )!=d_cardinality_lits.end() ){ + bool value; + if( d_valuation.hasSatValue( d_cardinality_lits[ d_curr_cardinality.get() ], value ) ) { + if( !value ){ + d_curr_cardinality.set( d_curr_cardinality.get() + 1 ); + decideCard = d_curr_cardinality.get(); + Trace("strings-fmf-debug") << "Has false SAT value, increment and decide." << std::endl; + }else{ + decideCard = -1; + Trace("strings-fmf-debug") << "Has true SAT value, do not decide." << std::endl; + } + }else{ + Trace("strings-fmf-debug") << "No SAT value, decide." << std::endl; + } + } + if( decideCard!=-1 ){ + if( d_cardinality_lits.find( decideCard )==d_cardinality_lits.end() ){ + Node lit = NodeManager::currentNM()->mkNode( kind::LEQ, d_in_var_lsum, NodeManager::currentNM()->mkConst( Rational( decideCard ) ) ); + lit = Rewriter::rewrite( lit ); + d_cardinality_lits[decideCard] = lit; + Node lem = NodeManager::currentNM()->mkNode( kind::OR, lit, lit.negate() ); + Trace("strings-fmf") << "Strings FMF: Add split lemma " << lem << ", decideCard = " << decideCard << std::endl; + d_out->lemma( lem ); + d_out->requirePhase( lit, true ); + } + Trace("strings-fmf") << "Strings FMF: Decide positive on " << d_cardinality_lits[ decideCard ] << std::endl; + return d_cardinality_lits[ decideCard ]; + } + } } return Node::null(); } +void TheoryStrings::assertNode( Node lit ) { + +} + }/* CVC4::theory::strings namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 7f2dce5ae..69875edf4 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -60,7 +60,6 @@ class TheoryStrings : public Theory { bool propagate(TNode literal); void explain( TNode literal, std::vector& assumptions ); Node explain( TNode literal ); - Node getNextDecisionRequest(); // NotifyClass for equality engine @@ -127,9 +126,6 @@ class TheoryStrings : public Theory { Node d_true; Node d_false; Node d_zero; - // Finite Model Finding - bool d_fmf; - std::vector< Node > d_in_vars; // RegExp depth int d_regexp_unroll_depth; //list of pairs of nodes to merge @@ -249,8 +245,20 @@ protected: //seperate into collections with equal length void seperateByLength( std::vector< Node >& n, std::vector< std::vector< Node > >& col, std::vector< Node >& lts ); -private: void printConcat( std::vector< Node >& n, const char * c ); + +private: + // Finite Model Finding + //bool d_fmf; + std::vector< Node > d_in_vars; + Node d_in_var_lsum; + std::map< int, Node > d_cardinality_lits; + context::CDO< int > d_curr_cardinality; +public: + //for finite model finding + Node getNextDecisionRequest(); + void assertNode( Node lit ); + };/* class TheoryStrings */ }/* CVC4::theory::strings namespace */ diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index 49a431796..ffbfb077d 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -26,6 +26,7 @@ TESTS = \ str004.smt2 \ str005.smt2 \ str006.smt2 \ + fmf001.smt2 \ model001.smt2 \ substr001.smt2 \ regexp001.smt2 \ diff --git a/test/regress/regress0/strings/fmf001.smt2 b/test/regress/regress0/strings/fmf001.smt2 new file mode 100644 index 000000000..a8874b59f --- /dev/null +++ b/test/regress/regress0/strings/fmf001.smt2 @@ -0,0 +1,19 @@ +(set-logic QF_S) +(set-option :fmf-strings true) +(set-info :status sat) + +(declare-fun x () String) +(declare-fun y () String) + +(assert (str.in.re x + (re.* (re.++ (re.* (str.to.re "a") ) (str.to.re "b") )) + )) + +(assert (str.in.re y + (re.* (re.++ (re.* (str.to.re "a") ) (str.to.re "b") )) + )) + +(assert (not (= x y))) +(assert (= (str.len x) (str.len y))) + +(check-sat) -- cgit v1.2.3 From 60aab6e5b7dde21603eb039f37921614d4424d59 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Sun, 20 Oct 2013 21:25:57 -0500 Subject: adds regular expression range --- src/parser/smt2/Smt2.g | 2 ++ src/theory/strings/kinds | 2 ++ src/theory/strings/theory_strings_rewriter.cpp | 13 ++++++++++ src/theory/strings/theory_strings_type_rules.h | 34 ++++++++++++++++++++++++++ src/util/regexp.h | 8 ++++++ test/regress/regress0/strings/Makefile.am | 1 + test/regress/regress0/strings/fmf002.smt2 | 16 ++++++++++++ 7 files changed, 76 insertions(+) create mode 100644 test/regress/regress0/strings/fmf002.smt2 (limited to 'src') diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 885a7c487..c7e088124 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1255,6 +1255,7 @@ builtinOp[CVC4::Kind& kind] | RESTAR_TOK { $kind = CVC4::kind::REGEXP_STAR; } | REPLUS_TOK { $kind = CVC4::kind::REGEXP_PLUS; } | REOPT_TOK { $kind = CVC4::kind::REGEXP_OPT; } + | RERANGE_TOK { $kind = CVC4::kind::REGEXP_RANGE; } // NOTE: Theory operators go here ; @@ -1628,6 +1629,7 @@ REINTER_TOK : 're.itr'; RESTAR_TOK : 're.*'; REPLUS_TOK : 're.+'; REOPT_TOK : 're.opt'; +RERANGE_TOK : 're.range'; /** * A sequence of printable ASCII characters (except backslash) that starts diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index f4fbd7194..e325708c2 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -70,6 +70,7 @@ operator REGEXP_INTER 2: "regexp intersection" operator REGEXP_STAR 1 "regexp *" operator REGEXP_PLUS 1 "regexp +" operator REGEXP_OPT 1 "regexp ?" +operator REGEXP_RANGE 2 "regexp range" #constant REGEXP_EMPTY \ # ::CVC4::RegExp \ @@ -95,6 +96,7 @@ typerule REGEXP_INTER ::CVC4::theory::strings::RegExpInterTypeRule typerule REGEXP_STAR ::CVC4::theory::strings::RegExpStarTypeRule typerule REGEXP_PLUS ::CVC4::theory::strings::RegExpPlusTypeRule typerule REGEXP_OPT ::CVC4::theory::strings::RegExpOptTypeRule +typerule REGEXP_RANGE ::CVC4::theory::strings::RegExpRangeTypeRule typerule STRING_TO_REGEXP ::CVC4::theory::strings::StringToRegExpTypeRule diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 5ba67c25f..95e19c5aa 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -351,6 +351,19 @@ RewriteResponse TheoryStringsRewriter::preRewrite(TNode node) { retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_OR, NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst( ::CVC4::String("") ) ), node[0]); + } else if(node.getKind() == kind::REGEXP_RANGE) { + std::vector< Node > vec_nodes; + char c = node[0].getConst().getFirstChar(); + char end = node[1].getConst().getFirstChar(); + for(; c<=end; ++c) { + Node n = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst( ::CVC4::String( c ) ) ); + vec_nodes.push_back( n ); + } + if(vec_nodes.size() == 1) { + retNode = vec_nodes[0]; + } else { + retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_OR, vec_nodes ); + } } Trace("strings-prerewrite") << "Strings::preRewrite returning " << retNode << std::endl; diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h index 8af063284..080d6abf5 100644 --- a/src/theory/strings/theory_strings_type_rules.h +++ b/src/theory/strings/theory_strings_type_rules.h @@ -203,6 +203,40 @@ public: } }; +class RegExpRangeTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + TNode::iterator it = n.begin(); + TNode::iterator it_end = n.end(); + char ch[2]; + + for(int i=0; i<2; ++i) { + TypeNode t = (*it).getType(check); + if (!t.isString()) { + throw TypeCheckingExceptionPrivate(n, "expecting a string term in regexp range"); + } + if( (*it).getKind() != kind::CONST_STRING ) { + throw TypeCheckingExceptionPrivate(n, "expecting a constant string term in regexp range"); + } + if( (*it).getConst().size() != 1 ) { + throw TypeCheckingExceptionPrivate(n, "expecting a single constant string term in regexp range"); + } + ch[i] = (*it).getConst().getFirstChar(); + ++it; + } + if(ch[0] > ch[1]) { + throw TypeCheckingExceptionPrivate(n, "expecting the first constant is less or equal to the second one in regexp range"); + } + + if( it != it_end ) { + throw TypeCheckingExceptionPrivate(n, "too many terms in regexp range"); + } + + return nodeManager->regexpType(); + } +}; + class StringToRegExpTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) diff --git a/src/util/regexp.h b/src/util/regexp.h index 31a39e6f9..024bfd32e 100644 --- a/src/util/regexp.h +++ b/src/util/regexp.h @@ -57,6 +57,10 @@ public: } } + String(const char c) { + d_str.push_back( convertCharToUnsignedInt(c) ); + } + String(const std::vector &s) : d_str(s) { } ~String() {} @@ -151,6 +155,10 @@ public: return d_str.size(); } + char getFirstChar() const { + return convertUnsignedIntToChar( d_str[0] ); + } + String substr(unsigned i) const { std::vector ret_vec; std::vector::const_iterator itr = d_str.begin() + i; diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index ffbfb077d..cd3116eac 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -27,6 +27,7 @@ TESTS = \ str005.smt2 \ str006.smt2 \ fmf001.smt2 \ + fmf002.smt2 \ model001.smt2 \ substr001.smt2 \ regexp001.smt2 \ diff --git a/test/regress/regress0/strings/fmf002.smt2 b/test/regress/regress0/strings/fmf002.smt2 new file mode 100644 index 000000000..14f50c710 --- /dev/null +++ b/test/regress/regress0/strings/fmf002.smt2 @@ -0,0 +1,16 @@ +(set-logic QF_S) +(set-option :fmf-strings true) +(set-info :status sat) + +(declare-fun x () String) +(declare-fun y () String) +(declare-fun z () String) + +(assert (str.in.re x + (re.+ (re.range "a" "c")) + )) + +(assert (= x (str.++ y "c" z "b"))) +(assert (> (str.len z) 1)) + +(check-sat) -- cgit v1.2.3 From e9259bce584e2dd5abedbff6ecae5e27b6e6f1be Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Mon, 21 Oct 2013 09:52:37 -0500 Subject: bug fix for string special case --- src/theory/strings/theory_strings.cpp | 15 ++++++++------- src/theory/strings/theory_strings.h | 2 +- 2 files changed, 9 insertions(+), 8 deletions(-) (limited to 'src') diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 8bff4dddc..435be2ba4 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -61,7 +61,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu d_false = NodeManager::currentNM()->mkConst( false ); //option - d_regexp_unroll_depth = options::stringRegExpUnrollDepth(); + //d_regexp_unroll_depth = options::stringRegExpUnrollDepth(); //d_fmf = options::stringFMF(); } @@ -950,23 +950,24 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v //need to break - Node sk_w= NodeManager::currentNM()->mkSkolem( "w_loop_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); Node ant = mkExplain( antec, antec_new_lits ); Node str_in_re; if(index == loop_index - 1 && other_index + 2 == (int) normal_forms[other_n_index].size() && loop_index + 1 == (int) normal_forms[loop_n_index].size() && normal_forms[loop_n_index][index] == normal_forms[other_n_index][other_index + 1] && - normal_forms[loop_n_index][index].isConst() ) { + normal_forms[loop_n_index][index].isConst() && + normal_forms[loop_n_index][index].getConst().size() == 1 ) { Trace("strings-loop") << "Special case (X)=" << normal_forms[other_n_index][other_index] << " " << std::endl; Trace("strings-loop") << "... (C)=" << normal_forms[loop_n_index][index] << " " << std::endl; //special case - Node conc3 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[other_n_index][other_index], mkConcat( normal_forms[loop_n_index][index], sk_w ) ); - str_in_re = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, sk_w, + //Node conc3 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[other_n_index][other_index], mkConcat( normal_forms[loop_n_index][index], sk_w ) ); + str_in_re = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, normal_forms[other_n_index][other_index], NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, normal_forms[loop_n_index][index] ) ) ); conc = str_in_re; } else { + Node sk_w= NodeManager::currentNM()->mkSkolem( "w_loop_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); Node sk_y= NodeManager::currentNM()->mkSkolem( "y_loop_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); Node sk_z= NodeManager::currentNM()->mkSkolem( "z_loop_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); //t1 * ... * tn = y * z @@ -1812,7 +1813,7 @@ bool TheoryStrings::unrollStar( Node atom ) { Node x = atom[0]; Node r = atom[1]; int depth = d_reg_exp_unroll_depth.find( atom )==d_reg_exp_unroll_depth.end() ? 0 : d_reg_exp_unroll_depth[atom]; - if( depth <= d_regexp_unroll_depth ){ + if( depth <= options::stringRegExpUnrollDepth() ){ Trace("strings-regex") << "...unroll " << atom << " now." << std::endl; d_reg_exp_unroll[atom] = true; //add lemma? @@ -1881,7 +1882,7 @@ bool TheoryStrings::checkMemberships() { if( unrollStar( atom ) ){ addedLemma = true; }else{ - Trace("strings-regex") << "RegEx is incomplete due to " << assertion << ", depth = " << d_regexp_unroll_depth << std::endl; + Trace("strings-regex") << "RegEx is incomplete due to " << assertion << ", depth = " << options::stringRegExpUnrollDepth() << std::endl; is_unk = true; } }else{ diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 69875edf4..d5aecc633 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -127,7 +127,7 @@ class TheoryStrings : public Theory { Node d_false; Node d_zero; // RegExp depth - int d_regexp_unroll_depth; + //int d_regexp_unroll_depth; //list of pairs of nodes to merge std::map< Node, Node > d_pending_exp; std::vector< Node > d_pending; -- cgit v1.2.3 From 730e88ecb2b3ae6fdb9148c096820516c61356f3 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Mon, 21 Oct 2013 12:29:48 -0500 Subject: string fix --- src/theory/strings/theory_strings.cpp | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) (limited to 'src') diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 435be2ba4..910447589 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -548,8 +548,13 @@ void TheoryStrings::doPendingFacts() { 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] ) ); + //Assert( d_equalityEngine.hasTerm( atom[0] ) ); + //Assert( d_equalityEngine.hasTerm( atom[1] ) ); + for( unsigned j=0; j<2; j++ ){ + if( !d_equalityEngine.hasTerm( atom[j] ) ){ + d_equalityEngine.addTerm( atom[j] ); + } + } d_equalityEngine.assertEquality( atom, polarity, exp ); }else{ d_equalityEngine.assertPredicate( atom, polarity, exp ); @@ -797,7 +802,7 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v } Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, d_emptyString, normal_forms[k][index_k] ); Trace("strings-lemma") << "Strings : Infer " << eq << " from " << eq_exp << std::endl; - Assert( !d_equalityEngine.areEqual( d_emptyString, normal_forms[k][index_k] ) ); + Assert( !areEqual( d_emptyString, normal_forms[k][index_k] ) ); d_pending.push_back( eq ); d_pending_exp[eq] = eq_exp; d_infer.push_back(eq); -- cgit v1.2.3 From d676b7e044b7a92377cb3d9bb7063faefb80d7f9 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Mon, 21 Oct 2013 22:08:53 -0500 Subject: remove nested re or; opt loop --- src/theory/strings/theory_strings.cpp | 112 +++++++++++++++---------- src/theory/strings/theory_strings_rewriter.cpp | 26 ++++++ src/theory/strings/theory_strings_rewriter.h | 1 + src/util/regexp.h | 24 ++++++ 4 files changed, 121 insertions(+), 42 deletions(-) (limited to 'src') diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 910447589..4cb5e0293 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -913,24 +913,34 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v 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") << " ... T(Y.Z)= "; + std::vector< Node > vec_t; for(int lp=index; lp & v //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; - Trace("strings-loop") << "Cache: " << normal_form_src[i] << " vs " << normal_form_src[j] << std::endl; + Trace("strings-loop") << "Lemma Cache: " << normal_form_src[i] << " vs " << normal_form_src[j] << std::endl; + + if( s_zy.isConst() && r.isConst() && r != d_emptyString) { + int c; + bool flag = true; + if(s_zy.getConst().tailcmp( r.getConst(), c ) ) { + if(c >= 0) { + s_zy = NodeManager::currentNM()->mkConst( s_zy.getConst().substr(0, c + 1) ); + r = d_emptyString; + vec_r.clear(); + Trace("strings-loop") << "Refactor : S(Z.Y)= " << s_zy << ", c=" << c << std::endl; + flag = false; + } + } + if(flag) { + Trace("strings-loop") << "Loop different tail." << std::endl; + antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); + Node ant = mkExplain( antec, antec_new_lits ); + sendLemma( ant, conc, "Conflict" ); + return true; + } + } antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); //require that x is non-empty @@ -949,7 +979,7 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v //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() ); + //antec_new_lits.push_back( x_empty.negate() ); //} d_pending_req_phase[ x_empty ] = true; @@ -957,48 +987,33 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v //need to break Node ant = mkExplain( antec, antec_new_lits ); Node str_in_re; - if(index == loop_index - 1 && - other_index + 2 == (int) normal_forms[other_n_index].size() && - loop_index + 1 == (int) normal_forms[loop_n_index].size() && - normal_forms[loop_n_index][index] == normal_forms[other_n_index][other_index + 1] && - normal_forms[loop_n_index][index].isConst() && - normal_forms[loop_n_index][index].getConst().size() == 1 ) { + if( s_zy == t_yz && + r == d_emptyString && + s_zy.isConst() && + s_zy.getConst().isRepeated() + ) { + Node rep_c = NodeManager::currentNM()->mkConst( s_zy.getConst().substr(0, 1) ); Trace("strings-loop") << "Special case (X)=" << normal_forms[other_n_index][other_index] << " " << std::endl; - Trace("strings-loop") << "... (C)=" << normal_forms[loop_n_index][index] << " " << std::endl; + Trace("strings-loop") << "... (C)=" << rep_c << " " << std::endl; //special case //Node conc3 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[other_n_index][other_index], mkConcat( normal_forms[loop_n_index][index], sk_w ) ); str_in_re = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, normal_forms[other_n_index][other_index], NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, - NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, normal_forms[loop_n_index][index] ) ) ); + NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, rep_c ) ) ); conc = str_in_re; } else { + Trace("strings-loop") << "...Normal Splitting." << std::endl; Node sk_w= NodeManager::currentNM()->mkSkolem( "w_loop_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); Node sk_y= NodeManager::currentNM()->mkSkolem( "y_loop_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); Node sk_z= NodeManager::currentNM()->mkSkolem( "z_loop_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); //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, + Node conc1 = NodeManager::currentNM()->mkNode( kind::EQUAL, t_yz, 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 ) ); + // s1 * ... * sk = z * y * r + vec_r.insert(vec_r.begin(), sk_y); + vec_r.insert(vec_r.begin(), sk_z); + Node conc2 = NodeManager::currentNM()->mkNode( kind::EQUAL, s_zy, + mkConcat( vec_r ) ); Node conc3 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[other_n_index][other_index], mkConcat( sk_y, sk_w ) ); str_in_re = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, sk_w, NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, @@ -1030,9 +1045,10 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v //we will be done addNormalFormPair( normal_form_src[i], normal_form_src[j] ); //Assert( isNormalFormPair( normal_form_src[i], normal_form_src[j] ) ); + conc = NodeManager::currentNM()->mkNode( kind::OR, x_empty, conc ); sendLemma( ant, conc, "Loop" ); return true; - }else{ + } 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) { @@ -1818,8 +1834,8 @@ bool TheoryStrings::unrollStar( Node atom ) { Node x = atom[0]; Node r = atom[1]; int depth = d_reg_exp_unroll_depth.find( atom )==d_reg_exp_unroll_depth.end() ? 0 : d_reg_exp_unroll_depth[atom]; - if( depth <= options::stringRegExpUnrollDepth() ){ - Trace("strings-regex") << "...unroll " << atom << " now." << std::endl; + if( depth <= options::stringRegExpUnrollDepth() ) { + Trace("strings-regex") << "Strings::regex: Unroll " << atom << " for " << depth << " times." << std::endl; d_reg_exp_unroll[atom] = true; //add lemma? Node xeqe = x.eqNode( d_emptyString ); @@ -1853,16 +1869,27 @@ bool TheoryStrings::unrollStar( Node atom ) { Node len_x_gt_len_xp = NodeManager::currentNM()->mkNode( kind::GT, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, x ), NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_xp ) ); - - Node unr = NodeManager::currentNM()->mkNode( kind::AND, unr0, urc[0], unr2, unr3, len_x_gt_len_xp ); + + //Node len_x_eq_s_xp = NodeManager::currentNM()->mkNode( kind::EQUAL, + // NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, x ), + // NodeManager::currentNM()->mkNode( kind::PLUS, + // NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_s ), + // NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_xp ) )); + + std::vector< Node >cc; + cc.push_back(unr0); cc.push_back(urc[0]); cc.push_back(unr2); cc.push_back(unr3); cc.push_back(len_x_gt_len_xp); + //cc.push_back(len_x_eq_s_xp); + + Node unr = NodeManager::currentNM()->mkNode( kind::AND, cc ); Node lem = NodeManager::currentNM()->mkNode( kind::OR, xeqe, unr ); Node ant = atom; - if( d_reg_exp_ant.find( atom )!=d_reg_exp_ant.end() ){ + if( d_reg_exp_ant.find( atom )!=d_reg_exp_ant.end() ) { ant = d_reg_exp_ant[atom]; } sendLemma( ant, lem, "Unroll" ); return true; }else{ + Trace("strings-regex") << "Strings::regex: Stop unrolling " << atom << " the max (" << depth << ") is reached." << std::endl; return false; } } @@ -1916,6 +1943,7 @@ bool TheoryStrings::checkMemberships() { Node TheoryStrings::getNextDecisionRequest() { if(options::stringFMF() && !d_conflict) { + //Trace("strings-fmf-debug") << "Strings::FMF: Assertion Level = " << d_valuation.getAssertionLevel() << std::endl; //initialize the term we will minimize if( d_in_var_lsum.isNull() && !d_in_vars.empty() ){ Trace("strings-fmf-debug") << "Input variables: "; diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 95e19c5aa..73f17a146 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -145,6 +145,30 @@ Node TheoryStringsRewriter::prerewriteConcatRegExp( TNode node ) { return retNode; } +Node TheoryStringsRewriter::prerewriteOrRegExp(TNode node) { + Assert( node.getKind() == kind::REGEXP_OR ); + Trace("strings-prerewrite") << "Strings::prerewriteOrRegExp start " << node << std::endl; + Node retNode = node; + std::vector node_vec; + bool flag = true; + for(unsigned int i=0; imkNode(kind::REGEXP_OR, node_vec); + } + Trace("strings-prerewrite") << "Strings::prerewriteOrRegExp end " << retNode << std::endl; + return retNode; +} + bool TheoryStringsRewriter::checkConstRegExp( TNode t ) { if( t.getKind() != kind::STRING_TO_REGEXP ) { for( unsigned i = 0; imkNode( kind::REGEXP_CONCAT, node[0], NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, node[0])); diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h index e7d7eccb5..78f0da59e 100644 --- a/src/theory/strings/theory_strings_rewriter.h +++ b/src/theory/strings/theory_strings_rewriter.h @@ -35,6 +35,7 @@ public: static Node rewriteConcatString(TNode node); static Node prerewriteConcatRegExp(TNode node); + static Node prerewriteOrRegExp(TNode node); static Node rewriteMembership(TNode node); static RewriteResponse postRewrite(TNode node); diff --git a/src/util/regexp.h b/src/util/regexp.h index 024bfd32e..fef039371 100644 --- a/src/util/regexp.h +++ b/src/util/regexp.h @@ -159,6 +159,30 @@ public: return convertUnsignedIntToChar( d_str[0] ); } + bool isRepeated() const { + if(d_str.size() > 1) { + unsigned int f = d_str[0]; + for(unsigned i=1; i=0 && id_y>=0) { + if(d_str[id_x] != y.d_str[id_y]) { + c = id_x; + return false; + } + --id_x; --id_y; + } + c = id_x == -1 ? ( - id_y) : id_x; + return true; + } + String substr(unsigned i) const { std::vector ret_vec; std::vector::const_iterator itr = d_str.begin() + i; -- cgit v1.2.3 From 0330a9454d69d1972fea521de9ad95f2a792627c Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Tue, 22 Oct 2013 21:36:12 -0500 Subject: bug fixes: some issues remain, need more discussion later --- src/theory/strings/theory_strings.cpp | 271 ++++++++++++++++++---------------- src/theory/strings/theory_strings.h | 5 + 2 files changed, 152 insertions(+), 124 deletions(-) (limited to 'src') diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 4cb5e0293..306332f5b 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -110,7 +110,7 @@ Node TheoryStrings::getLengthTerm( Node t ) { } Node TheoryStrings::getLength( Node t ) { - return NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, getLengthTerm( t ) ); + return Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, getLengthTerm( t ) ) ); } void TheoryStrings::setMasterEqualityEngine(eq::EqualityEngine* eq) { @@ -581,12 +581,13 @@ void TheoryStrings::doPendingLemmas() { bool 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) { + Trace("strings-process-debug") << "Get normal forms " << eqc << std::endl; // EqcItr eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); while( !eqc_i.isFinished() ) { Node n = (*eqc_i); - Trace("strings-process-debug") << "Get Normal Form : Process term " << n << std::endl; 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 nf_n; std::vector nf_exp_n; bool result = true; @@ -607,6 +608,13 @@ bool TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std //successfully computed normal form if( nf.size()!=1 || nf[0]!=d_emptyString ) { for( unsigned r=0; r & visited, std bool 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 & v Node length_term_j = getLength( normal_forms[j][index_j] ); //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 ) { - //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 ); - if( !areEqual(length_term_i, length_term_j) ) { - Trace("strings-solve-debug") << "Case 2.1 : string lengths neither equal nor disequal" << std::endl; - //try to make the lengths equal via splitting on demand - sendSplit( length_term_i, length_term_j, "Length" ); - length_eq = Rewriter::rewrite( length_eq ); - d_pending_req_phase[ length_eq ] = true; - return true; - }else{ - Trace("strings-solve-debug") << "Case 2.2 : string lengths are explicitly equal" << std::endl; - //lengths are already equal, do unification - 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(length_eq); - 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_pending.push_back( eq ); - d_pending_exp[eq] = eq_exp; - d_infer.push_back(eq); - d_infer_exp.push_back(eq_exp); - return true; - } - }else if( ( normal_forms[i][index_i].getKind()!=kind::CONST_STRING && index_i==normal_forms[i].size()-1 ) || + Trace("strings-solve-debug") << "Case 2.1 : string lengths neither equal nor disequal" << std::endl; + //try to make the lengths equal via splitting on demand + sendSplit( length_term_i, length_term_j, "Length" ); + length_eq = Rewriter::rewrite( length_eq ); + d_pending_req_phase[ length_eq ] = true; + return true; + } else if( areEqual(length_term_i, length_term_j) ) { + Trace("strings-solve-debug") << "Case 2.2 : string lengths are equal" << std::endl; + Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[i][index_i], normal_forms[j][index_j] ); + Node length_eq = NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j ); + std::vector< Node > temp_exp; + temp_exp.insert(temp_exp.end(), curr_exp.begin(), curr_exp.end() ); + temp_exp.push_back(length_eq); + 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_pending.push_back( eq ); + d_pending_exp[eq] = eq_exp; + d_infer.push_back(eq); + d_infer_exp.push_back(eq_exp); + 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 ) ){ Trace("strings-solve-debug") << "Case 3 : at endpoint" << std::endl; Node conc; @@ -972,82 +967,91 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v } } + //Node loop_eq = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::EQUAL, + // NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[other_n_index][other_index], s_zy ), + // NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, t_yz, normal_forms[other_n_index][other_index], r ) ) ); + 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 ); + //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; - - - //need to break - Node ant = mkExplain( antec, antec_new_lits ); - Node str_in_re; - if( s_zy == t_yz && - r == d_emptyString && - s_zy.isConst() && - s_zy.getConst().isRepeated() - ) { - Node rep_c = NodeManager::currentNM()->mkConst( s_zy.getConst().substr(0, 1) ); - Trace("strings-loop") << "Special case (X)=" << normal_forms[other_n_index][other_index] << " " << std::endl; - Trace("strings-loop") << "... (C)=" << rep_c << " " << std::endl; - //special case - //Node conc3 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[other_n_index][other_index], mkConcat( normal_forms[loop_n_index][index], sk_w ) ); - str_in_re = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, normal_forms[other_n_index][other_index], - NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, - NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, rep_c ) ) ); - conc = str_in_re; - } else { - Trace("strings-loop") << "...Normal Splitting." << std::endl; - Node sk_w= NodeManager::currentNM()->mkSkolem( "w_loop_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); - Node sk_y= NodeManager::currentNM()->mkSkolem( "y_loop_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); - Node sk_z= NodeManager::currentNM()->mkSkolem( "z_loop_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); - //t1 * ... * tn = y * z - Node conc1 = NodeManager::currentNM()->mkNode( kind::EQUAL, t_yz, - NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk_y, sk_z ) ); - // s1 * ... * sk = z * y * r - vec_r.insert(vec_r.begin(), sk_y); - vec_r.insert(vec_r.begin(), sk_z); - Node conc2 = NodeManager::currentNM()->mkNode( kind::EQUAL, s_zy, - mkConcat( vec_r ) ); - Node conc3 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[other_n_index][other_index], mkConcat( sk_y, sk_w ) ); - str_in_re = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, sk_w, - NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, - NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, mkConcat( sk_z, sk_y ) ) ) ); - - //Node sk_y_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_y ); - //Node sk_z_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_z ); - //Node len_z_gt_zero = NodeManager::currentNM()->mkNode( kind::GT, sk_z_len, d_zero ); - //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, sk_z.eqNode(d_emptyString), sk_y.eqNode(d_emptyString)); - - //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 ); - conc = NodeManager::currentNM()->mkNode( kind::AND, conc1, conc2, conc3, str_in_re );//, 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 ); - } // normal case - - //set its antecedant to ant, to say when it is relevant - d_reg_exp_ant[str_in_re] = ant; - //unroll the str in re constraint once - unrollStar( str_in_re ); - - //we will be done - addNormalFormPair( normal_form_src[i], normal_form_src[j] ); - //Assert( isNormalFormPair( normal_form_src[i], normal_form_src[j] ) ); - conc = NodeManager::currentNM()->mkNode( kind::OR, x_empty, conc ); - sendLemma( ant, conc, "Loop" ); - return true; + //d_pending_req_phase[ x_empty ] = true; + if( !areDisequal( normal_forms[loop_n_index][loop_index], d_emptyString ) ){ + //try to make normal_forms[loop_n_index][loop_index] equal to empty to avoid loop + sendSplit( normal_forms[loop_n_index][loop_index], d_emptyString, "Loop Empty" ); + return true; + }else{ + //need to break + Node ant = mkExplain( antec, antec_new_lits ); + Node str_in_re; + if( s_zy == t_yz && + r == d_emptyString && + s_zy.isConst() && + s_zy.getConst().isRepeated() + ) { + Node rep_c = NodeManager::currentNM()->mkConst( s_zy.getConst().substr(0, 1) ); + Trace("strings-loop") << "Special case (X)=" << normal_forms[other_n_index][other_index] << " " << std::endl; + Trace("strings-loop") << "... (C)=" << rep_c << " " << std::endl; + //special case + //conc = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[other_n_index][other_index], mkConcat( rep_c, sk_w ) ); + str_in_re = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, normal_forms[other_n_index][other_index], + NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, + NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, rep_c ) ) ); + //conc = NodeManager::currentNM()->mkNode( kind::AND, conc, str_in_re ); + conc = str_in_re; + } else { + Trace("strings-loop") << "Strings::loop: ...Normal Splitting." << std::endl; + Node sk_w= NodeManager::currentNM()->mkSkolem( "w_loop_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); + Node sk_y= NodeManager::currentNM()->mkSkolem( "y_loop_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); + Node sk_z= NodeManager::currentNM()->mkSkolem( "z_loop_$$", normal_forms[i][index_i].getType(), "created for loop detection split" ); + //t1 * ... * tn = y * z + Node conc1 = NodeManager::currentNM()->mkNode( kind::EQUAL, t_yz, + NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk_y, sk_z ) ); + // s1 * ... * sk = z * y * r + vec_r.insert(vec_r.begin(), sk_y); + vec_r.insert(vec_r.begin(), sk_z); + Node conc2 = NodeManager::currentNM()->mkNode( kind::EQUAL, s_zy, + mkConcat( vec_r ) ); + Node conc3 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[other_n_index][other_index], mkConcat( sk_y, sk_w ) ); + str_in_re = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, sk_w, + NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, + NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, mkConcat( sk_z, sk_y ) ) ) ); + + //Node sk_y_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_y ); + //Node sk_z_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_z ); + //Node len_z_gt_zero = NodeManager::currentNM()->mkNode( kind::GT, sk_z_len, d_zero ); + //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, sk_z.eqNode(d_emptyString), sk_y.eqNode(d_emptyString)); + + //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 ); + conc = NodeManager::currentNM()->mkNode( kind::AND, conc1, conc2, conc3, str_in_re );//, 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 ); + } // normal case + + //set its antecedant to ant, to say when it is relevant + d_reg_exp_ant[str_in_re] = ant; + //unroll the str in re constraint once + unrollStar( str_in_re ); + //conc = NodeManager::currentNM()->mkNode( kind::OR, x_empty, conc ); + sendLemma( ant, conc, "Loop" ); + + //we will be done + addNormalFormPair( normal_form_src[i], normal_form_src[j] ); + //Assert( isNormalFormPair( normal_form_src[i], normal_form_src[j] ) ); + return true; + } } else { Trace("strings-solve-debug") << "No loops detected." << std::endl; if( normal_forms[i][index_i].getKind() == kind::CONST_STRING || @@ -1136,7 +1140,7 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v //construct the normal form if( normal_forms.empty() ){ Trace("strings-solve-debug2") << "construct the normal form" << std::endl; - nf.push_back( eqc ); + getConcatVec( eqc, nf ); } else { Trace("strings-solve-debug2") << "just take the first normal form" << std::endl; //just take the first normal form @@ -1401,6 +1405,18 @@ Node TheoryStrings::mkExplain( std::vector< Node >& a, std::vector< Node >& an ) return ant; } +void TheoryStrings::getConcatVec( Node n, std::vector< Node >& c ) { + if( n.getKind()==kind::STRING_CONCAT ){ + for( unsigned i=0; imkSkolem( "s_unroll_$$", x.getType(), "created for unrolling" ); Node sk_xp= NodeManager::currentNM()->mkSkolem( "x_unroll_$$", x.getType(), "created for unrolling" ); - Node unr0 = sk_s.eqNode( d_emptyString ).negate(); - // must also call preprocessing on unr1 - Node unr1 = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, sk_s, r[0] ); - - std::vector< Node > urc; - urc.push_back( unr1 ); + std::vector< Node >cc; - StringsPreprocess spp; - spp.simplify( urc ); - for( unsigned i=1; imkNode( kind::STRING_IN_REGEXP, sk_s, r[0] ) ); + if(unr1.getKind() == kind::EQUAL) { + sk_s = unr1[0] == sk_s ? unr1[1] : unr1[2]; + Node unr0 = sk_s.eqNode( d_emptyString ).negate(); + cc.push_back(unr0); + } else { + std::vector< Node > urc; + urc.push_back( unr1 ); + + StringsPreprocess spp; + spp.simplify( urc ); + for( unsigned i=1; imkNode( kind::STRING_LENGTH, sk_s ), // NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk_xp ) )); - std::vector< Node >cc; - cc.push_back(unr0); cc.push_back(urc[0]); cc.push_back(unr2); cc.push_back(unr3); cc.push_back(len_x_gt_len_xp); + cc.push_back(unr2); cc.push_back(unr3); cc.push_back(len_x_gt_len_xp); //cc.push_back(len_x_eq_s_xp); Node unr = NodeManager::currentNM()->mkNode( kind::AND, cc ); diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index d5aecc633..8f21888a2 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -146,6 +146,9 @@ class TheoryStrings : public Theory { bool isNormalFormPair( Node n1, Node n2 ); bool isNormalFormPair2( Node n1, Node n2 ); + //loop + //std::map< Node, bool > d_loop_processed; + //regular expression memberships NodeList d_reg_exp_mem; std::map< Node, bool > d_reg_exp_unroll; @@ -237,6 +240,8 @@ protected: /** mkExplain **/ Node mkExplain( std::vector< Node >& a ); Node mkExplain( std::vector< Node >& a, std::vector< Node >& an ); + /** get concat vector */ + void getConcatVec( Node n, std::vector< Node >& c ); //get equivalence classes void getEquivalenceClasses( std::vector< Node >& eqcs ); -- cgit v1.2.3 From 152e3546328f5aa327fe54463f2214497596422b Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Wed, 23 Oct 2013 10:35:42 -0500 Subject: bug fix --- src/theory/strings/theory_strings.cpp | 69 ++++++++++++++++++++--------------- src/util/regexp.h | 2 +- 2 files changed, 41 insertions(+), 30 deletions(-) (limited to 'src') diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 306332f5b..11024e351 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -165,10 +165,16 @@ void TheoryStrings::explain(TNode literal, std::vector& assumptions){ bool polarity = literal.getKind() != kind::NOT; TNode atom = polarity ? literal : literal[0]; unsigned ps = assumptions.size(); + std::vector< TNode > tassumptions; if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) { - d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions); + d_equalityEngine.explainEquality(atom[0], atom[1], polarity, tassumptions); } else { - d_equalityEngine.explainPredicate(atom, polarity, assumptions); + d_equalityEngine.explainPredicate(atom, polarity, tassumptions); + } + for( unsigned i=0; i & v bool flag = true; if(s_zy.getConst().tailcmp( r.getConst(), c ) ) { if(c >= 0) { - s_zy = NodeManager::currentNM()->mkConst( s_zy.getConst().substr(0, c + 1) ); + s_zy = NodeManager::currentNM()->mkConst( s_zy.getConst().substr(0, c) ); r = d_emptyString; vec_r.clear(); Trace("strings-loop") << "Refactor : S(Z.Y)= " << s_zy << ", c=" << c << std::endl; @@ -1091,9 +1097,10 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v //split the string Node sk = NodeManager::currentNM()->mkSkolem( "c_split_$$", normal_forms[i][index_i].getType(), "created for v/c split" ); - Node eq1 = NodeManager::currentNM()->mkNode( kind::EQUAL, other_str, d_emptyString ); - Node eq2 = NodeManager::currentNM()->mkNode( kind::EQUAL, other_str, - NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, firstChar, sk ) ); + Node eq1 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::EQUAL, other_str, d_emptyString ) ); + Node eq2 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::EQUAL, other_str, + NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, firstChar, sk ) ) ); + d_pending_req_phase[ eq1 ] = true; conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 ); Trace("strings-solve-debug") << "Break normal form constant/variable " << std::endl; @@ -1364,34 +1371,38 @@ Node TheoryStrings::mkExplain( std::vector< Node >& a ) { Node TheoryStrings::mkExplain( std::vector< Node >& a, std::vector< Node >& an ) { std::vector< TNode > antec_exp; for( unsigned i=0; i Date: Wed, 23 Oct 2013 11:45:34 -0500 Subject: bug fix for loop rule --- src/theory/strings/theory_strings.cpp | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) (limited to 'src') diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 11024e351..7c3e7ebbc 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -991,8 +991,15 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v //try to make normal_forms[loop_n_index][loop_index] equal to empty to avoid loop sendSplit( normal_forms[loop_n_index][loop_index], d_emptyString, "Loop Empty" ); return true; - }else{ + } else if( !areDisequal( t_yz, d_emptyString ) ) { + //TODO........... + //try to make normal_forms[loop_n_index][loop_index] equal to empty to avoid loop + sendSplit( t_yz, d_emptyString, "Loop Empty" ); + return true; + } else { //need to break + antec.push_back( normal_forms[loop_n_index][loop_index].eqNode( d_emptyString ).negate() ); + antec.push_back( t_yz.eqNode( d_emptyString ).negate() ); Node ant = mkExplain( antec, antec_new_lits ); Node str_in_re; if( s_zy == t_yz && -- cgit v1.2.3 From 496c5489a5073ef1aa9306e165ac4dc4aaeb69a9 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Wed, 23 Oct 2013 13:52:24 -0500 Subject: add back eager approach --- src/theory/strings/theory_strings.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src') diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 7c3e7ebbc..a50c295da 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -1451,7 +1451,7 @@ bool TheoryStrings::checkLengths() { //if n is concat, and //if n has not instantiatied the concat..length axiom //then, add lemma - if( n.getKind() == kind::CONST_STRING ) { // || n.getKind() == kind::STRING_CONCAT ){ + if( n.getKind() == kind::CONST_STRING || n.getKind() == kind::STRING_CONCAT ) { // || n.getKind() == kind::STRING_CONCAT ){ if( d_length_inst.find(n)==d_length_inst.end() ){ d_length_inst[n] = true; Trace("strings-debug") << "get n: " << n << endl; -- cgit v1.2.3 From 0274d973ae504fa74fd73aa80c725a778581bb26 Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Thu, 24 Oct 2013 16:48:30 -0700 Subject: Fix for bug515 --- src/theory/model.cpp | 92 +++++++++++++++++-------------- src/theory/model.h | 5 +- src/theory/uf/theory_uf_strong_solver.cpp | 2 +- test/regress/regress0/fmf/Makefile.am | 3 +- test/regress/regress0/fmf/array_card.smt2 | 18 ++++++ 5 files changed, 75 insertions(+), 45 deletions(-) create mode 100644 test/regress/regress0/fmf/array_card.smt2 (limited to 'src') diff --git a/src/theory/model.cpp b/src/theory/model.cpp index 840c8bc3a..393f3883c 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -28,17 +28,22 @@ using namespace CVC4::context; using namespace CVC4::theory; TheoryModel::TheoryModel( context::Context* c, std::string name, bool enableFuncModels) : - d_substitutions(c, false), d_equalityEngine(c, name), d_modelBuilt(c, false), d_enableFuncModels(enableFuncModels) + d_substitutions(c, false), d_modelBuilt(c, false), d_enableFuncModels(enableFuncModels) { d_true = NodeManager::currentNM()->mkConst( true ); d_false = NodeManager::currentNM()->mkConst( false ); + + d_eeContext = new context::Context(); + d_equalityEngine = new eq::EqualityEngine(d_eeContext, name); + // The kinds we are treating as function application in congruence - d_equalityEngine.addFunctionKind(kind::APPLY_UF); - d_equalityEngine.addFunctionKind(kind::SELECT); - // d_equalityEngine.addFunctionKind(kind::STORE); - d_equalityEngine.addFunctionKind(kind::APPLY_CONSTRUCTOR); - d_equalityEngine.addFunctionKind(kind::APPLY_SELECTOR); - d_equalityEngine.addFunctionKind(kind::APPLY_TESTER); + d_equalityEngine->addFunctionKind(kind::APPLY_UF); + d_equalityEngine->addFunctionKind(kind::SELECT); + // d_equalityEngine->addFunctionKind(kind::STORE); + d_equalityEngine->addFunctionKind(kind::APPLY_CONSTRUCTOR); + d_equalityEngine->addFunctionKind(kind::APPLY_SELECTOR); + d_equalityEngine->addFunctionKind(kind::APPLY_TESTER); + d_eeContext->push(); } void TheoryModel::reset(){ @@ -46,6 +51,8 @@ void TheoryModel::reset(){ d_rep_set.clear(); d_uf_terms.clear(); d_uf_models.clear(); + d_eeContext->pop(); + d_eeContext->push(); } Node TheoryModel::getValue(TNode n) const { @@ -98,7 +105,7 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const // no good. Instead, return the quantifier itself. If we're in // checkModel(), and the quantifier actually matters, we'll get an // assert-fail since the quantifier isn't a constant. - if(!d_equalityEngine.hasTerm(Rewriter::rewrite(n))) { + if(!d_equalityEngine->hasTerm(Rewriter::rewrite(n))) { return n; } else { n = Rewriter::rewrite(n); @@ -158,13 +165,13 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const return val; } - if (!d_equalityEngine.hasTerm(n)) { + if (!d_equalityEngine->hasTerm(n)) { // Unknown term - return first enumerated value for this type TypeEnumerator te(n.getType()); return *te; } } - Node val = d_equalityEngine.getRepresentative(n); + Node val = d_equalityEngine->getRepresentative(n); Assert(d_reps.find(val) != d_reps.end()); std::map< Node, Node >::const_iterator it = d_reps.find( val ); if( it!=d_reps.end() ){ @@ -237,7 +244,7 @@ void TheoryModel::addSubstitution( TNode x, TNode t, bool invalidateCache ){ /** add term */ void TheoryModel::addTerm(TNode n ){ - Assert(d_equalityEngine.hasTerm(n)); + Assert(d_equalityEngine->hasTerm(n)); //must collect UF terms if (n.getKind()==APPLY_UF) { Node op = n.getOperator(); @@ -254,8 +261,8 @@ void TheoryModel::assertEquality(TNode a, TNode b, bool polarity ){ return; } Trace("model-builder-assertions") << "(assert " << (polarity ? "(= " : "(not (= ") << a << " " << b << (polarity ? "));" : ")));") << endl; - d_equalityEngine.assertEquality( a.eqNode(b), polarity, Node::null() ); - Assert(d_equalityEngine.consistent()); + d_equalityEngine->assertEquality( a.eqNode(b), polarity, Node::null() ); + Assert(d_equalityEngine->consistent()); } /** assert predicate */ @@ -266,11 +273,11 @@ void TheoryModel::assertPredicate(TNode a, bool polarity ){ } if (a.getKind() == EQUAL) { Trace("model-builder-assertions") << "(assert " << (polarity ? " " : "(not ") << a << (polarity ? ");" : "));") << endl; - d_equalityEngine.assertEquality( a, polarity, Node::null() ); + d_equalityEngine->assertEquality( a, polarity, Node::null() ); } else { Trace("model-builder-assertions") << "(assert " << (polarity ? "" : "(not ") << a << (polarity ? ");" : "));") << endl; - d_equalityEngine.assertPredicate( a, polarity, Node::null() ); - Assert(d_equalityEngine.consistent()); + d_equalityEngine->assertPredicate( a, polarity, Node::null() ); + Assert(d_equalityEngine->consistent()); } } @@ -309,8 +316,8 @@ void TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee, set* } else { Trace("model-builder-assertions") << "(assert (= " << *eqc_i << " " << rep << "));" << endl; - d_equalityEngine.mergePredicates(*eqc_i, rep, Node::null()); - Assert(d_equalityEngine.consistent()); + d_equalityEngine->mergePredicates(*eqc_i, rep, Node::null()); + Assert(d_equalityEngine->consistent()); } } } else { @@ -334,13 +341,13 @@ void TheoryModel::assertRepresentative(TNode n ) bool TheoryModel::hasTerm(TNode a) { - return d_equalityEngine.hasTerm( a ); + return d_equalityEngine->hasTerm( a ); } Node TheoryModel::getRepresentative(TNode a) { - if( d_equalityEngine.hasTerm( a ) ){ - Node r = d_equalityEngine.getRepresentative( a ); + if( d_equalityEngine->hasTerm( a ) ){ + Node r = d_equalityEngine->getRepresentative( a ); if( d_reps.find( r )!=d_reps.end() ){ return d_reps[ r ]; }else{ @@ -355,8 +362,8 @@ bool TheoryModel::areEqual(TNode a, TNode b) { if( a==b ){ return true; - }else if( d_equalityEngine.hasTerm( a ) && d_equalityEngine.hasTerm( b ) ){ - return d_equalityEngine.areEqual( a, b ); + }else if( d_equalityEngine->hasTerm( a ) && d_equalityEngine->hasTerm( b ) ){ + return d_equalityEngine->areEqual( a, b ); }else{ return false; } @@ -364,8 +371,8 @@ bool TheoryModel::areEqual(TNode a, TNode b) bool TheoryModel::areDisequal(TNode a, TNode b) { - if( d_equalityEngine.hasTerm( a ) && d_equalityEngine.hasTerm( b ) ){ - return d_equalityEngine.areDisequal( a, b, false ); + if( d_equalityEngine->hasTerm( a ) && d_equalityEngine->hasTerm( b ) ){ + return d_equalityEngine->areDisequal( a, b, false ); }else{ return false; } @@ -422,7 +429,7 @@ void TheoryEngineModelBuilder::checkTerms(TNode n, TheoryModel* tm, NodeSet& cac return; } if (isAssignable(n)) { - tm->d_equalityEngine.addTerm(n); + tm->d_equalityEngine->addTerm(n); } for(TNode::iterator child_it = n.begin(); child_it != n.end(); ++child_it) { checkTerms(*child_it, tm, cache); @@ -448,11 +455,11 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) d_te->collectModelInfo(tm, fullModel); // Loop through all terms and make sure that assignable sub-terms are in the equality engine - eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &tm->d_equalityEngine ); + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( tm->d_equalityEngine ); { NodeSet cache; for ( ; !eqcs_i.isFinished(); ++eqcs_i) { - eq::EqClassIterator eqc_i = eq::EqClassIterator((*eqcs_i), &tm->d_equalityEngine); + eq::EqClassIterator eqc_i = eq::EqClassIterator((*eqcs_i),tm->d_equalityEngine); for ( ; !eqc_i.isFinished(); ++eqc_i) { checkTerms(*eqc_i, tm, cache); } @@ -465,20 +472,20 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) std::map< Node, Node > assertedReps, constantReps; TypeSet typeConstSet, typeRepSet, typeNoRepSet; std::set< TypeNode > allTypes; - eqcs_i = eq::EqClassesIterator(&tm->d_equalityEngine); + eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine); for ( ; !eqcs_i.isFinished(); ++eqcs_i) { // eqc is the equivalence class representative Node eqc = (*eqcs_i); Trace("model-builder") << "Processing EC: " << eqc << endl; - Assert(tm->d_equalityEngine.getRepresentative(eqc) == eqc); + Assert(tm->d_equalityEngine->getRepresentative(eqc) == eqc); TypeNode eqct = eqc.getType(); Assert(assertedReps.find(eqc) == assertedReps.end()); Assert(constantReps.find(eqc) == constantReps.end()); // Loop through terms in this EC Node rep, const_rep; - eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, &tm->d_equalityEngine); + eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, tm->d_equalityEngine); for ( ; !eqc_i.isFinished(); ++eqc_i) { Node n = *eqc_i; Trace("model-builder") << " Processing Term: " << n << endl; @@ -556,7 +563,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) assignable = false; evaluable = false; evaluated = false; - eq::EqClassIterator eqc_i = eq::EqClassIterator(*i2, &tm->d_equalityEngine); + eq::EqClassIterator eqc_i = eq::EqClassIterator(*i2, tm->d_equalityEngine); for ( ; !eqc_i.isFinished(); ++eqc_i) { Node n = *eqc_i; if (isAssignable(n)) { @@ -653,7 +660,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) for (i = noRepSet.begin(); i != noRepSet.end(); ) { i2 = i; ++i; - eq::EqClassIterator eqc_i = eq::EqClassIterator(*i2, &tm->d_equalityEngine); + eq::EqClassIterator eqc_i = eq::EqClassIterator(*i2, tm->d_equalityEngine); assignable = false; evaluable = false; for ( ; !eqc_i.isFinished(); ++eqc_i) { @@ -744,7 +751,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) #ifdef CVC4_ASSERTIONS if (fullModel) { // Check that every term evaluates to its representative in the model - for (eqcs_i = eq::EqClassesIterator(&tm->d_equalityEngine); !eqcs_i.isFinished(); ++eqcs_i) { + for (eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine); !eqcs_i.isFinished(); ++eqcs_i) { // eqc is the equivalence class representative Node eqc = (*eqcs_i); Node rep; @@ -757,7 +764,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) Assert(itMap != constantReps.end()); rep = itMap->second; } - eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, &tm->d_equalityEngine); + eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, tm->d_equalityEngine); for ( ; !eqc_i.isFinished(); ++eqc_i) { Node n = *eqc_i; static int repCheckInstance = 0; @@ -795,18 +802,19 @@ Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, std::map< Node bool childrenConst = true; for (size_t i=0; i < r.getNumChildren(); ++i) { Node ri = r[i]; + bool recurse = true; if (!ri.isConst()) { - if (m->d_equalityEngine.hasTerm(ri)) { - ri = m->d_equalityEngine.getRepresentative(ri); - itMap = constantReps.find(ri); + if (m->d_equalityEngine->hasTerm(ri)) { + itMap = constantReps.find(m->d_equalityEngine->getRepresentative(ri)); if (itMap != constantReps.end()) { ri = (*itMap).second; + recurse = false; } - else if (evalOnly) { - ri = normalize(m, r[i], constantReps, evalOnly); - } + else if (!evalOnly) { + recurse = false; + } } - else { + if (recurse) { ri = normalize(m, ri, constantReps, evalOnly); } if (!ri.isConst()) { diff --git a/src/theory/model.h b/src/theory/model.h index 03a641df4..a18d66ab0 100644 --- a/src/theory/model.h +++ b/src/theory/model.h @@ -42,8 +42,11 @@ protected: public: TheoryModel(context::Context* c, std::string name, bool enableFuncModels); virtual ~TheoryModel(){} + + /** special local context for our equalityEngine so we can clear it independently of search context */ + context::Context* d_eeContext; /** equality engine containing all known equalities/disequalities */ - eq::EqualityEngine d_equalityEngine; + eq::EqualityEngine* d_equalityEngine; /** map of representatives of equality engine to used representatives in representative set */ std::map< Node, Node > d_reps; /** stores set of representatives for each type */ diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index 8c85e4dd2..8aa7d625d 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -1382,7 +1382,7 @@ void StrongSolverTheoryUF::SortModel::debugPrint( const char* c ){ void StrongSolverTheoryUF::SortModel::debugModel( TheoryModel* m ){ if( Trace.isOn("uf-ss-warn") ){ std::vector< Node > eqcs; - eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &m->d_equalityEngine ); + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( m->d_equalityEngine ); while( !eqcs_i.isFinished() ){ Node eqc = (*eqcs_i); if( eqc.getType()==d_type ){ diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index 601d65799..bfbc851ef 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -19,6 +19,7 @@ MAKEFLAGS = -k # If a test shouldn't be run in e.g. competition mode, # put it below in "TESTS +=" TESTS = \ + array_card.smt2 \ agree466.smt2 \ ALG008-1.smt2 \ german169.smt2 \ @@ -29,7 +30,7 @@ TESTS = \ german73.smt2 \ PUZ001+1.smt2 \ refcount24.cvc.smt2 \ - bug0909.smt2 + bug0909.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/fmf/array_card.smt2 b/test/regress/regress0/fmf/array_card.smt2 new file mode 100644 index 000000000..9ee00d13a --- /dev/null +++ b/test/regress/regress0/fmf/array_card.smt2 @@ -0,0 +1,18 @@ +; COMMAND-LINE: --finite-model-find +; EXPECT: sat +; EXIT: 10 +(set-logic AUFLIA) +(set-option :produce-models true) +(declare-sort U 0) +(declare-fun f () (Array U U)) +(declare-fun a () U) +(declare-fun b () U) +(declare-fun c () U) + +(assert (distinct a b c)) + +(assert (distinct (select f a) (select f b))) + +(assert (forall ((x U)) (or (= (select f x) c) (= (select f x) b)))) + +(check-sat) -- cgit v1.2.3 From 384952474a1b5e93dd3f08d2fba6a2580c7468e9 Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Mon, 28 Oct 2013 14:36:56 -0700 Subject: Turn off model-based arrays (causing crashes in portfolio) --- src/smt/smt_engine.cpp | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) (limited to 'src') diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index be6acd09c..0b233e7b6 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -881,16 +881,16 @@ void SmtEngine::setLogicInternal() throw() { } } // Turn on model-based arrays for QF_AX (unless models are enabled) - if(! options::arraysModelBased.wasSetByUser()) { - if (not d_logic.isQuantified() && - d_logic.isTheoryEnabled(THEORY_ARRAY) && - d_logic.isPure(THEORY_ARRAY) && - !options::produceModels() && - !options::checkModels()) { - Trace("smt") << "turning on model-based array solver" << endl; - options::arraysModelBased.set(true); - } - } + // if(! options::arraysModelBased.wasSetByUser()) { + // if (not d_logic.isQuantified() && + // d_logic.isTheoryEnabled(THEORY_ARRAY) && + // d_logic.isPure(THEORY_ARRAY) && + // !options::produceModels() && + // !options::checkModels()) { + // Trace("smt") << "turning on model-based array solver" << endl; + // options::arraysModelBased.set(true); + // } + // } // Turn on multiple-pass non-clausal simplification for QF_AUFBV if(! options::repeatSimp.wasSetByUser()) { bool repeatSimp = !d_logic.isQuantified() && -- cgit v1.2.3