diff options
-rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 277 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.h | 13 | ||||
-rw-r--r-- | src/theory/quantifiers/bounded_integers.h | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_match_generator.cpp | 7 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiation_engine.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/model_engine.cpp | 104 | ||||
-rw-r--r-- | src/theory/quantifiers/model_engine.h | 2 | ||||
-rwxr-xr-x | src/theory/quantifiers/quant_conflict_find.h | 8 | ||||
-rw-r--r-- | src/theory/quantifiers/rewrite_engine.cpp | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/rewrite_engine.h | 4 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 14 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.h | 10 |
12 files changed, 309 insertions, 136 deletions
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index eef25ca80..2715f8e75 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -49,6 +49,7 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, d_equalityEngine(d_notify, c, "theory::datatypes::TheoryDatatypes"), d_labels( c ), d_selector_apps( c ), + d_consEqc( c ), d_conflict( c, false ), d_collectTermsCache( c ), d_consTerms( c ), @@ -59,6 +60,8 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, d_equalityEngine.addFunctionKind(kind::APPLY_SELECTOR_TOTAL); d_equalityEngine.addFunctionKind(kind::APPLY_TESTER); d_equalityEngine.addFunctionKind(kind::APPLY_UF); + + d_true = NodeManager::currentNM()->mkConst( true ); } TheoryDatatypes::~TheoryDatatypes() { @@ -99,6 +102,15 @@ TheoryDatatypes::EqcInfo* TheoryDatatypes::getOrMakeEqcInfo( Node n, bool doMake } } +TNode TheoryDatatypes::getEqcConstructor( TNode r ) { + EqcInfo * ei = getOrMakeEqcInfo( r, false ); + if( ei && !ei->d_constructor.get().isNull() ){ + return ei->d_constructor.get(); + }else{ + return r; + } +} + void TheoryDatatypes::check(Effort e) { Trace("datatypes-debug") << "Check effort " << e << std::endl; while(!done() && !d_conflict) { @@ -189,7 +201,7 @@ void TheoryDatatypes::check(Effort e) { if( dt.getNumConstructors()==1 ){ Node t = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[0].getTester() ), n ); d_pending.push_back( t ); - d_pending_exp[ t ] = NodeManager::currentNM()->mkConst( true ); + d_pending_exp[ t ] = d_true; Trace("datatypes-infer") << "DtInfer : 1-cons : " << t << std::endl; d_infer.push_back( t ); }else{ @@ -252,7 +264,7 @@ void TheoryDatatypes::flushPendingFacts(){ if( mustCommunicateFact( fact, exp ) ){ Trace("dt-lemma-debug") << "Assert fact " << fact << " " << exp << std::endl; Node lem = fact; - if( exp.isNull() || exp==NodeManager::currentNM()->mkConst( true ) ){ + if( exp.isNull() || exp==d_true ){ lem = fact; }else{ Trace("dt-lemma-debug") << "Get explanation..." << std::endl; @@ -345,7 +357,7 @@ Node TheoryDatatypes::expandDefinition(LogicRequest &logicRequest, Node n) { Node tst = NodeManager::currentNM()->mkNode( kind::APPLY_TESTER, Node::fromExpr( tester ), n[0] ); tst = Rewriter::rewrite( tst ); Node n_ret; - if( tst==NodeManager::currentNM()->mkConst( true ) ){ + if( tst==d_true ){ n_ret = sel; }else{ if( d_exp_def_skolem.find( selector )==d_exp_def_skolem.end() ){ @@ -424,7 +436,7 @@ Node TheoryDatatypes::ppRewrite(TNode in) { if( DatatypesRewriter::checkClash(in[0], in[1], rew) ){ nn = NodeManager::currentNM()->mkConst(false); }else{ - nn = rew.size()==0 ? NodeManager::currentNM()->mkConst( true ) : + nn = rew.size()==0 ? d_true : ( rew.size()==1 ? rew[0] : NodeManager::currentNM()->mkNode( kind::AND, rew ) ); } return nn; @@ -562,6 +574,14 @@ Node TheoryDatatypes::explain( TNode literal ){ return mkAnd( assumptions ); } +Node TheoryDatatypes::explain( std::vector< Node >& lits ) { + std::vector< TNode > assumptions; + for( unsigned i=0; i<lits.size(); i++ ){ + explain( lits[i], assumptions ); + } + return mkAnd( assumptions ); +} + /** Conflict when merging two constants */ void TheoryDatatypes::conflict(TNode a, TNode b){ if (a.getKind() == kind::CONST_BOOLEAN) { @@ -578,6 +598,25 @@ void TheoryDatatypes::conflict(TNode a, TNode b){ void TheoryDatatypes::eqNotifyNewClass(TNode t){ if( t.getKind()==APPLY_CONSTRUCTOR ){ getOrMakeEqcInfo( t, true ); + //look at all equivalence classes with constructor terms +/* + for( BoolMap::const_iterator it = d_consEqc.begin(); it != d_consEqc.end(); ++it ){ + if( (*it).second ){ + TNode r = (*it).first; + if( r.getType()==t.getType() ){ + EqcInfo * ei = getOrMakeEqcInfo( r, false ); + if( ei && !ei->d_constructor.get().isNull() && ei->d_constructor.get().getOperator()!=t.getOperator() ){ + Node deq = ei->d_constructor.get().eqNode( t ).negate(); + d_pending.push_back( deq ); + d_pending_exp[ deq ] = d_true; + Trace("datatypes-infer") << "DtInfer : diff constructor : " << deq << std::endl; + d_infer.push_back( deq ); + } + } + } + } +*/ + d_consEqc[t] = true; } } @@ -615,18 +654,20 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ //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() ){ + Node unifEq = cons1.eqNode( cons2 ); + std::vector< Node > exp; + if( checkClashModEq( cons1, cons2, exp ) ){ + exp.push_back( unifEq ); //check for clash - d_conflictNode = explain( cons1.eqNode( cons2 ) ); + d_conflictNode = explain( exp ); Trace("dt-conflict") << "CONFLICT: Clash conflict : " << d_conflictNode << std::endl; d_out->conflict( d_conflictNode ); d_conflict = true; return; }else{ //do unification - Node unifEq = cons1.eqNode( cons2 ); for( int i=0; i<(int)cons1.getNumChildren(); i++ ) { - if( cons1[i]!=cons2[i] ){ + if( !areEqual( cons1[i], cons2[i] ) ){ Node eq = cons1[i].getType().isBoolean() ? cons1[i].iffNode( cons2[i] ) : cons1[i].eqNode( cons2[i] ); d_pending.push_back( eq ); d_pending_exp[ eq ] = unifEq; @@ -635,18 +676,36 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ d_infer_exp.push_back( unifEq ); } } +/* + std::vector< Node > rew; + if( DatatypesRewriter::checkClash( cons1, cons2, rew ) ){ + Assert(false); + }else{ + for( unsigned i=0; i<rew.size(); i++ ){ + d_pending.push_back( rew[i] ); + d_pending_exp[ rew[i] ] = unifEq; + Trace("datatypes-infer") << "DtInfer : cons-inj : " << rew[i] << " by " << unifEq << std::endl; + d_infer.push_back( rew[i] ); + d_infer_exp.push_back( unifEq ); + } + } +*/ } } if( !eqc1->d_inst && eqc2->d_inst ){ eqc1->d_inst = true; } - if( cons1.isNull() && !cons2.isNull() ){ - Debug("datatypes-debug") << "Must check if it is okay to set the constructor." << std::endl; - checkInst = true; - addConstructor( eqc2->d_constructor.get(), eqc1, t1 ); - if( d_conflict ){ - return; + if( !cons2.isNull() ){ + if( cons1.isNull() ){ + Debug("datatypes-debug") << "Must check if it is okay to set the constructor." << std::endl; + checkInst = true; + addConstructor( eqc2->d_constructor.get(), eqc1, t1 ); + if( d_conflict ){ + return; + } + d_consEqc[t1] = true; } + d_consEqc[t2] = false; } }else{ Debug("datatypes-debug") << "No eqc info for " << t1 << ", must create" << std::endl; @@ -939,7 +998,7 @@ void TheoryDatatypes::collapseSelector( Node s, Node c ) { //if( r!=rr ){ //Node eq_exp = NodeManager::currentNM()->mkConst(true); //Node eq = r.getType().isBoolean() ? r.iffNode( rr ) : r.eqNode( rr ); - if( s!=rr ){ + if( s!=rr ){:: Node eq_exp = c.eqNode( s[0] ); Node eq = rr.getType().isBoolean() ? s.iffNode( rr ) : s.eqNode( rr ); @@ -988,17 +1047,32 @@ void TheoryDatatypes::computeCareGraph(){ }else if( !areEqual( x, y ) ){ Trace("dt-cg") << "Arg #" << k << " is " << x << " " << y << std::endl; //check if they are definately disequal - - if( d_equalityEngine.isTriggerTerm(x, THEORY_UF) && d_equalityEngine.isTriggerTerm(y, THEORY_UF) ){ - TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_DATATYPES); - TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_DATATYPES); - Trace("dt-cg") << "Arg #" << k << " shared term is " << x_shared << " " << y_shared << std::endl; - //EqualityStatus eqStatus = d_valuation.getEqualityStatus(x_shared, y_shared); - //if( eqStatus!=EQUALITY_UNKNOWN ){ - currentPairs.push_back(make_pair(x_shared, y_shared)); + bool defDiseq = false; +/* + TNode rx = getRepresentative( x ); + EqcInfo* eix = getOrMakeEqcInfo( rx, false ); + if( eix ){ + TNode ry = getRepresentative( y ); + EqcInfo* eiy = getOrMakeEqcInfo( ry, false ); + if( eiy ){ + if( !eix->d_constructor.get().isNull() && !eiy->d_constructor.get().isNull() ){ + defDiseq = eix->d_constructor.get().getOperator()!=eiy->d_constructor.get().getOperator(); + }else{ + } + } + } +*/ + if( !defDiseq && d_equalityEngine.isTriggerTerm(x, THEORY_UF) && d_equalityEngine.isTriggerTerm(y, THEORY_UF) ){ + EqualityStatus eqStatus = d_valuation.getEqualityStatus(x, y); + if( eqStatus!=EQUALITY_UNKNOWN ){ + TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_DATATYPES); + TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_DATATYPES); + Trace("dt-cg") << "Arg #" << k << " shared term is " << x_shared << " " << y_shared << std::endl; + currentPairs.push_back(make_pair(x_shared, y_shared)); + } } } - } + } if (!somePairIsDisequal) { for (unsigned c = 0; c < currentPairs.size(); ++ c) { Trace("dt-cg-pair") << "Pair : " << currentPairs[c].first << " " << currentPairs[c].second << std::endl; @@ -1059,6 +1133,7 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ eq::EqClassesIterator eqccs_i = eq::EqClassesIterator( &d_equalityEngine ); std::vector< Node > cons; std::vector< Node > nodes; + std::map< Node, Node > eqc_cons; while( !eqccs_i.isFinished() ){ Node eqc = (*eqccs_i); //for all equivalence classes that are datatypes @@ -1066,51 +1141,55 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ EqcInfo* ei = getOrMakeEqcInfo( eqc ); if( !ei->d_constructor.get().isNull() ){ cons.push_back( ei->d_constructor.get() ); + eqc_cons[ eqc ] = ei->d_constructor.get(); }else{ nodes.push_back( eqc ); } } ++eqccs_i; } - + unsigned orig_size = nodes.size(); unsigned index = 0; while( index<nodes.size() ){ Node eqc = nodes[index]; Node neqc; + const Datatype& dt = ((DatatypeType)(eqc.getType()).toType()).getDatatype(); if( !d_equalityEngine.hasTerm( eqc ) ){ - Trace("dt-cmi") << "NOTICE : Datatypes: need to assign constructor for " << eqc << std::endl; - Trace("dt-cmi") << " Type : " << eqc.getType() << std::endl; - //can assign arbitrary term - TypeEnumerator te(eqc.getType()); - bool success; - do{ - success = true; - Assert( !te.isFinished() ); - neqc = *te; - Trace("dt-cmi-debug") << "Try " << neqc << " ... " << std::endl; - ++te; - //if it is infinite or we are assigning to terms known by datatypes, make sure it is fresh - if( eqc.getType().getCardinality().isInfinite() || index<orig_size ){ - for( unsigned i=0; i<cons.size(); i++ ){ - //check if it is modulo equality the same - if( cons[i].getOperator()==neqc.getOperator() ){ - bool diff = false; - for( unsigned j=0; j<cons[i].getNumChildren(); j++ ){ - if( !m->areEqual( cons[i][j], neqc[j] ) ){ - diff = true; + if( !dt.isCodatatype() ){ + Trace("dt-cmi") << "NOTICE : Datatypes: need to assign constructor for " << eqc << std::endl; + Trace("dt-cmi") << " Type : " << eqc.getType() << std::endl; + //can assign arbitrary term + TypeEnumerator te(eqc.getType()); + bool success; + do{ + success = true; + Assert( !te.isFinished() ); + neqc = *te; + Trace("dt-cmi-debug") << "Try " << neqc << " ... " << std::endl; + ++te; + //if it is infinite or we are assigning to terms known by datatypes, make sure it is fresh + if( eqc.getType().getCardinality().isInfinite() || index<orig_size ){ + for( unsigned i=0; i<cons.size(); i++ ){ + //check if it is modulo equality the same + if( cons[i].getOperator()==neqc.getOperator() ){ + bool diff = false; + for( unsigned j=0; j<cons[i].getNumChildren(); j++ ){ + if( !m->areEqual( 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; } } - if( !diff ){ - Trace("dt-cmi-debug") << "...Already equivalent modulo equality to " << cons[i] << std::endl; - success = false; - break; - } } } - } - }while( !success ); + }while( !success ); + } }else{ Trace("dt-cmi") << "NOTICE : Datatypes: no constructor in equivalence class " << eqc << std::endl; Trace("dt-cmi") << " Type : " << eqc.getType() << std::endl; @@ -1138,8 +1217,6 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ } Trace("dt-cmi") << std::endl; */ - - const Datatype& dt = ((DatatypeType)(eqc.getType()).toType()).getDatatype(); for( unsigned r=0; r<2; r++ ){ if( neqc.isNull() ){ for( unsigned i=0; i<pcons.size(); i++ ){ @@ -1158,9 +1235,11 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ } } } - Assert( !neqc.isNull() ); - Trace("dt-cmi") << "Assign : " << neqc << std::endl; - m->assertEquality( eqc, neqc, true ); + if( !neqc.isNull() ){ + Trace("dt-cmi") << "Assign : " << neqc << std::endl; + m->assertEquality( eqc, neqc, true ); + eqc_cons[ eqc ] = neqc; + } /* for( unsigned kk=0; kk<all_eqc.size(); kk++ ){ for( unsigned ll=(kk+1); ll<all_eqc.size(); ll++ ){ @@ -1184,9 +1263,44 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ ++index; } + //assign MU for each codatatype eqc + std::map< Node, Node > eqc_mu; + for( std::map< Node, Node >::iterator it = eqc_cons.begin(); it != eqc_cons.end(); ++it ){ + Node eqc = it->first; + const Datatype& dt = ((DatatypeType)(eqc.getType()).toType()).getDatatype(); + if( dt.isCodatatype() ){ + std::map< Node, Node > vmap; + Node v = getCodatatypesValue( it->first, eqc_cons, eqc_mu, vmap ); + Trace("dt-cmi-cod") << " EQC(" << it->first << "), constructor is " << it->second << ", value is " << v << std::endl; + } + } } +Node TheoryDatatypes::getCodatatypesValue( Node n, std::map< Node, Node >& eqc_cons, std::map< Node, Node >& eqc_mu, std::map< Node, Node >& vmap ){ + std::map< Node, Node >::iterator itv = vmap.find( n ); + if( itv!=vmap.end() ){ + return itv->second; + }else if( DatatypesRewriter::isTermDatatype( n ) ){ + Node nv = NodeManager::currentNM()->mkBoundVar( n.getType() ); + vmap[n] = nv; + Trace("dt-cmi-cod-debug") << " map " << n << " -> " << nv << std::endl; + Node nc = eqc_cons[n]; + Assert( nc.getKind()==APPLY_CONSTRUCTOR ); + std::vector< Node > children; + children.push_back( nc.getOperator() ); + for( unsigned i=0; i<nc.getNumChildren(); i++ ){ + Node r = getRepresentative( nc[i] ); + Node rv = getCodatatypesValue( r, eqc_cons, eqc_mu, vmap ); + children.push_back( rv ); + } + vmap.erase( n ); + return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children ); + }else{ + return n; + } +} + void TheoryDatatypes::collectTerms( Node n ) { if( d_collectTermsCache.find( n )==d_collectTermsCache.end() ){ d_collectTermsCache[n] = true; @@ -1234,7 +1348,7 @@ void TheoryDatatypes::processNewTerm( Node 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 ); + d_pending_exp[ eq ] = d_true; Trace("datatypes-infer") << "DtInfer : rewrite : " << eq << std::endl; d_infer.push_back( eq ); } @@ -1266,7 +1380,7 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){ Node exp; Node tt; if( !eqc->d_constructor.get().isNull() ){ - exp = NodeManager::currentNM()->mkConst( true ); + exp = d_true; tt = eqc->d_constructor; }else{ exp = getLabel( n ); @@ -1622,7 +1736,7 @@ bool TheoryDatatypes::areDisequal( TNode a, TNode b ){ } } -Node TheoryDatatypes::getRepresentative( TNode a ){ +TNode TheoryDatatypes::getRepresentative( TNode a ){ if( hasTerm( a ) ){ return d_equalityEngine.getRepresentative( a ); }else{ @@ -1692,10 +1806,51 @@ void TheoryDatatypes::printModelDebug( const char* c ){ Node TheoryDatatypes::mkAnd( std::vector< TNode >& assumptions ) { if( assumptions.empty() ){ - return NodeManager::currentNM()->mkConst( true ); + return d_true; }else if( assumptions.size()==1 ){ return assumptions[0]; }else{ return NodeManager::currentNM()->mkNode( AND, assumptions ); } } + +bool TheoryDatatypes::checkClashModEq( Node n1, Node n2, std::vector< Node >& exp ) { + if( (n1.getKind() == kind::APPLY_CONSTRUCTOR && n2.getKind() == kind::APPLY_CONSTRUCTOR) || + (n1.getKind() == kind::TUPLE && n2.getKind() == kind::TUPLE) || + (n1.getKind() == kind::RECORD && n2.getKind() == kind::RECORD) ) { + if( n1.getOperator() != n2.getOperator() ) { + return true; + } else { + Assert( n1.getNumChildren() == n2.getNumChildren() ); + for( int i=0; i<(int)n1.getNumChildren(); i++ ) { + TNode nc1 = n1[i]; + TNode nc2 = n2[i]; + if( DatatypesRewriter::isTermDatatype( n1[i] ) ){ + nc1 = getEqcConstructor( n1[i] ); + nc2 = getEqcConstructor( n2[i] ); + } + if( checkClashModEq( nc1, nc2, exp ) ) { + if( nc1!=n1[i] ){ + exp.push_back( nc1.eqNode( n1[i] ) ); + } + if( nc2!=n2[i] ){ + exp.push_back( nc2.eqNode( n2[i] ) ); + } + return true; + } + } + } + }else if( n1!=n2 ){ + if( n1.isConst() && n2.isConst() ){ + return true; + }else{ + Node eq = NodeManager::currentNM()->mkNode( n1.getType().isBoolean() ? kind::IFF : kind::EQUAL, n1, n2 ); + if( d_equalityEngine.areDisequal( n1, n2, true ) ){ + exp.push_back( eq.negate() ); + return true; + } + } + } + return false; +} + diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index eb86c3f76..fe87d4439 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -50,7 +50,7 @@ private: /** inferences */ NodeList d_infer; NodeList d_infer_exp; - + Node d_true; /** mkAnd */ Node mkAnd( std::vector< TNode >& assumptions ); private: @@ -156,6 +156,8 @@ private: NodeListMap d_labels; /** selector apps for eqch equivalence class */ NodeListMap d_selector_apps; + /** constructor terms */ + BoolMap d_consEqc; /** Are we in conflict */ context::CDO<bool> d_conflict; /** The conflict node */ @@ -183,6 +185,8 @@ private: EqcInfo* getOrMakeEqcInfo( Node n, bool doMake = false ); /** has eqc info */ bool hasEqcInfo( Node n ) { return d_labels.find( n )!=d_labels.end(); } + /** get eqc constructor */ + TNode getEqcConstructor( TNode r ); protected: /** compute care graph */ void computeCareGraph(); @@ -204,6 +208,7 @@ public: void explainPredicate( TNode p, bool polarity, std::vector<TNode>& assumptions ); void explain( TNode literal, std::vector<TNode>& assumptions ); Node explain( TNode literal ); + Node explain( std::vector< Node >& lits ); /** Conflict when merging two constants */ void conflict(TNode a, TNode b); /** called when a new equivalance class is created */ @@ -248,6 +253,8 @@ private: std::vector< TNode >& exp, std::map< Node, Node >& cn, std::map< Node, std::map< Node, int > >& dni, int dniLvl, bool mkExp ); + /** build model */ + Node getCodatatypesValue( Node n, std::map< Node, Node >& eqc_cons, std::map< Node, Node >& eqc_mu, std::map< Node, Node >& vmap ); /** collect terms */ void collectTerms( Node n ); /** get instantiate cons */ @@ -263,12 +270,14 @@ private: bool mustSpecifyAssignment(); /** must communicate fact */ bool mustCommunicateFact( Node n, Node exp ); + /** check clash mod eq */ + bool checkClashModEq( Node n1, Node n2, std::vector< Node >& exp ); private: //equality queries bool hasTerm( TNode a ); bool areEqual( TNode a, TNode b ); bool areDisequal( TNode a, TNode b ); - Node getRepresentative( TNode a ); + TNode getRepresentative( TNode a ); public: /** get equality engine */ eq::EqualityEngine* getEqualityEngine() { return &d_equalityEngine; } diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h index 972bdb2ec..4130bffee 100644 --- a/src/theory/quantifiers/bounded_integers.h +++ b/src/theory/quantifiers/bounded_integers.h @@ -121,6 +121,9 @@ public: void getBounds( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u ); void getBoundValues( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u ); bool isGroundRange(Node f, Node v); + + /** Identify this module */ + std::string identify() const { return "BoundedIntegers"; } }; } diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index 13186c7cc..da0a3c4f6 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -155,9 +155,7 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi Trace("matching") << "Matching " << t << " against pattern " << d_match_pattern << " (" << m << ")" << ", " << d_children.size() << ", pattern is " << d_pattern << std::endl; Assert( !d_match_pattern.isNull() ); - if( qe->d_optMatchIgnoreModelBasis && t.getAttribute(ModelBasisAttribute()) ){ - return true; - }else if( d_matchPolicy==MATCH_GEN_INTERNAL_ERROR ){ + if( d_matchPolicy==MATCH_GEN_INTERNAL_ERROR ){ return false; }else{ EqualityQuery* q = qe->getEqualityQuery(); @@ -324,9 +322,6 @@ int InstMatchGenerator::addInstantiations( Node f, InstMatch& baseMatch, Quantif m.add( baseMatch ); if( qe->addInstantiation( f, m ) ){ addedLemmas++; - if( qe->d_optInstLimitActive && qe->d_optInstLimit<=0 ){ - return addedLemmas; - } } }else{ addedLemmas++; diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h index 5f7e26297..394d53d42 100644 --- a/src/theory/quantifiers/instantiation_engine.h +++ b/src/theory/quantifiers/instantiation_engine.h @@ -150,6 +150,8 @@ public: ~Statistics(); }; Statistics d_statistics; + /** Identify this module */ + std::string identify() const { return "InstEngine"; } };/* class InstantiationEngine */ }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 8b62fc39b..d7b074acc 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -55,68 +55,74 @@ QuantifiersModule( qe ){ void ModelEngine::check( Theory::Effort e ){ if( e==Theory::EFFORT_LAST_CALL && !d_quantEngine->hasAddedLemma() ){ - FirstOrderModel* fm = d_quantEngine->getModel(); - //the following will attempt to build a model and test that it satisfies all asserted universal quantifiers int addedLemmas = 0; - //quantifiers are initialized, we begin an instantiation round - double clSet = 0; - if( Trace.isOn("model-engine") ){ - clSet = double(clock())/double(CLOCKS_PER_SEC); - } - ++(d_statistics.d_inst_rounds); - bool buildAtFullModel = d_builder->optBuildAtFullModel(); - //two effort levels: first try exhaustive instantiation without axioms, then with. - int startEffort = ( !fm->isAxiomAsserted() || options::axiomInstMode()==AXIOM_INST_MODE_DEFAULT ) ? 1 : 0; - for( int effort=startEffort; effort<2; effort++ ){ - // for effort = 0, we only instantiate non-axioms - // for effort = 1, we instantiate everything - if( addedLemmas==0 ){ - Trace("model-engine") << "---Model Engine Round---" << std::endl; - //initialize the model - Trace("model-engine-debug") << "Build model..." << std::endl; - d_builder->d_considerAxioms = effort>=1; - d_builder->d_addedLemmas = 0; - d_builder->buildModel( fm, buildAtFullModel ); - addedLemmas += (int)d_builder->d_addedLemmas; - //if builder has lemmas, add and return + bool needsBuild = true; + FirstOrderModel* fm = d_quantEngine->getModel(); + if( fm->getNumAssertedQuantifiers()>0 ){ + //the following will attempt to build a model and test that it satisfies all asserted universal quantifiers + //quantifiers are initialized, we begin an instantiation round + double clSet = 0; + if( Trace.isOn("model-engine") ){ + clSet = double(clock())/double(CLOCKS_PER_SEC); + } + ++(d_statistics.d_inst_rounds); + bool buildAtFullModel = d_builder->optBuildAtFullModel(); + needsBuild = !buildAtFullModel; + //two effort levels: first try exhaustive instantiation without axioms, then with. + int startEffort = ( !fm->isAxiomAsserted() || options::axiomInstMode()==AXIOM_INST_MODE_DEFAULT ) ? 1 : 0; + for( int effort=startEffort; effort<2; effort++ ){ + // for effort = 0, we only instantiate non-axioms + // for effort = 1, we instantiate everything if( addedLemmas==0 ){ - Trace("model-engine-debug") << "Verify uf ss is minimal..." << std::endl; - //let the strong solver verify that the model is minimal - //for debugging, this will if there are terms in the model that the strong solver was not notified of - if( ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->debugModel( fm ) ){ - Trace("model-engine-debug") << "Check model..." << std::endl; - d_incomplete_check = false; - //print debug - Debug("fmf-model-complete") << std::endl; - debugPrint("fmf-model-complete"); - //successfully built an acceptable model, now check it - addedLemmas += checkModel(); - }else{ - addedLemmas++; + Trace("model-engine") << "---Model Engine Round---" << std::endl; + //initialize the model + Trace("model-engine-debug") << "Build model..." << std::endl; + d_builder->d_considerAxioms = effort>=1; + d_builder->d_addedLemmas = 0; + d_builder->buildModel( fm, buildAtFullModel ); + addedLemmas += (int)d_builder->d_addedLemmas; + //if builder has lemmas, add and return + if( addedLemmas==0 ){ + Trace("model-engine-debug") << "Verify uf ss is minimal..." << std::endl; + //let the strong solver verify that the model is minimal + //for debugging, this will if there are terms in the model that the strong solver was not notified of + if( ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->debugModel( fm ) ){ + Trace("model-engine-debug") << "Check model..." << std::endl; + d_incomplete_check = false; + //print debug + Debug("fmf-model-complete") << std::endl; + debugPrint("fmf-model-complete"); + //successfully built an acceptable model, now check it + addedLemmas += checkModel(); + }else{ + addedLemmas++; + } } } - } - if( addedLemmas==0 ){ - //if we have not added lemmas yet and axiomInstMode=trust, then we are done - if( options::axiomInstMode()==AXIOM_INST_MODE_TRUST ){ - //we must return unknown if an axiom is asserted - if( effort==0 ){ - d_incomplete_check = true; + if( addedLemmas==0 ){ + //if we have not added lemmas yet and axiomInstMode=trust, then we are done + if( options::axiomInstMode()==AXIOM_INST_MODE_TRUST ){ + //we must return unknown if an axiom is asserted + if( effort==0 ){ + d_incomplete_check = true; + } + break; } - break; } } - } - if( Trace.isOn("model-engine") ){ - double clSet2 = double(clock())/double(CLOCKS_PER_SEC); - Trace("model-engine") << "Finished model engine, time = " << (clSet2-clSet) << std::endl; + if( Trace.isOn("model-engine") ){ + double clSet2 = double(clock())/double(CLOCKS_PER_SEC); + Trace("model-engine") << "Finished model engine, time = " << (clSet2-clSet) << std::endl; + } + }else{ + Trace("model-engine-debug") << "No quantified formulas asserted." << std::endl; } if( addedLemmas==0 ){ Trace("model-engine-debug") << "No lemmas added, incomplete = " << d_incomplete_check << std::endl; //CVC4 will answer SAT or unknown Trace("fmf-consistent") << std::endl; debugPrint("fmf-consistent"); - if( options::produceModels() && !buildAtFullModel ){ + if( options::produceModels() && needsBuild ){ // finish building the model d_builder->buildModel( fm, true ); } diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h index cf770a7b9..3b34f7504 100644 --- a/src/theory/quantifiers/model_engine.h +++ b/src/theory/quantifiers/model_engine.h @@ -68,6 +68,8 @@ public: ~Statistics(); }; Statistics d_statistics; + /** Identify this module */ + std::string identify() const { return "ModelEngine"; } };/* class ModelEngine */ }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 62bd347c7..8a0d956ac 100755 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -116,7 +116,7 @@ public: class QuantInfo {
private:
void registerNode( Node n, bool hasPol, bool pol, bool beneathQuant = false );
- void flatten( Node n, bool beneathQuant ); + void flatten( Node n, bool beneathQuant );
private: //for completing match
std::vector< int > d_unassigned;
std::vector< TypeNode > d_unassigned_tn;
@@ -156,8 +156,8 @@ public: bool completeMatch( QuantConflictFind * p, std::vector< int >& assigned, bool doContinue = false );
void revertMatch( std::vector< int >& assigned );
void debugPrintMatch( const char * c );
- bool isConstrainedVar( int v ); -public: + bool isConstrainedVar( int v );
+public:
void getMatch( std::vector< Node >& terms );
};
@@ -274,6 +274,8 @@ public: ~Statistics();
};
Statistics d_statistics;
+ /** Identify this module */
+ std::string identify() const { return "QcfEngine"; }
};
}
diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp index 59ba40ca7..75f54d7d9 100644 --- a/src/theory/quantifiers/rewrite_engine.cpp +++ b/src/theory/quantifiers/rewrite_engine.cpp @@ -39,6 +39,7 @@ struct PrioritySort { RewriteEngine::RewriteEngine( context::Context* c, QuantifiersEngine* qe ) : QuantifiersModule(qe) { d_true = NodeManager::currentNM()->mkConst( true ); + d_needsSort = true; } double RewriteEngine::getPriority( Node f ) { diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h index f85803617..a16a6d598 100644 --- a/src/theory/quantifiers/rewrite_engine.h +++ b/src/theory/quantifiers/rewrite_engine.h @@ -56,7 +56,9 @@ public: void check( Theory::Effort e ); void registerQuantifier( Node f ); - void assertNode( Node n ); + void assertNode( Node n ); + /** Identify this module */ + std::string identify() const { return "RewriteEngine"; } }; } diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 63697f5e7..be011cdb6 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -109,12 +109,6 @@ d_lemmas_produced_c(u){ } //options - d_optInstCheckDuplicate = true; - d_optInstMakeRepresentative = true; - d_optInstAddSplits = false; - d_optMatchIgnoreModelBasis = false; - d_optInstLimitActive = false; - d_optInstLimit = 0; d_total_inst_count_debug = 0; } @@ -166,6 +160,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ Trace("quant-engine") << "Master equality engine not consistent, return." << std::endl; return; } + Trace("quant-engine-debug") << "Resetting modules..." << std::endl; //reset relevant information d_hasAddedLemma = false; d_term_db->reset( e ); @@ -176,6 +171,8 @@ void QuantifiersEngine::check( Theory::Effort e ){ for( int i=0; i<(int)d_modules.size(); i++ ){ d_modules[i]->reset_round( e ); } + Trace("quant-engine-debug") << "Done resetting modules." << std::endl; + if( e==Theory::EFFORT_LAST_CALL ){ //if effort is last call, try to minimize model first if( options::finiteModelFind() ){ @@ -188,14 +185,19 @@ void QuantifiersEngine::check( Theory::Effort e ){ }else if( e==Theory::EFFORT_FULL ){ ++(d_statistics.d_instantiation_rounds); } + Trace("quant-engine-debug") << "Check with modules..." << std::endl; for( int i=0; i<(int)d_modules.size(); i++ ){ + Trace("quant-engine-debug") << "Check " << d_modules[i]->identify().c_str() << "..." << std::endl; d_modules[i]->check( e ); } + Trace("quant-engine-debug") << "Done check with modules." << std::endl; //build the model if not done so already // this happens if no quantifiers are currently asserted and no model-building module is enabled if( e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma ){ if( options::produceModels() && !d_model->isModelSet() ){ + Trace("quant-engine-debug") << "Build the model..." << std::endl; d_te->getModelBuilder()->buildModel( d_model, true ); + Trace("quant-engine-debug") << "Done building the model." << std::endl; } if( Trace.isOn("inst-per-quant") ){ for( std::map< Node, int >::iterator it = d_total_inst_debug.begin(); it != d_total_inst_debug.end(); ++it ){ diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 858093543..eb9803592 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -59,6 +59,8 @@ public: virtual void propagate( Theory::Effort level ){} virtual Node getNextDecisionRequest() { return TNode::null(); } virtual Node explain(TNode n) { return TNode::null(); } + /** Identify this module (for debugging, dynamic configuration, etc..) */ + virtual std::string identify() const = 0; };/* class QuantifiersModule */ namespace quantifiers { @@ -252,14 +254,6 @@ public: ~Statistics(); };/* class QuantifiersEngine::Statistics */ Statistics d_statistics; -public: - /** options */ - bool d_optInstCheckDuplicate; - bool d_optInstMakeRepresentative; - bool d_optInstAddSplits; - bool d_optMatchIgnoreModelBasis; - bool d_optInstLimitActive; - int d_optInstLimit; };/* class QuantifiersEngine */ |