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() ){
}
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
Node getNextCandidate();
};/* class CandidateGeneratorQueue */
-class CandidateGeneratorQEDisequal;
-
+//the default generator
class CandidateGeneratorQE : public CandidateGenerator
{
friend class CandidateGeneratorQEDisequal;
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:
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 */
return true;\r
}\r
}\r
- if( d_child.find( c[index] )!=d_child.end() ){\r
+ if( c[index]!=st && d_child.find( c[index] )!=d_child.end() ){\r
if( d_child[ c[index] ].hasGeneralization(m, c, index+1) ){\r
return true;\r
}\r
minIndex = d_child[st].getGeneralizationIndex(m, inst, index+1);\r
}\r
Node cc = inst[index];\r
- if( d_child.find( cc )!=d_child.end() ){\r
+ if( cc!=st && d_child.find( cc )!=d_child.end() ){\r
int gindex = d_child[ cc ].getGeneralizationIndex(m, inst, index+1);\r
if (minIndex==-1 || (gindex!=-1 && gindex<minIndex) ){\r
minIndex = gindex;\r
}\r
else {\r
d_child[ c[index] ].addEntry(m,c,v,data,index+1);\r
+ if( d_complete==0 ){\r
+ d_complete = -1;\r
+ }\r
}\r
}\r
\r
}\r
\r
\r
-bool Def::addEntry( FirstOrderModelFmc * m, Node c, Node v) {\r
- if (!d_et.hasGeneralization(m, c)) {\r
- int newIndex = (int)d_cond.size();\r
- if (!d_has_simplified) {\r
- std::vector<int> compat;\r
- std::vector<int> gen;\r
- d_et.getEntries(m, c, compat, gen);\r
- for( unsigned i=0; i<compat.size(); i++) {\r
- if( d_status[compat[i]]==status_unk ){\r
- if( d_value[compat[i]]!=v ){\r
- d_status[compat[i]] = status_non_redundant;\r
+bool EntryTrie::isCovered(FirstOrderModelFmc * m, Node c, int index) {\r
+ if (index==(int)c.getNumChildren()) {\r
+ return false;\r
+ }else{\r
+ TypeNode tn = c[index].getType();\r
+ Node st = m->getStar(tn);\r
+ if( c[index]==st ){\r
+ //check if all children exist and are complete\r
+ int num_child_def = d_child.size() - (d_child.find(st)!=d_child.end() ? 1 : 0);\r
+ if( num_child_def==m->d_rep_set.getNumRepresentatives(tn) ){\r
+ bool complete = true;\r
+ for ( std::map<Node,EntryTrie>::iterator it = d_child.begin(); it != d_child.end(); ++it ){\r
+ if( !m->isStar(it->first) ){\r
+ if( !it->second.isComplete(m, c, index+1) ){\r
+ complete = false;\r
+ break;\r
+ }\r
}\r
}\r
- }\r
- for( unsigned i=0; i<gen.size(); i++) {\r
- if( d_status[gen[i]]==status_unk ){\r
- if( d_value[gen[i]]==v ){\r
- d_status[gen[i]] = status_redundant;\r
- }\r
+ if( complete ){\r
+ return true;\r
}\r
}\r
- d_status.push_back( status_unk );\r
}\r
- d_et.addEntry(m, c, v, newIndex);\r
- d_cond.push_back(c);\r
- d_value.push_back(v);\r
- return true;\r
+ if( d_child.find(c[index])!=d_child.end() ){\r
+ return d_child[c[index]].isCovered(m, c, index+1);\r
+ }else{\r
+ return false;\r
+ }\r
+ }\r
+}\r
+\r
+void EntryTrie::collectIndices(Node c, int index, std::vector< int >& indices ) {\r
+ if (index==(int)c.getNumChildren()) {\r
+ if( d_data!=-1 ){\r
+ indices.push_back( d_data );\r
+ }\r
}else{\r
+ for ( std::map<Node,EntryTrie>::iterator it = d_child.begin(); it != d_child.end(); ++it ){\r
+ it->second.collectIndices(c, index+1, indices );\r
+ }\r
+ }\r
+}\r
+\r
+bool EntryTrie::isComplete(FirstOrderModelFmc * m, Node c, int index) {\r
+ if( d_complete==-1 ){\r
+ d_complete = 1;\r
+ if (index<(int)c.getNumChildren()) {\r
+ Node st = m->getStar(c[index].getType());\r
+ if(d_child.find(st)!=d_child.end()) {\r
+ if (!d_child[st].isComplete(m, c, index+1)) {\r
+ d_complete = 0;\r
+ }\r
+ }else{\r
+ d_complete = 0;\r
+ }\r
+ }\r
+ }\r
+ return d_complete==1;\r
+}\r
+\r
+bool Def::addEntry( FirstOrderModelFmc * m, Node c, Node v) {\r
+ if (d_et.hasGeneralization(m, c)) {\r
return false;\r
}\r
+ if( options::fmfFmcCoverSimplify() ){\r
+ if( d_et.isCovered(m, c, 0) ){\r
+ Trace("fmc-cover-simplify") << "Entry " << c << " is covered." << std::endl;\r
+ return false;\r
+ }\r
+ }\r
+ int newIndex = (int)d_cond.size();\r
+ if (!d_has_simplified) {\r
+ std::vector<int> compat;\r
+ std::vector<int> gen;\r
+ d_et.getEntries(m, c, compat, gen);\r
+ for( unsigned i=0; i<compat.size(); i++) {\r
+ if( d_status[compat[i]]==status_unk ){\r
+ if( d_value[compat[i]]!=v ){\r
+ d_status[compat[i]] = status_non_redundant;\r
+ }\r
+ }\r
+ }\r
+ for( unsigned i=0; i<gen.size(); i++) {\r
+ if( d_status[gen[i]]==status_unk ){\r
+ if( d_value[gen[i]]==v ){\r
+ d_status[gen[i]] = status_redundant;\r
+ }\r
+ }\r
+ }\r
+ d_status.push_back( status_unk );\r
+ }\r
+ d_et.addEntry(m, c, v, newIndex);\r
+ d_cond.push_back(c);\r
+ d_value.push_back(v);\r
+ return true;\r
}\r
\r
Node Def::evaluate( FirstOrderModelFmc * m, std::vector<Node>& inst ) {\r
return d_et.getGeneralizationIndex(m, inst);\r
}\r
\r
-void Def::simplify(FirstOrderModelFmc * m) {\r
+void Def::basic_simplify( FirstOrderModelFmc * m ) {\r
d_has_simplified = true;\r
std::vector< Node > cond;\r
cond.insert( cond.end(), d_cond.begin(), d_cond.end() );\r
d_status.clear();\r
}\r
\r
+void Def::simplify(FullModelChecker * mc, FirstOrderModelFmc * m) {\r
+ basic_simplify( m );\r
+\r
+ //check if the last entry is not all star, if so, we can make the last entry all stars\r
+ if( !d_cond.empty() ){\r
+ bool last_all_stars = true;\r
+ Node cc = d_cond[d_cond.size()-1];\r
+ for( unsigned i=0; i<cc.getNumChildren(); i++ ){\r
+ if( !m->isStar(cc[i]) ){\r
+ last_all_stars = false;\r
+ break;\r
+ }\r
+ }\r
+ if( !last_all_stars ){\r
+ Trace("fmc-cover-simplify") << "Need to modify last entry to be all stars." << std::endl;\r
+ Trace("fmc-cover-simplify") << "Beforehand: " << std::endl;\r
+ debugPrint("fmc-cover-simplify",Node::null(), mc);\r
+ Trace("fmc-cover-simplify") << std::endl;\r
+ std::vector< Node > cond;\r
+ cond.insert( cond.end(), d_cond.begin(), d_cond.end() );\r
+ d_cond.clear();\r
+ std::vector< Node > value;\r
+ value.insert( value.end(), d_value.begin(), d_value.end() );\r
+ d_value.clear();\r
+ d_et.reset();\r
+ d_has_simplified = false;\r
+ //change the last to all star\r
+ std::vector< Node > nc;\r
+ nc.push_back( cc.getOperator() );\r
+ for( unsigned j=0; j< cc.getNumChildren(); j++){\r
+ nc.push_back(m->getStar(cc[j].getType()));\r
+ }\r
+ cond[cond.size()-1] = NodeManager::currentNM()->mkNode( APPLY_UF, nc );\r
+ //re-add the entries\r
+ for (unsigned i=0; i<cond.size(); i++) {\r
+ addEntry(m, cond[i], value[i]);\r
+ }\r
+ Trace("fmc-cover-simplify") << "Finished re-adding entries." << std::endl;\r
+ basic_simplify( m );\r
+ Trace("fmc-cover-simplify") << "Afterhand: " << std::endl;\r
+ debugPrint("fmc-cover-simplify",Node::null(), mc);\r
+ Trace("fmc-cover-simplify") << std::endl;\r
+ }\r
+ }\r
+\r
+\r
+/*\r
+ //now do exhaustive covering simplification\r
+ if( options::fmfFmcCoverSimplify() && !d_cond.empty() ){\r
+ std::vector< int > indices;\r
+ std::map< int, std::vector< int > > star_replace;\r
+ d_et.exhaustiveSimplify( m, d_cond[0], 0, indices, star_replace );\r
+ if( !indices.empty() ){\r
+ static bool appSimp = false;\r
+ if( !appSimp ){\r
+ appSimp = true;\r
+ std::cout << "FMC-CS" << std::endl;\r
+ }\r
+ Trace("fmc-cover-simplify") << "Beforehand: " << std::endl;\r
+ debugPrint("fmc-cover-simplify",Node::null(), mc);\r
+ Trace("fmc-cover-simplify") << std::endl;\r
+ d_has_simplified = false;\r
+ Trace("fmc-cover-simplify") << "By exhaustive covering, these indices can be removed : ";\r
+ for( unsigned i=0; i<indices.size(); i++) {\r
+ Trace("fmc-cover-simplify") << indices[i] << " ";\r
+ }\r
+ Trace("fmc-cover-simplify") << std::endl;\r
+ std::vector< Node > cond;\r
+ cond.insert( cond.end(), d_cond.begin(), d_cond.end() );\r
+ d_cond.clear();\r
+ std::vector< Node > value;\r
+ value.insert( value.end(), d_value.begin(), d_value.end() );\r
+ d_value.clear();\r
+ d_et.reset();\r
+ d_has_simplified = false;\r
+ for (unsigned i=0; i<cond.size(); i++) {\r
+ if( std::find( indices.begin(), indices.end(), i )==indices.end() ){\r
+ Node cc = cond[i];\r
+ if(star_replace.find(i)!=star_replace.end()) {\r
+ std::vector< Node > nc;\r
+ nc.push_back( cc.getOperator() );\r
+ Trace("fmc-cover-simplify") << "Modify entry : " << cc << std::endl;\r
+ for( unsigned j=0; j< cc.getNumChildren(); j++){\r
+ if( std::find( star_replace[i].begin(), star_replace[i].end(), j )!=star_replace[i].end() ){\r
+ nc.push_back( m->getStar(cc[j].getType()) );\r
+ }else{\r
+ nc.push_back( cc[j] );\r
+ }\r
+ }\r
+ cc = NodeManager::currentNM()->mkNode( APPLY_UF, nc );\r
+ Trace("fmc-cover-simplify") << "Got : " << cc << std::endl;\r
+ }\r
+ addEntry(m, cc, value[i]);\r
+ }\r
+ }\r
+ Trace("fmc-cover-simplify") << "Finished re-adding entries." << std::endl;\r
+ basic_simplify( m );\r
+ Trace("fmc-cover-simplify") << "Afterhand: " << std::endl;\r
+ debugPrint("fmc-cover-simplify",Node::null(), mc);\r
+ Trace("fmc-cover-simplify") << std::endl;\r
+ }\r
+ }\r
+ */\r
+}\r
+\r
void Def::debugPrint(const char * tr, Node op, FullModelChecker * m) {\r
if (!op.isNull()) {\r
Trace(tr) << "Model for " << op << " : " << std::endl;\r
for( unsigned i=0; i<tno.getNumChildren(); i++) {\r
TypeNode tn = tno[i];\r
if( fm->d_model_basis_rep.find( tn )==fm->d_model_basis_rep.end() ){\r
- Node mbn = d_qe->getTermDatabase()->getModelBasisTerm(tn);\r
- fm->d_model_basis_rep[tn] = fm->getUsedRepresentative( mbn );\r
+ Node mbn;\r
+ if (!fm->d_rep_set.hasType(tn)) {\r
+ mbn = fm->getSomeDomainElement(tn);\r
+ }else{\r
+ mbn = d_qe->getTermDatabase()->getModelBasisTerm(tn);\r
+ }\r
+ Node mbnr = fm->getUsedRepresentative( mbn );\r
+ fm->d_model_basis_rep[tn] = mbnr;\r
+ Trace("fmc") << "Add model basis for type " << tn << " : " << mbn << " " << mbnr << std::endl;\r
}\r
}\r
}\r
fm->d_models[op]->debugPrint("fmc-model", op, this);\r
Trace("fmc-model") << std::endl;\r
\r
- fm->d_models[op]->simplify( fm );\r
+ Trace("fmc-model-simplify") << "Simplifying " << op << "..." << std::endl;\r
+ fm->d_models[op]->simplify( this, fm );\r
Trace("fmc-model-simplify") << "After simplification : " << std::endl;\r
fm->d_models[op]->debugPrint("fmc-model-simplify", op, this);\r
Trace("fmc-model-simplify") << std::endl;\r
doInterpretedCompose( fm, f, d, n, children, 0, cond, val );\r
}\r
}\r
- d.simplify(fm);\r
+ Trace("fmc-debug") << "Simplify the definition..." << std::endl;\r
+ d.simplify(this, fm);\r
+ Trace("fmc-debug") << "Done simplifying" << std::endl;\r
}\r
Trace("fmc-debug") << "Definition for " << n << " is : " << std::endl;\r
d.debugPrint("fmc-debug", Node::null(), this);\r
//add them to the definition\r
for( unsigned e=0; e<df.d_cond.size(); e++ ){\r
if ( entries.find(e)!=entries.end() ){\r
+ Trace("fmf-uf-process-debug") << "Add entry..." << std::endl;\r
d.addEntry(fm, entries[e], df.d_value[e] );\r
+ Trace("fmf-uf-process-debug") << "Done add entry." << std::endl;\r
}\r
}\r
}\r
\r
class EntryTrie\r
{\r
+private:\r
+ int d_complete;\r
public:\r
- EntryTrie() : d_data(-1){}\r
+ EntryTrie() : d_complete(-1), d_data(-1){}\r
std::map<Node,EntryTrie> d_child;\r
int d_data;\r
- void reset() { d_data = -1; d_child.clear(); }\r
+ void reset() { d_data = -1; d_child.clear(); d_complete = -1; }\r
void addEntry( FirstOrderModelFmc * m, Node c, Node v, int data, int index = 0 );\r
bool hasGeneralization( FirstOrderModelFmc * m, Node c, int index = 0 );\r
int getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node> & inst, int index = 0 );\r
void getEntries( FirstOrderModelFmc * m, Node c, std::vector<int> & compat, std::vector<int> & gen, int index = 0, bool is_gen = true );\r
+\r
+ bool isCovered(FirstOrderModelFmc * m, Node c, int index);\r
+\r
+ //void exhaustiveSimplify( FirstOrderModelFmc * m, Node c, int index, std::vector< int >& indices,\r
+ // std::map< int, std::vector< int > >& star_replace );\r
+ void collectIndices(Node c, int index, std::vector< int >& indices );\r
+ bool isComplete(FirstOrderModelFmc * m, Node c, int index);\r
};\r
\r
\r
std::vector< Node > d_cond;\r
//value is returned by FullModelChecker::getRepresentative\r
std::vector< Node > d_value;\r
+ void basic_simplify( FirstOrderModelFmc * m );\r
private:\r
enum {\r
status_unk,\r
bool addEntry( FirstOrderModelFmc * m, Node c, Node v);\r
Node evaluate( FirstOrderModelFmc * m, std::vector<Node>& inst );\r
int getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node>& inst );\r
- void simplify( FirstOrderModelFmc * m );\r
+ void simplify( FullModelChecker * mc, FirstOrderModelFmc * m );\r
void debugPrint(const char * tr, Node op, FullModelChecker * m);\r
};\r
\r
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]) ){
}
}
- 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 ){
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{
}
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;
}
}
-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();
}
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;
}
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 );
}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 );
}
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.
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
for( unsigned i=0; i<d_rr_quant.size(); i++ ) {\r
addedLemmas += checkRewriteRule( d_rr_quant[i] );\r
}\r
- Trace("rewrite-engine") << "Rewrite engine generated " << addedLemmas << " lemmas." << std::endl;\r
+ Trace("inst-engine") << "Rewrite engine added " << addedLemmas << " lemmas." << std::endl;\r
if (addedLemmas==0) {\r
}else{\r
//otherwise, the search will continue\r
bool trueInModel = false;\r
\r
if( !trueInModel ){\r
- Trace("rewrite-engine-inst") << "Add instantiation : " << m << std::endl;\r
+ Trace("rewrite-engine-inst-debug") << "Add instantiation : " << m << std::endl;\r
if( d_quantEngine->addInstantiation( f, m ) ){\r
addedLemmas++;\r
Trace("rewrite-engine-inst-debug") << "success" << std::endl;\r
qe->getTermDatabase()->registerTrigger( this, d_nodes[i].getOperator() );
}
}
+ Trace("trigger-debug") << "Finished making trigger." << std::endl;
}
void Trigger::resetInstantiationRound(){
}
}
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{
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();
+ }
}
}
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
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
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;
//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
+ }
}
}
}
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
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;
}
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") << " ";
}
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 */
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 {
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 );
};
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();
projects / cvc5.git / commitdiff