diff options
| -rw-r--r-- | src/theory/quantifiers/candidate_generator.cpp | 28 | ||||
| -rw-r--r-- | src/theory/quantifiers/candidate_generator.h | 42 | ||||
| -rwxr-xr-x | src/theory/quantifiers/full_model_check.cpp | 244 | ||||
| -rwxr-xr-x | src/theory/quantifiers/full_model_check.h | 16 | ||||
| -rw-r--r-- | src/theory/quantifiers/inst_match_generator.cpp | 146 | ||||
| -rw-r--r-- | src/theory/quantifiers/inst_match_generator.h | 4 | ||||
| -rw-r--r-- | src/theory/quantifiers/options | 2 | ||||
| -rwxr-xr-x | src/theory/quantifiers/rewrite_engine.cpp | 4 | ||||
| -rw-r--r-- | src/theory/quantifiers/trigger.cpp | 7 | ||||
| -rw-r--r-- | src/theory/rep_set.cpp | 7 | ||||
| -rw-r--r-- | src/theory/uf/options | 5 | ||||
| -rw-r--r-- | src/theory/uf/theory_uf_strong_solver.cpp | 94 | ||||
| -rw-r--r-- | src/theory/uf/theory_uf_strong_solver.h | 6 | ||||
| -rw-r--r-- | 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<Node> 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<minIndex) ){
minIndex = gindex;
@@ -81,6 +81,9 @@ void EntryTrie::addEntry( FirstOrderModelFmc * m, Node c, Node v, int data, int }
else {
d_child[ c[index] ].addEntry(m,c,v,data,index+1);
+ if( d_complete==0 ){
+ d_complete = -1;
+ }
}
}
@@ -111,36 +114,102 @@ void EntryTrie::getEntries( FirstOrderModelFmc * m, Node c, std::vector<int> & 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<int> compat;
- std::vector<int> gen;
- d_et.getEntries(m, c, compat, gen);
- for( unsigned i=0; i<compat.size(); i++) {
- if( d_status[compat[i]]==status_unk ){
- if( d_value[compat[i]]!=v ){
- d_status[compat[i]] = status_non_redundant;
+bool EntryTrie::isCovered(FirstOrderModelFmc * m, Node c, int index) {
+ if (index==(int)c.getNumChildren()) {
+ return false;
+ }else{
+ TypeNode tn = c[index].getType();
+ Node st = m->getStar(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<Node,EntryTrie>::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<gen.size(); i++) {
- if( d_status[gen[i]]==status_unk ){
- if( d_value[gen[i]]==v ){
- d_status[gen[i]] = status_redundant;
- }
+ if( complete ){
+ return true;
}
}
- d_status.push_back( status_unk );
}
- d_et.addEntry(m, c, v, newIndex);
- d_cond.push_back(c);
- d_value.push_back(v);
- return true;
+ if( d_child.find(c[index])!=d_child.end() ){
+ return d_child[c[index]].isCovered(m, c, index+1);
+ }else{
+ return false;
+ }
+ }
+}
+
+void EntryTrie::collectIndices(Node c, int index, std::vector< int >& indices ) {
+ if (index==(int)c.getNumChildren()) {
+ if( d_data!=-1 ){
+ indices.push_back( d_data );
+ }
}else{
+ for ( std::map<Node,EntryTrie>::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<int> compat;
+ std::vector<int> gen;
+ d_et.getEntries(m, c, compat, gen);
+ for( unsigned i=0; i<compat.size(); i++) {
+ if( d_status[compat[i]]==status_unk ){
+ if( d_value[compat[i]]!=v ){
+ d_status[compat[i]] = status_non_redundant;
+ }
+ }
+ }
+ for( unsigned i=0; i<gen.size(); i++) {
+ if( d_status[gen[i]]==status_unk ){
+ if( d_value[gen[i]]==v ){
+ d_status[gen[i]] = status_redundant;
+ }
+ }
+ }
+ d_status.push_back( status_unk );
+ }
+ d_et.addEntry(m, c, v, newIndex);
+ d_cond.push_back(c);
+ d_value.push_back(v);
+ return true;
}
Node Def::evaluate( FirstOrderModelFmc * m, std::vector<Node>& inst ) {
@@ -156,7 +225,7 @@ int Def::getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node>& 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; i<cc.getNumChildren(); i++ ){
+ if( !m->isStar(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<cond.size(); i++) {
+ addEntry(m, cond[i], 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;
+ }
+ }
+
+
+/*
+ //now do exhaustive covering simplification
+ if( options::fmfFmcCoverSimplify() && !d_cond.empty() ){
+ std::vector< int > 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<indices.size(); i++) {
+ Trace("fmc-cover-simplify") << indices[i] << " ";
+ }
+ 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;
+ for (unsigned i=0; i<cond.size(); i++) {
+ if( std::find( indices.begin(), indices.end(), i )==indices.end() ){
+ Node cc = cond[i];
+ if(star_replace.find(i)!=star_replace.end()) {
+ std::vector< Node > 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; i<tno.getNumChildren(); i++) {
TypeNode tn = tno[i];
if( fm->d_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<df.d_cond.size(); e++ ){
if ( entries.find(e)!=entries.end() ){
+ Trace("fmf-uf-process-debug") << "Add entry..." << std::endl;
d.addEntry(fm, entries[e], df.d_value[e] );
+ Trace("fmf-uf-process-debug") << "Done add entry." << std::endl;
}
}
}
diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h index c390c9437..3d9a82b9e 100755 --- a/src/theory/quantifiers/full_model_check.h +++ b/src/theory/quantifiers/full_model_check.h @@ -27,15 +27,24 @@ class FullModelChecker; class EntryTrie
{
+private:
+ int d_complete;
public:
- EntryTrie() : d_data(-1){}
+ EntryTrie() : d_complete(-1), d_data(-1){}
std::map<Node,EntryTrie> 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<Node> & inst, int index = 0 );
void getEntries( FirstOrderModelFmc * m, Node c, std::vector<int> & compat, std::vector<int> & 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<Node>& inst );
int getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node>& 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<Rational>() ); - 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; i<d_rr_quant.size(); i++ ) {
addedLemmas += checkRewriteRule( d_rr_quant[i] );
}
- Trace("rewrite-engine") << "Rewrite engine generated " << addedLemmas << " lemmas." << std::endl;
+ Trace("inst-engine") << "Rewrite engine added " << addedLemmas << " lemmas." << std::endl;
if (addedLemmas==0) {
}else{
//otherwise, the search will continue
@@ -85,7 +85,7 @@ int RewriteEngine::checkRewriteRule( Node f ) { bool trueInModel = false;
if( !trueInModel ){
- Trace("rewrite-engine-inst") << "Add instantiation : " << m << std::endl;
+ Trace("rewrite-engine-inst-debug") << "Add instantiation : " << m << std::endl;
if( d_quantEngine->addInstantiation( 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( varCount<f[0].getNumChildren() ){ + Trace("trigger-debug") << "Don't consider trigger since it does not contain all variables in " << f << std::endl; + for( unsigned i=0; i<nodes.size(); i++) { + Trace("trigger-debug") << nodes[i] << " "; + } + Trace("trigger-debug") << std::endl; + //do not generate multi-trigger if it does not contain all variables return NULL; }else{ diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index 99e28714f..f2cb22b85 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -295,11 +295,18 @@ void RepSetIterator::increment2( int counter ){ d_index.clear(); }else{ d_index[counter]++; + bool emptyDomain = false; for( int i=(int)d_index.size()-1; i>counter; 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; i<cardinality; i++ ){ - eqs.push_back( n.eqNode( getTotalityLemmaTerm( cardinality, i ) ) ); + if( std::find( d_totality_terms[0].begin(), d_totality_terms[0].end(), n )==d_totality_terms[0].end() ){ + if( std::find( d_totality_lems[n].begin(), d_totality_lems[n].end(), cardinality ) == d_totality_lems[n].end() ){ + d_totality_lems[n].push_back( cardinality ); + Node cardLit = d_cardinality_literal[ cardinality ]; + int sort_id = 0; + if( options::sortInference() ){ + sort_id = d_thss->getTheory()->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()<cardinality-1 ){ + use_cardinality = d_sym_break_terms[n.getType()][sort_id].size() + 1; + d_sym_break_terms[n.getType()][sort_id].push_back( n ); + d_sym_break_index[n] = use_cardinality; + Trace("uf-ss-totality") << "Allocate symmetry breaking term " << n << ", index = " << use_cardinality << std::endl; + } + } + + std::vector< Node > eqs; + for( int i=0; i<use_cardinality; i++ ){ + eqs.push_back( n.eqNode( getTotalityLemmaTerm( cardinality, i ) ) ); + } + 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 ); + } } - 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(); |