From 30d21b25af6ee619e5f53d1ca8821b710fad4cb7 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 24 Jun 2013 12:52:07 -0500 Subject: [PATCH] Add options for symmetry breaking in uf+ss totality axiom approach, option for using clique lemmas instead of splitting on demand, option for simplifying models in fmf-fmc, minor fixes for rewrite engine --- .../quantifiers/candidate_generator.cpp | 28 +- src/theory/quantifiers/candidate_generator.h | 42 ++- src/theory/quantifiers/full_model_check.cpp | 244 +++++++++++++++--- src/theory/quantifiers/full_model_check.h | 16 +- .../quantifiers/inst_match_generator.cpp | 146 +++-------- src/theory/quantifiers/inst_match_generator.h | 4 - src/theory/quantifiers/options | 2 + src/theory/quantifiers/rewrite_engine.cpp | 4 +- src/theory/quantifiers/trigger.cpp | 7 + src/theory/rep_set.cpp | 7 + src/theory/uf/options | 5 + src/theory/uf/theory_uf_strong_solver.cpp | 94 +++++-- src/theory/uf/theory_uf_strong_solver.h | 6 + src/util/sort_inference.cpp | 5 +- 14 files changed, 418 insertions(+), 192 deletions(-) diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp index 6c6a80b90..e20f8c8e8 100644 --- a/src/theory/quantifiers/candidate_generator.cpp +++ b/src/theory/quantifiers/candidate_generator.cpp @@ -149,7 +149,7 @@ void CandidateGeneratorQELitEq::reset( Node eqc ){ d_eq = eq::EqClassesIterator( d_qe->getEqualityQuery()->getEngine() ); } Node CandidateGeneratorQELitEq::getNextCandidate(){ - while( d_eq.isFinished() ){ + while( !d_eq.isFinished() ){ Node n = (*d_eq); ++d_eq; if( n.getType()==d_match_pattern[0].getType() ){ @@ -186,3 +186,29 @@ Node CandidateGeneratorQELitDeq::getNextCandidate(){ } return Node::null(); } + + +CandidateGeneratorQEAll::CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mpat ) : + d_match_pattern( mpat ), d_qe( qe ){ + +} + +void CandidateGeneratorQEAll::resetInstantiationRound() { + +} + +void CandidateGeneratorQEAll::reset( Node eqc ) { + d_eq = eq::EqClassesIterator( d_qe->getEqualityQuery()->getEngine() ); +} + +Node CandidateGeneratorQEAll::getNextCandidate() { + while( !d_eq.isFinished() ){ + Node n = (*d_eq); + ++d_eq; + if( n.getType()==d_match_pattern.getType() ){ + //an equivalence class with the same type as the pattern, return it + return n; + } + } + return Node::null(); +} \ No newline at end of file diff --git a/src/theory/quantifiers/candidate_generator.h b/src/theory/quantifiers/candidate_generator.h index 81b98ce0a..402a29848 100644 --- a/src/theory/quantifiers/candidate_generator.h +++ b/src/theory/quantifiers/candidate_generator.h @@ -69,8 +69,7 @@ public: Node getNextCandidate(); };/* class CandidateGeneratorQueue */ -class CandidateGeneratorQEDisequal; - +//the default generator class CandidateGeneratorQE : public CandidateGenerator { friend class CandidateGeneratorQEDisequal; @@ -93,27 +92,6 @@ public: Node getNextCandidate(); }; - -//class CandidateGeneratorQEDisequal : public CandidateGenerator -//{ -//private: -// //equivalence class -// Node d_eq_class; -// //equivalence class info -// EqClassInfo* d_eci; -// //equivalence class iterator -// EqClassInfo::BoolMap::const_iterator d_eqci_iter; -// //instantiator pointer -// QuantifiersEngine* d_qe; -//public: -// CandidateGeneratorQEDisequal( QuantifiersEngine* qe, Node eqc ); -// ~CandidateGeneratorQEDisequal(){} -// -// void resetInstantiationRound(); -// void reset( Node eqc ); //should be what you want to be disequal from -// Node getNextCandidate(); -//}; - class CandidateGeneratorQELitEq : public CandidateGenerator { private: @@ -150,6 +128,24 @@ public: Node getNextCandidate(); }; +class CandidateGeneratorQEAll : public CandidateGenerator +{ +private: + //the equality classes iterator + eq::EqClassesIterator d_eq; + //equality you are trying to match equalities for + Node d_match_pattern; + //einstantiator pointer + QuantifiersEngine* d_qe; +public: + CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mpat ); + ~CandidateGeneratorQEAll(){} + + void resetInstantiationRound(); + void reset( Node eqc ); + Node getNextCandidate(); +}; + }/* CVC4::theory::inst namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index 2033797d5..4411d205e 100755 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -44,7 +44,7 @@ bool EntryTrie::hasGeneralization( FirstOrderModelFmc * m, Node c, int index ) { return true; } } - if( d_child.find( c[index] )!=d_child.end() ){ + if( c[index]!=st && d_child.find( c[index] )!=d_child.end() ){ if( d_child[ c[index] ].hasGeneralization(m, c, index+1) ){ return true; } @@ -63,7 +63,7 @@ int EntryTrie::getGeneralizationIndex( FirstOrderModelFmc * m, std::vector minIndex = d_child[st].getGeneralizationIndex(m, inst, index+1); } Node cc = inst[index]; - if( d_child.find( cc )!=d_child.end() ){ + if( cc!=st && d_child.find( cc )!=d_child.end() ){ int gindex = d_child[ cc ].getGeneralizationIndex(m, inst, index+1); if (minIndex==-1 || (gindex!=-1 && gindex & c } -bool Def::addEntry( FirstOrderModelFmc * m, Node c, Node v) { - if (!d_et.hasGeneralization(m, c)) { - int newIndex = (int)d_cond.size(); - if (!d_has_simplified) { - std::vector compat; - std::vector gen; - d_et.getEntries(m, c, compat, gen); - for( unsigned i=0; igetStar(tn); + if( c[index]==st ){ + //check if all children exist and are complete + int num_child_def = d_child.size() - (d_child.find(st)!=d_child.end() ? 1 : 0); + if( num_child_def==m->d_rep_set.getNumRepresentatives(tn) ){ + bool complete = true; + for ( std::map::iterator it = d_child.begin(); it != d_child.end(); ++it ){ + if( !m->isStar(it->first) ){ + if( !it->second.isComplete(m, c, index+1) ){ + complete = false; + break; + } } } - } - for( unsigned i=0; i& indices ) { + if (index==(int)c.getNumChildren()) { + if( d_data!=-1 ){ + indices.push_back( d_data ); + } }else{ + for ( std::map::iterator it = d_child.begin(); it != d_child.end(); ++it ){ + it->second.collectIndices(c, index+1, indices ); + } + } +} + +bool EntryTrie::isComplete(FirstOrderModelFmc * m, Node c, int index) { + if( d_complete==-1 ){ + d_complete = 1; + if (index<(int)c.getNumChildren()) { + Node st = m->getStar(c[index].getType()); + if(d_child.find(st)!=d_child.end()) { + if (!d_child[st].isComplete(m, c, index+1)) { + d_complete = 0; + } + }else{ + d_complete = 0; + } + } + } + return d_complete==1; +} + +bool Def::addEntry( FirstOrderModelFmc * m, Node c, Node v) { + if (d_et.hasGeneralization(m, c)) { return false; } + if( options::fmfFmcCoverSimplify() ){ + if( d_et.isCovered(m, c, 0) ){ + Trace("fmc-cover-simplify") << "Entry " << c << " is covered." << std::endl; + return false; + } + } + int newIndex = (int)d_cond.size(); + if (!d_has_simplified) { + std::vector compat; + std::vector gen; + d_et.getEntries(m, c, compat, gen); + for( unsigned i=0; i& inst ) { @@ -156,7 +225,7 @@ int Def::getGeneralizationIndex( FirstOrderModelFmc * m, std::vector& inst return d_et.getGeneralizationIndex(m, inst); } -void Def::simplify(FirstOrderModelFmc * m) { +void Def::basic_simplify( FirstOrderModelFmc * m ) { d_has_simplified = true; std::vector< Node > cond; cond.insert( cond.end(), d_cond.begin(), d_cond.end() ); @@ -173,6 +242,111 @@ void Def::simplify(FirstOrderModelFmc * m) { d_status.clear(); } +void Def::simplify(FullModelChecker * mc, FirstOrderModelFmc * m) { + basic_simplify( m ); + + //check if the last entry is not all star, if so, we can make the last entry all stars + if( !d_cond.empty() ){ + bool last_all_stars = true; + Node cc = d_cond[d_cond.size()-1]; + for( unsigned i=0; iisStar(cc[i]) ){ + last_all_stars = false; + break; + } + } + if( !last_all_stars ){ + Trace("fmc-cover-simplify") << "Need to modify last entry to be all stars." << std::endl; + Trace("fmc-cover-simplify") << "Beforehand: " << std::endl; + debugPrint("fmc-cover-simplify",Node::null(), mc); + Trace("fmc-cover-simplify") << std::endl; + std::vector< Node > cond; + cond.insert( cond.end(), d_cond.begin(), d_cond.end() ); + d_cond.clear(); + std::vector< Node > value; + value.insert( value.end(), d_value.begin(), d_value.end() ); + d_value.clear(); + d_et.reset(); + d_has_simplified = false; + //change the last to all star + std::vector< Node > nc; + nc.push_back( cc.getOperator() ); + for( unsigned j=0; j< cc.getNumChildren(); j++){ + nc.push_back(m->getStar(cc[j].getType())); + } + cond[cond.size()-1] = NodeManager::currentNM()->mkNode( APPLY_UF, nc ); + //re-add the entries + for (unsigned i=0; i indices; + std::map< int, std::vector< int > > star_replace; + d_et.exhaustiveSimplify( m, d_cond[0], 0, indices, star_replace ); + if( !indices.empty() ){ + static bool appSimp = false; + if( !appSimp ){ + appSimp = true; + std::cout << "FMC-CS" << std::endl; + } + Trace("fmc-cover-simplify") << "Beforehand: " << std::endl; + debugPrint("fmc-cover-simplify",Node::null(), mc); + Trace("fmc-cover-simplify") << std::endl; + d_has_simplified = false; + Trace("fmc-cover-simplify") << "By exhaustive covering, these indices can be removed : "; + for( unsigned i=0; i cond; + cond.insert( cond.end(), d_cond.begin(), d_cond.end() ); + d_cond.clear(); + std::vector< Node > value; + value.insert( value.end(), d_value.begin(), d_value.end() ); + d_value.clear(); + d_et.reset(); + d_has_simplified = false; + for (unsigned i=0; i nc; + nc.push_back( cc.getOperator() ); + Trace("fmc-cover-simplify") << "Modify entry : " << cc << std::endl; + for( unsigned j=0; j< cc.getNumChildren(); j++){ + if( std::find( star_replace[i].begin(), star_replace[i].end(), j )!=star_replace[i].end() ){ + nc.push_back( m->getStar(cc[j].getType()) ); + }else{ + nc.push_back( cc[j] ); + } + } + cc = NodeManager::currentNM()->mkNode( APPLY_UF, nc ); + Trace("fmc-cover-simplify") << "Got : " << cc << std::endl; + } + addEntry(m, cc, value[i]); + } + } + Trace("fmc-cover-simplify") << "Finished re-adding entries." << std::endl; + basic_simplify( m ); + Trace("fmc-cover-simplify") << "Afterhand: " << std::endl; + debugPrint("fmc-cover-simplify",Node::null(), mc); + Trace("fmc-cover-simplify") << std::endl; + } + } + */ +} + void Def::debugPrint(const char * tr, Node op, FullModelChecker * m) { if (!op.isNull()) { Trace(tr) << "Model for " << op << " : " << std::endl; @@ -263,8 +437,15 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ for( unsigned i=0; id_model_basis_rep.find( tn )==fm->d_model_basis_rep.end() ){ - Node mbn = d_qe->getTermDatabase()->getModelBasisTerm(tn); - fm->d_model_basis_rep[tn] = fm->getUsedRepresentative( mbn ); + Node mbn; + if (!fm->d_rep_set.hasType(tn)) { + mbn = fm->getSomeDomainElement(tn); + }else{ + mbn = d_qe->getTermDatabase()->getModelBasisTerm(tn); + } + Node mbnr = fm->getUsedRepresentative( mbn ); + fm->d_model_basis_rep[tn] = mbnr; + Trace("fmc") << "Add model basis for type " << tn << " : " << mbn << " " << mbnr << std::endl; } } } @@ -319,7 +500,8 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ fm->d_models[op]->debugPrint("fmc-model", op, this); Trace("fmc-model") << std::endl; - fm->d_models[op]->simplify( fm ); + Trace("fmc-model-simplify") << "Simplifying " << op << "..." << std::endl; + fm->d_models[op]->simplify( this, fm ); Trace("fmc-model-simplify") << "After simplification : " << std::endl; fm->d_models[op]->debugPrint("fmc-model-simplify", op, this); Trace("fmc-model-simplify") << std::endl; @@ -617,7 +799,9 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n doInterpretedCompose( fm, f, d, n, children, 0, cond, val ); } } - d.simplify(fm); + Trace("fmc-debug") << "Simplify the definition..." << std::endl; + d.simplify(this, fm); + Trace("fmc-debug") << "Done simplifying" << std::endl; } Trace("fmc-debug") << "Definition for " << n << " is : " << std::endl; d.debugPrint("fmc-debug", Node::null(), this); @@ -709,7 +893,9 @@ void FullModelChecker::doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, //add them to the definition for( unsigned e=0; e d_child; int d_data; - void reset() { d_data = -1; d_child.clear(); } + void reset() { d_data = -1; d_child.clear(); d_complete = -1; } void addEntry( FirstOrderModelFmc * m, Node c, Node v, int data, int index = 0 ); bool hasGeneralization( FirstOrderModelFmc * m, Node c, int index = 0 ); int getGeneralizationIndex( FirstOrderModelFmc * m, std::vector & inst, int index = 0 ); void getEntries( FirstOrderModelFmc * m, Node c, std::vector & compat, std::vector & gen, int index = 0, bool is_gen = true ); + + bool isCovered(FirstOrderModelFmc * m, Node c, int index); + + //void exhaustiveSimplify( FirstOrderModelFmc * m, Node c, int index, std::vector< int >& indices, + // std::map< int, std::vector< int > >& star_replace ); + void collectIndices(Node c, int index, std::vector< int >& indices ); + bool isComplete(FirstOrderModelFmc * m, Node c, int index); }; @@ -47,6 +56,7 @@ public: std::vector< Node > d_cond; //value is returned by FullModelChecker::getRepresentative std::vector< Node > d_value; + void basic_simplify( FirstOrderModelFmc * m ); private: enum { status_unk, @@ -67,7 +77,7 @@ public: bool addEntry( FirstOrderModelFmc * m, Node c, Node v); Node evaluate( FirstOrderModelFmc * m, std::vector& inst ); int getGeneralizationIndex( FirstOrderModelFmc * m, std::vector& inst ); - void simplify( FirstOrderModelFmc * m ); + void simplify( FullModelChecker * mc, FirstOrderModelFmc * m ); void debugPrint(const char * tr, Node op, FullModelChecker * m); }; diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index 50362340b..bf4bb15a6 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -53,30 +53,39 @@ void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMat d_match_pattern = d_pattern[0]; } if( d_match_pattern.getKind()==IFF || d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==GEQ ){ + //make sure the matching portion of the equality is on the LHS of d_pattern + // and record what d_match_pattern is if( !quantifiers::TermDb::hasInstConstAttr(d_match_pattern[0]) || d_match_pattern[0].getKind()==INST_CONSTANT ){ - Assert( quantifiers::TermDb::hasInstConstAttr(d_match_pattern[1]) ); - Node mp = d_match_pattern[1]; - //swap sides - Node pat = d_pattern; - if(d_match_pattern.getKind()==GEQ){ - d_pattern = NodeManager::currentNM()->mkNode( kind::GT, d_match_pattern[1], d_match_pattern[0] ); - d_pattern = d_pattern.negate(); - }else{ - d_pattern = NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), d_match_pattern[1], d_match_pattern[0] ); + if( d_match_pattern[1].getKind()!=INST_CONSTANT ){ + Assert( quantifiers::TermDb::hasInstConstAttr(d_match_pattern[1]) ); + Node mp = d_match_pattern[1]; + //swap sides + Node pat = d_pattern; + if(d_match_pattern.getKind()==GEQ){ + d_pattern = NodeManager::currentNM()->mkNode( kind::GT, d_match_pattern[1], d_match_pattern[0] ); + d_pattern = d_pattern.negate(); + }else{ + d_pattern = NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), d_match_pattern[1], d_match_pattern[0] ); + } + d_pattern = pat.getKind()==NOT ? d_pattern.negate() : d_pattern; + d_match_pattern = mp; } - d_pattern = pat.getKind()==NOT ? d_pattern.negate() : d_pattern; - d_match_pattern = mp; }else if( !quantifiers::TermDb::hasInstConstAttr(d_match_pattern[1]) || d_match_pattern[1].getKind()==INST_CONSTANT ){ - Assert( quantifiers::TermDb::hasInstConstAttr(d_match_pattern[0]) ); - if( d_pattern.getKind()!=NOT ){ //TEMPORARY until we do better implementation of disequality matching - d_match_pattern = d_match_pattern[0]; - }else if( d_match_pattern[1].getKind()==INST_CONSTANT ){ - d_match_pattern = d_match_pattern[0]; + if( d_match_pattern[0].getKind()!=INST_CONSTANT ){ + Assert( quantifiers::TermDb::hasInstConstAttr(d_match_pattern[0]) ); + if( d_pattern.getKind()!=NOT ){ //TEMPORARY until we do better implementation of disequality matching + d_match_pattern = d_match_pattern[0]; + }else if( d_match_pattern[1].getKind()==INST_CONSTANT ){ + d_match_pattern = d_match_pattern[0]; + } } } } + Trace("inst-match-gen") << "Pattern is " << d_pattern << ", match pattern is " << d_match_pattern << std::endl; + + //now, collect children of d_match_pattern int childMatchPolicy = MATCH_GEN_DEFAULT; for( int i=0; i<(int)d_match_pattern.getNumChildren(); i++ ){ if( quantifiers::TermDb::hasInstConstAttr(d_match_pattern[i]) ){ @@ -89,10 +98,11 @@ void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMat } } - Debug("inst-match-gen") << "Pattern is " << d_pattern << ", match pattern is " << d_match_pattern << std::endl; - //create candidate generator - if( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ){ + if( d_match_pattern.getKind()==INST_CONSTANT ){ + d_cg = new CandidateGeneratorQEAll( qe, d_match_pattern ); + } + else if( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ){ Assert( d_matchPolicy==MATCH_GEN_DEFAULT ); //we will be producing candidates via literal matching heuristics if( d_pattern.getKind()!=NOT ){ @@ -118,40 +128,24 @@ void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMat Assert( Trigger::isAtomicTrigger( d_match_pattern ) ); //we are matching only in a particular equivalence class d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern.getOperator() ); - }else if( Trigger::isAtomicTrigger( d_match_pattern ) ){ - //if( d_matchPolicy==MATCH_GEN_EFFICIENT_E_MATCH ){ - //Warning() << "Currently efficient e matching is not taken into account for quantifiers: " << d_pattern << std::endl; - //} //we will be scanning lists trying to find d_match_pattern.getOperator() d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern.getOperator() ); }else{ d_cg = new CandidateGeneratorQueue; - if( !Trigger::isArithmeticTrigger( quantifiers::TermDb::getInstConstAttr(d_match_pattern), d_match_pattern, d_arith_coeffs ) ){ - Debug("inst-match-gen") << "(?) Unknown matching pattern is " << d_match_pattern << std::endl; - //Warning() << "(?) Unknown matching pattern is " << d_match_pattern << std::endl; - d_matchPolicy = MATCH_GEN_INTERNAL_ERROR; - }else{ - Debug("matching-arith") << "Generated arithmetic pattern for " << d_match_pattern << ": " << std::endl; - for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){ - Debug("matching-arith") << " " << it->first << " -> " << it->second << std::endl; - } - //we will treat this as match gen internal arithmetic - d_matchPolicy = MATCH_GEN_INTERNAL_ARITHMETIC; - } + Trace("inst-match-gen-warn") << "(?) Unknown matching pattern is " << d_match_pattern << std::endl; + d_matchPolicy = MATCH_GEN_INTERNAL_ERROR; } } } /** get match (not modulo equality) */ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngine* qe ){ - Debug("matching") << "Matching " << t << " against pattern " << d_match_pattern << " (" + 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_ARITHMETIC ){ - return getMatchArithmetic( t, m, qe ); }else if( d_matchPolicy==MATCH_GEN_INTERNAL_ERROR ){ return false; }else{ @@ -176,18 +170,18 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi } if( !m.setMatch( q, vv, tt ) ){ //match is in conflict - Debug("matching-debug") << "Match in conflict " << tt << " and " + Trace("matching-debug") << "Match in conflict " << tt << " and " << vv << " because " << m.get(vv) << std::endl; - Debug("matching-fail") << "Match fail: " << m.get(vv) << " and " << tt << std::endl; + Trace("matching-fail") << "Match fail: " << m.get(vv) << " and " << tt << std::endl; success = false; break; } } }else{ if( !q->areEqual( d_match_pattern[i], t[i] ) ){ - Debug("matching-fail") << "Match fail arg: " << d_match_pattern[i] << " and " << t[i] << std::endl; + Trace("matching-fail") << "Match fail arg: " << d_match_pattern[i] << " and " << t[i] << std::endl; //ground arguments are not equal success = false; break; @@ -250,68 +244,10 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi } } -bool InstMatchGenerator::getMatchArithmetic( Node t, InstMatch& m, QuantifiersEngine* qe ){ - Debug("matching-arith") << "Matching " << t << " " << d_match_pattern << std::endl; - if( !d_arith_coeffs.empty() ){ - NodeBuilder<> tb(kind::PLUS); - Node ic = Node::null(); - for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){ - Debug("matching-arith") << it->first << " -> " << it->second << std::endl; - if( !it->first.isNull() ){ - if( m.find( it->first )==m.end() ){ - //see if we can choose this to set - if( ic.isNull() && ( it->second.isNull() || !it->first.getType().isInteger() ) ){ - ic = it->first; - } - }else{ - Debug("matching-arith") << "already set " << m.get( it->first ) << std::endl; - Node tm = m.get( it->first ); - if( !it->second.isNull() ){ - tm = NodeManager::currentNM()->mkNode( MULT, it->second, tm ); - } - tb << tm; - } - }else{ - tb << it->second; - } - } - if( !ic.isNull() ){ - Node tm; - if( tb.getNumChildren()==0 ){ - tm = t; - }else{ - tm = tb.getNumChildren()==1 ? tb.getChild( 0 ) : tb; - tm = NodeManager::currentNM()->mkNode( MINUS, t, tm ); - } - if( !d_arith_coeffs[ ic ].isNull() ){ - Assert( !ic.getType().isInteger() ); - Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / d_arith_coeffs[ ic ].getConst() ); - tm = NodeManager::currentNM()->mkNode( MULT, coeff, tm ); - } - m.set( ic, Rewriter::rewrite( tm )); - //set the rest to zeros - for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){ - if( !it->first.isNull() ){ - if( m.find( it->first )==m.end() ){ - m.set( it->first, NodeManager::currentNM()->mkConst( Rational(0) ) ); - } - } - } - Debug("matching-arith") << "Setting " << ic << " to " << tm << std::endl; - return true; - }else{ - return false; - } - }else{ - return false; - } -} - - /** reset instantiation round */ void InstMatchGenerator::resetInstantiationRound( QuantifiersEngine* qe ){ if( !d_match_pattern.isNull() ){ - Debug("matching-debug2") << this << " reset instantiation round." << std::endl; + Trace("matching-debug2") << this << " reset instantiation round." << std::endl; d_needsReset = true; if( d_cg ){ d_cg->resetInstantiationRound(); @@ -323,7 +259,7 @@ void InstMatchGenerator::resetInstantiationRound( QuantifiersEngine* qe ){ } void InstMatchGenerator::reset( Node eqc, QuantifiersEngine* qe ){ - Debug("matching-debug2") << this << " reset " << eqc << "." << std::endl; + Trace("matching-debug2") << this << " reset " << eqc << "." << std::endl; if( !eqc.isNull() ){ d_eq_class = eqc; } @@ -336,17 +272,17 @@ void InstMatchGenerator::reset( Node eqc, QuantifiersEngine* qe ){ bool InstMatchGenerator::getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ){ if( d_needsReset ){ - Debug("matching") << "Reset not done yet, must do the reset..." << std::endl; + Trace("matching") << "Reset not done yet, must do the reset..." << std::endl; reset( d_eq_class.getKind()==INST_CONSTANT ? Node::null() : d_eq_class, qe ); } m.d_matched = Node::null(); - Debug("matching") << this << " " << d_match_pattern << " get next match " << m << " in eq class " << d_eq_class << std::endl; + Trace("matching") << this << " " << d_match_pattern << " get next match " << m << " in eq class " << d_eq_class << std::endl; bool success = false; Node t; do{ //get the next candidate term t t = d_cg->getNextCandidate(); - Debug("matching-debug2") << "Matching candidate : " << t << std::endl; + Trace("matching-debug2") << "Matching candidate : " << t << std::endl; //if t not null, try to fit it into match m if( !t.isNull() && t.getType()==d_match_pattern.getType() ){ success = getMatch( f, t, m, qe ); @@ -354,7 +290,7 @@ bool InstMatchGenerator::getNextMatch( Node f, InstMatch& m, QuantifiersEngine* }while( !success && !t.isNull() ); m.d_matched = t; if( !success ){ - Debug("matching") << this << " failed, reset " << d_eq_class << std::endl; + Trace("matching") << this << " failed, reset " << d_eq_class << std::endl; //we failed, must reset reset( d_eq_class.getKind()==INST_CONSTANT ? Node::null() : d_eq_class, qe ); } diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h index 9f856a56b..5d2128922 100644 --- a/src/theory/quantifiers/inst_match_generator.h +++ b/src/theory/quantifiers/inst_match_generator.h @@ -73,12 +73,8 @@ public: MATCH_GEN_DEFAULT = 0, MATCH_GEN_EFFICIENT_E_MATCH, //generate matches via Efficient E-matching for SMT solvers //others (internally used) - MATCH_GEN_INTERNAL_ARITHMETIC, MATCH_GEN_INTERNAL_ERROR, }; -private: - /** for arithmetic */ - bool getMatchArithmetic( Node t, InstMatch& m, QuantifiersEngine* qe ); public: /** get the match against ground term or formula t. d_match_pattern and t should have the same shape. diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index a0e42c425..0f9d0f295 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -97,6 +97,8 @@ option fmfFullModelCheck --fmf-fmc bool :default false enable full model check for finite model finding option fmfFullModelCheckSimple /--disable-fmf-fmc-simple bool :default true disable simple models in full model check for finite model finding +option fmfFmcCoverSimplify --fmf-fmc-cover-simplify bool :default false + apply covering simplification technique to fmc models option fmfOneInstPerRound --fmf-one-inst-per-round bool :default false only add one instantiation per quantifier per round for fmf diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp index 5a35e3808..84d465579 100755 --- a/src/theory/quantifiers/rewrite_engine.cpp +++ b/src/theory/quantifiers/rewrite_engine.cpp @@ -36,7 +36,7 @@ void RewriteEngine::check( Theory::Effort e ) { for( unsigned i=0; iaddInstantiation( f, m ) ){ addedLemmas++; Trace("rewrite-engine-inst-debug") << "success" << std::endl; diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index b71a1486c..39063942d 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -73,6 +73,7 @@ d_quantEngine( qe ), d_f( f ){ qe->getTermDatabase()->registerTrigger( this, d_nodes[i].getOperator() ); } } + Trace("trigger-debug") << "Finished making trigger." << std::endl; } void Trigger::resetInstantiationRound(){ @@ -144,6 +145,12 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& } } if( varCountcounter; i-- ){ if (!resetIndex(i)){ break; + }else if( domainSize(i)<=0 ){ + emptyDomain = true; } } + if( emptyDomain ){ + Trace("rsi-debug") << "This is an empty domain, increment again." << std::endl; + increment(); + } } } diff --git a/src/theory/uf/options b/src/theory/uf/options index bed535342..437e30e46 100644 --- a/src/theory/uf/options +++ b/src/theory/uf/options @@ -23,6 +23,8 @@ option ufssTotalityLimited --uf-ss-totality-limited=N int :default -1 apply totality axioms, but only up to cardinality N (-1 == do not apply totality axioms, default) option ufssTotalityLazy --uf-ss-totality-lazy bool :default false apply totality axioms lazily +option ufssTotalitySymBreak --uf-ss-totality-sym-break bool :default false + apply symmetry breaking for totality axioms option ufssAbortCardinality --uf-ss-abort-card=N int :default -1 tells the uf strong solver a cardinality to abort at (-1 == no limit, default) option ufssSmartSplits --uf-ss-smart-split bool :default false @@ -35,5 +37,8 @@ option ufssDiseqPropagation --uf-ss-deq-prop bool :default false eagerly propagate disequalities for uf strong solver option ufssMinimalModel /--disable-uf-ss-min-model bool :default true disable finding a minimal model in uf strong solver +option ufssCliqueSplits --uf-ss-clique-splits bool :default false + use cliques instead of splitting on demand to shrink model + endmodule diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index e868460f8..baa40463f 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -322,6 +322,20 @@ bool StrongSolverTheoryUF::SortModel::Region::check( Theory::Effort level, int c return false; } +bool StrongSolverTheoryUF::SortModel::Region::getCandidateClique( int cardinality, std::vector< Node >& clique ) { + if( d_testCliqueSize>=long(cardinality+1) ){ + //test clique is a clique + for( NodeBoolMap::iterator it = d_testClique.begin(); it != d_testClique.end(); ++it ){ + if( (*it).second ){ + clique.push_back( (*it).first ); + } + } + return true; + } + return false; +} + + void StrongSolverTheoryUF::SortModel::Region::getRepresentatives( std::vector< Node >& reps ){ for( std::map< Node, RegionNodeInfo* >::iterator it = d_nodes.begin(); it != d_nodes.end(); ++it ){ RegionNodeInfo* rni = it->second; @@ -625,11 +639,21 @@ void StrongSolverTheoryUF::SortModel::check( Theory::Effort level, OutputChannel //see if we have any recommended splits from large regions for( int i=0; i<(int)d_regions_index; i++ ){ if( d_regions[i]->d_valid && d_regions[i]->getNumReps()>d_cardinality ){ - if( addSplit( d_regions[i], out ) ){ - addedLemma = true; + //just add the clique lemma + if( level==Theory::EFFORT_FULL && options::ufssCliqueSplits() ){ + std::vector< Node > clique; + if( d_regions[i]->getCandidateClique( d_cardinality, clique ) ){ + //add clique lemma + addCliqueLemma( clique, out ); + return; + } + }else{ + if( addSplit( d_regions[i], out ) ){ + addedLemma = true; #ifdef ONE_SPLIT_REGION - break; + break; #endif + } } } } @@ -977,14 +1001,14 @@ void StrongSolverTheoryUF::SortModel::allocateCardinality( OutputChannel* out ){ if( applyTotality( d_aloc_cardinality ) ){ //must generate new cardinality lemma term Node var; - if( d_aloc_cardinality==1 ){ + //if( d_aloc_cardinality==1 ){ //get arbitrary ground term - var = d_cardinality_term; - }else{ + //var = d_cardinality_term; + //}else{ std::stringstream ss; ss << "_c_" << d_aloc_cardinality; var = NodeManager::currentNM()->mkSkolem( ss.str(), d_type, "is a cardinality lemma term" ); - } + //} d_totality_terms[0].push_back( var ); Trace("mkVar") << "allocateCardinality, mkVar : " << var << " : " << d_type << std::endl; //must be distinct from all other cardinality terms @@ -1097,6 +1121,12 @@ void StrongSolverTheoryUF::SortModel::addCliqueLemma( std::vector< Node >& cliqu while( clique.size()>size_t(d_cardinality+1) ){ clique.pop_back(); } + //debugging information + if( Trace.isOn("uf-ss-cliques") ){ + std::vector< Node > clique_vec; + clique_vec.insert( clique_vec.begin(), clique.begin(), clique.end() ); + d_cliques[ d_cardinality ].push_back( clique_vec ); + } if( options::ufssSimpleCliques() && !options::ufssExplainedCliques() ){ //add as lemma std::vector< Node > eqs; @@ -1109,16 +1139,10 @@ void StrongSolverTheoryUF::SortModel::addCliqueLemma( std::vector< Node >& cliqu } eqs.push_back( d_cardinality_literal[ d_cardinality ].notNode() ); Node lem = NodeManager::currentNM()->mkNode( OR, eqs ); - Trace("uf-ss-lemma") << "*** Add clique conflict " << lem << std::endl; + Trace("uf-ss-lemma") << "*** Add clique lemma " << lem << std::endl; ++( d_thss->d_statistics.d_clique_lemmas ); out->lemma( lem ); }else{ - //debugging information - if( Trace.isOn("uf-ss-cliques") ){ - std::vector< Node > clique_vec; - clique_vec.insert( clique_vec.begin(), clique.begin(), clique.end() ); - d_cliques[ d_cardinality ].push_back( clique_vec ); - } //found a clique Debug("uf-ss-cliques") << "Found a clique (cardinality=" << d_cardinality << ") :" << std::endl; Debug("uf-ss-cliques") << " "; @@ -1243,17 +1267,39 @@ void StrongSolverTheoryUF::SortModel::addCliqueLemma( std::vector< Node >& cliqu } void StrongSolverTheoryUF::SortModel::addTotalityAxiom( Node n, int cardinality, OutputChannel* out ){ - Node cardLit = d_cardinality_literal[ cardinality ]; - std::vector< Node > eqs; - for( int i=0; igetTheory()->getQuantifiersEngine()->getTheoryEngine()->getSortInference()->getSortId(n); + } + Trace("uf-ss-totality") << "Add totality lemma for " << n << " " << cardinality << ", sort id is " << sort_id << std::endl; + int use_cardinality = cardinality; + if( options::ufssTotalitySymBreak() ){ + if( d_sym_break_index.find(n)!=d_sym_break_index.end() ){ + use_cardinality = d_sym_break_index[n]; + }else if( (int)d_sym_break_terms[n.getType()][sort_id].size()getOutputChannel().lemma( lem ); + ++( d_thss->d_statistics.d_totality_lemmas ); + } } - Node ax = NodeManager::currentNM()->mkNode( OR, eqs ); - Node lem = NodeManager::currentNM()->mkNode( IMPLIES, cardLit, ax ); - Trace("uf-ss-lemma") << "*** Add totality axiom " << lem << std::endl; - //send as lemma to the output channel - d_thss->getOutputChannel().lemma( lem ); - ++( d_thss->d_statistics.d_totality_lemmas ); } /** apply totality */ diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h index 0cc995723..d263d8cc7 100644 --- a/src/theory/uf/theory_uf_strong_solver.h +++ b/src/theory/uf/theory_uf_strong_solver.h @@ -45,6 +45,10 @@ protected: public: /** information for incremental conflict/clique finding for a particular sort */ class SortModel { + private: + std::map< Node, std::vector< int > > d_totality_lems; + std::map< TypeNode, std::map< int, std::vector< Node > > > d_sym_break_terms; + std::map< Node, int > d_sym_break_index; public: /** a partition of the current equality graph for which cliques can occur internally */ class Region { @@ -146,6 +150,8 @@ public: public: /** check for cliques */ bool check( Theory::Effort level, int cardinality, std::vector< Node >& clique ); + /** get candidate clique */ + bool getCandidateClique( int cardinality, std::vector< Node >& clique ); //print debug void debugPrint( const char* c, bool incClique = false ); }; diff --git a/src/util/sort_inference.cpp b/src/util/sort_inference.cpp index d44499fa8..13631e590 100644 --- a/src/util/sort_inference.cpp +++ b/src/util/sort_inference.cpp @@ -191,7 +191,10 @@ int SortInference::process( Node n, std::map< Node, Node >& var_bound ){ int retType; if( n.getKind()==kind::EQUAL ){ //we only require that the left and right hand side must be equal - setEqual( child_types[0], child_types[1] ); + //setEqual( child_types[0], child_types[1] ); + int eqType = getIdForType( n[0].getType() ); + setEqual( child_types[0], eqType ); + setEqual( child_types[1], eqType ); retType = getIdForType( n.getType() ); }else if( n.getKind()==kind::APPLY_UF ){ Node op = n.getOperator(); -- 2.30.2