* Refactor theory model, working on making RepSet references const.
* Encapsulation of members of rep set.
* More documentation on rep set.
* Swap names
* Reference issues.
* Minor
* Minor
* New clang format.
const theory::TheoryModel& tm = (const theory::TheoryModel&) m;
if(dynamic_cast<const DeclareTypeCommand*>(c) != NULL) {
TypeNode tn = TypeNode::fromType( ((const DeclareTypeCommand*)c)->getType() );
- if( options::modelUninterpDtEnum() && tn.isSort() &&
- tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
- out << "DATATYPE" << std::endl;
- out << " " << dynamic_cast<const DeclareTypeCommand*>(c)->getSymbol() << " = ";
- for( size_t i=0; i<(*tm.d_rep_set.d_type_reps.find(tn)).second.size(); i++ ){
- if (i>0) {
- out << "| ";
+ if (options::modelUninterpDtEnum() && tn.isSort())
+ {
+ const theory::RepSet* rs = tm.getRepSet();
+ if (rs->d_type_reps.find(tn) != rs->d_type_reps.end())
+ {
+ out << "DATATYPE" << std::endl;
+ out << " " << dynamic_cast<const DeclareTypeCommand*>(c)->getSymbol()
+ << " = ";
+ for (size_t i = 0; i < (*rs->d_type_reps.find(tn)).second.size(); i++)
+ {
+ if (i > 0)
+ {
+ out << "| ";
+ }
+ out << (*rs->d_type_reps.find(tn)).second[i] << " ";
}
- out << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << " ";
+ out << std::endl << "END;" << std::endl;
}
- out << std::endl << "END;" << std::endl;
- } else {
- if( tn.isSort() ){
- // print the cardinality
- if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
- out << "% cardinality of " << tn << " is " << (*tm.d_rep_set.d_type_reps.find(tn)).second.size() << std::endl;
+ else
+ {
+ if (tn.isSort())
+ {
+ // print the cardinality
+ if (rs->d_type_reps.find(tn) != rs->d_type_reps.end())
+ {
+ out << "% cardinality of " << tn << " is "
+ << (*rs->d_type_reps.find(tn)).second.size() << std::endl;
+ }
}
- }
- out << c << std::endl;
- if( tn.isSort() ){
- // print the representatives
- if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
- for( size_t i=0; i<(*tm.d_rep_set.d_type_reps.find(tn)).second.size(); i++ ){
- if( (*tm.d_rep_set.d_type_reps.find(tn)).second[i].isVar() ){
- out << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << " : " << tn << ";" << std::endl;
- }else{
- out << "% rep: " << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << std::endl;
+ out << c << std::endl;
+ if (tn.isSort())
+ {
+ // print the representatives
+ if (rs->d_type_reps.find(tn) != rs->d_type_reps.end())
+ {
+ for (size_t i = 0; i < (*rs->d_type_reps.find(tn)).second.size();
+ i++)
+ {
+ if ((*rs->d_type_reps.find(tn)).second[i].isVar())
+ {
+ out << (*rs->d_type_reps.find(tn)).second[i] << " : " << tn
+ << ";" << std::endl;
+ }
+ else
+ {
+ out << "% rep: " << (*rs->d_type_reps.find(tn)).second[i]
+ << std::endl;
+ }
}
}
}
}
Node val = Node::fromExpr(tm.getSmtEngine()->getValue(n.toExpr()));
if( options::modelUninterpDtEnum() && val.getKind() == kind::STORE ) {
+ const theory::RepSet* rs = tm.getRepSet();
TypeNode tn = val[1].getType();
- if (tn.isSort() && tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
- Cardinality indexCard((*tm.d_rep_set.d_type_reps.find(tn)).second.size());
+ if (tn.isSort() && rs->d_type_reps.find(tn) != rs->d_type_reps.end())
+ {
+ Cardinality indexCard((*rs->d_type_reps.find(tn)).second.size());
val = theory::arrays::TheoryArraysRewriter::normalizeConstant( val, indexCard );
}
}
const theory::TheoryModel& tm = (const theory::TheoryModel&) m;
if(dynamic_cast<const DeclareTypeCommand*>(c) != NULL) {
TypeNode tn = TypeNode::fromType( ((const DeclareTypeCommand*)c)->getType() );
- const std::map< TypeNode, std::vector< Node > >& type_reps = tm.d_rep_set.d_type_reps;
+ const theory::RepSet* rs = tm.getRepSet();
+ const std::map<TypeNode, std::vector<Node> >& type_reps = rs->d_type_reps;
std::map< TypeNode, std::vector< Node > >::const_iterator tn_iterator = type_reps.find( tn );
if( options::modelUninterpDtEnum() && tn.isSort() && tn_iterator != type_reps.end() ){
} else {
if( options::modelUninterpDtEnum() && val.getKind() == kind::STORE ) {
TypeNode tn = val[1].getType();
- if (tn.isSort() && tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
- Cardinality indexCard((*tm.d_rep_set.d_type_reps.find(tn)).second.size());
+ const theory::RepSet* rs = tm.getRepSet();
+ if (tn.isSort() && rs->d_type_reps.find(tn) != rs->d_type_reps.end())
+ {
+ Cardinality indexCard((*rs->d_type_reps.find(tn)).second.size());
val = theory::arrays::TheoryArraysRewriter::normalizeConstant( val, indexCard );
}
}
//construct children
for( std::map< unsigned, std::vector< TNode > >::iterator it = fapp_child.begin(); it != fapp_child.end(); ++it ){
Trace("abs-model-debug") << "Construct " << it->first << " : " << fapp_child_index[it->first] << " : ";
- debugPrintUInt( "abs-model-debug", m->d_rep_set.d_type_reps[tn].size(), fapp_child_index[it->first] );
+ const RepSet* rs = m->getRepSet();
+ debugPrintUInt("abs-model-debug",
+ rs->getNumRepresentatives(tn),
+ fapp_child_index[it->first]);
Trace("abs-model-debug") << " : " << it->second.size() << " terms." << std::endl;
d_def[fapp_child_index[it->first]].construct_func( m, it->second, depth+1 );
}
Trace(c) << "V[" << d_value << "]" << std::endl;
}else{
TypeNode tn = f[depth].getType();
- unsigned dSize = m->d_rep_set.getNumRepresentatives( tn );
+ const RepSet* rs = m->getRepSet();
+ unsigned dSize = rs->getNumRepresentatives(tn);
Assert( dSize<32 );
for( std::map< unsigned, AbsDef >::const_iterator it = d_def.begin(); it != d_def.end(); ++it ){
for( unsigned i=0; i<depth; i++ ){ Trace(c) << " ";}
success = false;
index = getId( it->first, index );
if( index<32 ){
- Assert( index<m->d_rep_set.d_type_reps[tn].size() );
- terms[m->d_var_order[q][depth]] = m->d_rep_set.d_type_reps[tn][index];
- //terms[depth] = m->d_rep_set.d_type_reps[tn][index];
+ const RepSet* rs = m->getRepSet();
+ Assert(index < rs->getNumRepresentatives(tn));
+ terms[m->d_var_order[q][depth]] =
+ rs->getRepresentative(tn, index);
if( !it->second.addInstantiations( m, qe, q, terms, inst, depth+1 ) && inst==0 ){
//if we are incomplete, and have not yet added an instantiation, keep trying
index++;
if( depth==terms.size() ){
if( Trace.isOn("ambqi-check-debug2") ){
Trace("ambqi-check-debug2") << "Add entry ( ";
+ const RepSet* rs = m->getRepSet();
for( unsigned i=0; i<entry.size(); i++ ){
- unsigned dSize = m->d_rep_set.d_type_reps[m->getVariable( q, i ).getType()].size();
+ unsigned dSize =
+ rs->getNumRepresentatives(m->getVariable(q, i).getType());
debugPrintUInt( "ambqi-check-debug2", dSize, entry[i] );
Trace("ambqi-check-debug2") << " ";
}
}else{
Assert( currv==val_none );
if( curr==val_none ){
- unsigned numReps = m->d_rep_set.getNumRepresentatives( tn );
+ unsigned numReps = m->getRepSet()->getNumRepresentatives(tn);
Assert( numReps < 32 );
for( unsigned i=0; i<numReps; i++ ){
curr = 1 << i;
}else{
TypeNode tn = m->getVariable( q, depth ).getType();
if( v==depth ){
- unsigned numReps = m->d_rep_set.d_type_reps[tn].size();
+ unsigned numReps = m->getRepSet()->getNumRepresentatives(tn);
Assert( numReps>0 && numReps < 32 );
for( unsigned i=0; i<numReps; i++ ){
d_def[ 1 << i ].construct_var( m, q, v, i, depth+1 );
std::map< unsigned, AbsDef * >& children,
std::map< unsigned, int >& bchildren, std::map< unsigned, int >& vchildren,
std::vector< unsigned >& entry, std::vector< bool >& entry_def ) {
+ const RepSet* rs = m->getRepSet();
if( n.getKind()==OR || n.getKind()==AND ){
// short circuiting
for( std::map< unsigned, AbsDef * >::iterator it = children.begin(); it != children.end(); ++it ){
for( std::map< unsigned, AbsDef * >::iterator it = children.begin(); it != children.end(); ++it ){
Trace("ambqi-check-debug2") << "composite : " << it->first << " : " << it->second->d_value;
if( it->second->d_value>=0 ){
- if( it->second->d_value>=(int)m->d_rep_set.d_type_reps[n[it->first].getType()].size() ){
- std::cout << it->second->d_value << " " << n[it->first] << " " << n[it->first].getType() << " " << m->d_rep_set.d_type_reps[n[it->first].getType()].size() << std::endl;
+ if (it->second->d_value
+ >= (int)rs->getNumRepresentatives(n[it->first].getType()))
+ {
+ std::cout << it->second->d_value << " " << n[it->first] << " "
+ << n[it->first].getType() << " "
+ << rs->getNumRepresentatives(n[it->first].getType())
+ << std::endl;
}
- Assert( it->second->d_value<(int)m->d_rep_set.d_type_reps[n[it->first].getType()].size() );
- values[it->first] = m->d_rep_set.d_type_reps[n[it->first].getType()][it->second->d_value];
+ Assert(it->second->d_value
+ < (int)rs->getNumRepresentatives(n[it->first].getType()));
+ values[it->first] = rs->getRepresentative(n[it->first].getType(),
+ it->second->d_value);
}else{
incomplete = true;
}
for( std::map< unsigned, int >::iterator it = bchildren.begin(); it != bchildren.end(); ++it ){
Trace("ambqi-check-debug2") << " basic : " << it->first << " : " << it->second;
if( it->second>=0 ){
- Assert( it->second<(int)m->d_rep_set.d_type_reps[n[it->first].getType()].size() );
- values[it->first] = m->d_rep_set.d_type_reps[n[it->first].getType()][it->second];
+ Assert(it->second
+ < (int)rs->getNumRepresentatives(n[it->first].getType()));
+ values[it->first] =
+ rs->getRepresentative(n[it->first].getType(), it->second);
}else{
incomplete = true;
}
if( Trace.isOn("ambqi-check-debug2") ){
for( unsigned i=0; i<entry.size(); i++ ){ Trace("ambqi-check-debug2") << " "; }
Trace("ambqi-check-debug2") << "...process : ";
- debugPrintUInt("ambqi-check-debug2", m->d_rep_set.d_type_reps[tn].size(), itd->first );
+ debugPrintUInt("ambqi-check-debug2",
+ rs->getNumRepresentatives(tn),
+ itd->first);
Trace("ambqi-check-debug2") << " " << children.size() << " " << cchildren.size() << std::endl;
}
entry.push_back( itd->first );
if( Trace.isOn("ambqi-check-debug2") ){
for( unsigned i=0; i<entry.size(); i++ ){ Trace("ambqi-check-debug2") << " "; }
Trace("ambqi-check-debug2") << "...process default : ";
- debugPrintUInt("ambqi-check-debug2", m->d_rep_set.getNumRepresentatives( tn ), def );
+ debugPrintUInt(
+ "ambqi-check-debug2", rs->getNumRepresentatives(tn), def);
Trace("ambqi-check-debug2") << " " << children.size() << " " << cdchildren.size() << std::endl;
}
entry.push_back( def );
}
Node AbsDef::getFunctionValue( FirstOrderModelAbs * m, TNode op, std::vector< Node >& vars, unsigned depth ) {
+ const RepSet* rs = m->getRepSet();
if( depth==vars.size() ){
TypeNode tn = op.getType();
if( tn.getNumChildren()>0 ){
tn = tn[tn.getNumChildren() - 1];
}
if( d_value>=0 ){
- Assert( d_value<(int)m->d_rep_set.d_type_reps[tn].size() );
+ Assert(d_value < (int)rs->getNumRepresentatives(tn));
if( tn.isBoolean() ){
return NodeManager::currentNM()->mkConst( d_value==1 );
}else{
- return m->d_rep_set.d_type_reps[tn][d_value];
+ return rs->getRepresentative(tn, d_value);
}
}else{
return Node::null();
for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){
if( it->first!=d_default ){
unsigned id = getId( it->first );
- Assert( id<m->d_rep_set.d_type_reps[tn].size() );
- TNode n = m->d_rep_set.d_type_reps[tn][id];
+ Assert(id < rs->getNumRepresentatives(tn));
+ TNode n = rs->getRepresentative(tn, id);
Node fv = it->second.getFunctionValue( m, op, vars, depth+1 );
if( !curr.isNull() && !fv.isNull() ){
curr = NodeManager::currentNM()->mkNode( ITE, vars[depth].eqNode( n ), fv, curr );
if( d_value==val_unk ){
return Node::null();
}else{
- Assert( d_value>=0 && d_value<(int)m->d_rep_set.d_type_reps[retTyp].size() );
- return m->d_rep_set.d_type_reps[retTyp][d_value];
+ const RepSet* rs = m->getRepSet();
+ Assert(d_value >= 0 && d_value < (int)rs->getNumRepresentatives(retTyp));
+ return rs->getRepresentative(retTyp, d_value);
}
}else{
std::map< unsigned, AbsDef >::iterator it = d_def.find( iargs[depth] );
Trace("ambqi-debug") << "process build model " << std::endl;
FirstOrderModel* f = (FirstOrderModel*)m;
FirstOrderModelAbs* fm = f->asFirstOrderModelAbs();
+ RepSet* rs = m->getRepSetPtr();
fm->initialize();
//process representatives
fm->d_rep_id.clear();
//initialize boolean sort
TypeNode b = d_true.getType();
- fm->d_rep_set.d_type_reps[b].clear();
- fm->d_rep_set.d_type_reps[b].push_back( d_false );
- fm->d_rep_set.d_type_reps[b].push_back( d_true );
+ rs->d_type_reps[b].clear();
+ rs->d_type_reps[b].push_back(d_false);
+ rs->d_type_reps[b].push_back(d_true);
fm->d_rep_id[d_false] = 0;
fm->d_rep_id[d_true] = 1;
//initialize unintpreted sorts
Trace("ambqi-model") << std::endl << "Making representatives..." << std::endl;
- for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin();
- it != fm->d_rep_set.d_type_reps.end(); ++it ){
+ for (std::map<TypeNode, std::vector<Node> >::iterator it =
+ rs->d_type_reps.begin();
+ it != rs->d_type_reps.end();
+ ++it)
+ {
if( it->first.isSort() ){
Assert( !it->second.empty() );
//set the domain
Assert( q[0][v]==d_set[q][i] );
Node t = rsi->getCurrentTerm( v );
Trace("bound-int-rsi") << "term : " << t << std::endl;
- if( rsi->d_rep_set->d_values_to_terms.find( t )!=rsi->d_rep_set->d_values_to_terms.end() ){
- t = rsi->d_rep_set->d_values_to_terms[t];
+ Node tt = rsi->d_rep_set->getTermForRepresentative(t);
+ if (!tt.isNull())
+ {
+ t = tt;
Trace("bound-int-rsi") << "term (post-rep) : " << t << std::endl;
}
vars.push_back( d_set[q][i] );
if( r.isConst() && quantifiers::TermUtil::containsUninterpretedConstant( r ) ){
//map back from values assigned by model, if any
if( d_qe->getModel() ){
- std::map< Node, Node >::iterator it = d_qe->getModel()->d_rep_set.d_values_to_terms.find( r );
- if( it!=d_qe->getModel()->d_rep_set.d_values_to_terms.end() ){
- r = it->second;
+ Node tr = d_qe->getModel()->getRepSet()->getTermForRepresentative(r);
+ if (!tr.isNull())
+ {
+ r = tr;
r = getRepresentative( r );
}else{
if( r.getType().isSort() ){
//for star: check if all children are defined and have generalizations
if( c[index]==st ){ ///options::fmfFmcCoverSimplify()
//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) ){
+ unsigned num_child_def =
+ d_child.size() - (d_child.find(st) != d_child.end() ? 1 : 0);
+ if (num_child_def == m->getRepSet()->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) ){
d_rep_ids.clear();
d_star_insts.clear();
//process representatives
- for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin();
- it != fm->d_rep_set.d_type_reps.end(); ++it ){
+ RepSet* rs = fm->getRepSetPtr();
+ for (std::map<TypeNode, std::vector<Node> >::iterator it =
+ rs->d_type_reps.begin();
+ it != rs->d_type_reps.end();
+ ++it)
+ {
if( it->first.isSort() ){
Trace("fmc") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
for( size_t a=0; a<it->second.size(); a++ ){
}else{
Node vmb = getSomeDomainElement(fm, nmb.getType());
Trace("fmc-model-debug") << "Add default to default representative " << nmb << " ";
- Trace("fmc-model-debug") << fm->d_rep_set.d_type_reps[nmb.getType()].size() << std::endl;
+ Trace("fmc-model-debug")
+ << fm->getRepSet()->getNumRepresentatives(nmb.getType())
+ << std::endl;
add_conds.push_back( nmb );
add_values.push_back( vmb );
}
if( tn.isSort() ){
int j = fm->getVariableId(f, eq[0]);
int k = fm->getVariableId(f, eq[1]);
- if( !fm->d_rep_set.hasType( tn ) ){
+ const RepSet* rs = fm->getRepSet();
+ if (!rs->hasType(tn))
+ {
getSomeDomainElement( fm, tn ); //to verify the type is initialized
}
- for (unsigned i=0; i<fm->d_rep_set.d_type_reps[tn].size(); i++) {
- Node r = fm->getRepresentative( fm->d_rep_set.d_type_reps[tn][i] );
+ unsigned nreps = rs->getNumRepresentatives(tn);
+ for (unsigned i = 0; i < nreps; i++)
+ {
+ Node r = fm->getRepresentative(rs->getRepresentative(tn, i));
cond[j+1] = r;
cond[k+1] = r;
d.addEntry( fm, mkCond(cond), d_true);
}
Node FullModelChecker::getSomeDomainElement( FirstOrderModelFmc * fm, TypeNode tn ) {
- bool addRepId = !fm->d_rep_set.hasType( tn );
+ bool addRepId = !fm->getRepSet()->hasType(tn);
Node de = fm->getSomeDomainElement(tn);
if( addRepId ){
d_rep_ids[tn][de] = 0;
FirstOrderModel * fm = (FirstOrderModel*)m;
//traverse equality engine
std::map< TypeNode, bool > eqc_usort;
- eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( fm->d_equalityEngine );
+ eq::EqClassesIterator eqcs_i =
+ eq::EqClassesIterator(fm->getEqualityEngine());
while( !eqcs_i.isFinished() ){
TypeNode tr = (*eqcs_i).getType();
eqc_usort[tr] = true;
for( unsigned j=0; j<f[0].getNumChildren(); j++ ){
vars.push_back( f[0][j] );
}
- RepSetIterator riter( d_qe, &(fm->d_rep_set) );
+ RepSetIterator riter(d_qe, fm->getRepSetPtr());
if( riter.setQuantifier( f ) ){
while( !riter.isFinished() ){
tests++;
}
Node n = d_qe->getInstantiation( f, vars, terms );
Node val = fm->getValue( n );
- if( val!=fm->d_true ){
+ if (val != d_qe->getTermUtil()->d_true)
+ {
Trace("quant-check-model") << "******* Instantiation " << n << " for " << std::endl;
Trace("quant-check-model") << " " << f << std::endl;
Trace("quant-check-model") << " Evaluates to " << val << std::endl;
//do exhaustive instantiation
int QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) {
if( optUseModel() ){
- RepSetIterator riter( d_qe, &(d_qe->getModel()->d_rep_set) );
+ RepSetIterator riter(d_qe, d_qe->getModel()->getRepSetPtr());
if( riter.setQuantifier( f ) ){
FirstOrderModelIG * fmig = (FirstOrderModelIG*)d_qe->getModel();
Debug("inst-fmf-ei") << "Reset evaluate..." << std::endl;
std::vector< Node > tr_terms;
if( lit.getKind()==APPLY_UF ){
//only match predicates that are contrary to this one, use literal matching
- Node eq = NodeManager::currentNM()->mkNode( EQUAL, lit, !phase ? fm->d_true : fm->d_false );
+ Node eq = NodeManager::currentNM()->mkNode(
+ EQUAL, lit, NodeManager::currentNM()->mkConst(!phase));
tr_terms.push_back( eq );
}else if( lit.getKind()==EQUAL ){
//collect trigger terms
Node n = itut->second[i];
// only consider unique up to congruence (in model equality engine)?
Node v = fmig->getRepresentative( n );
- Trace("fmf-model-cons") << "Set term " << n << " : " << fmig->d_rep_set.getIndexFor( v ) << " " << v << std::endl;
+ Trace("fmf-model-cons") << "Set term " << n << " : "
+ << fmig->getRepSet()->getIndexFor(v) << " " << v
+ << std::endl;
//if this assertion did not help the model, just consider it ground
//set n = v in the model tree
//set it as ground value
//chose defaultVal based on heuristic, currently the best ratio of "pro" responses
Node defaultVal = d_uf_prefs[op].getBestDefaultValue( defaultTerm, fm );
if( defaultVal.isNull() ){
- if (!fmig->d_rep_set.hasType(defaultTerm.getType())) {
+ if (!fmig->getRepSet()->hasType(defaultTerm.getType()))
+ {
Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(defaultTerm.getType());
- fmig->d_rep_set.d_type_reps[defaultTerm.getType()].push_back(mbt);
+ fmig->getRepSetPtr()->d_type_reps[defaultTerm.getType()].push_back(
+ mbt);
}
- defaultVal = fmig->d_rep_set.d_type_reps[defaultTerm.getType()][0];
+ defaultVal =
+ fmig->getRepSet()->getRepresentative(defaultTerm.getType(), 0);
}
Assert( !defaultVal.isNull() );
- Trace("fmf-model-cons") << "Set default term : " << fmig->d_rep_set.getIndexFor( defaultVal ) << std::endl;
+ Trace("fmf-model-cons")
+ << "Set default term : " << fmig->getRepSet()->getIndexFor(defaultVal)
+ << std::endl;
fmig->d_uf_model_gen[op].setValue( fm, defaultTerm, defaultVal, false );
}
Debug("fmf-model-cons") << " Making model...";
//flatten the representatives
//Trace("model-engine-debug") << "Flattening representatives...." << std::endl;
- //d_quantEngine->getEqualityQuery()->flattenRepresentatives( fm->d_rep_set.d_type_reps );
+ // d_quantEngine->getEqualityQuery()->flattenRepresentatives(
+ // fm->getRepSet()->d_type_reps );
//for debugging, setup
- for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin();
- it != fm->d_rep_set.d_type_reps.end(); ++it ){
+ for (std::map<TypeNode, std::vector<Node> >::iterator it =
+ fm->getRepSetPtr()->d_type_reps.begin();
+ it != fm->getRepSetPtr()->d_type_reps.end();
+ ++it)
+ {
if( it->first.isSort() ){
Trace("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
Trace("model-engine-debug") << " Reps : ";
int totalInst = 1;
for( unsigned j=0; j<f[0].getNumChildren(); j++ ){
TypeNode tn = f[0][j].getType();
- if( fm->d_rep_set.hasType( tn ) ){
- totalInst = totalInst * (int)fm->d_rep_set.d_type_reps[ tn ].size();
+ if (fm->getRepSet()->hasType(tn))
+ {
+ totalInst =
+ totalInst * (int)fm->getRepSet()->getNumRepresentatives(tn);
}
}
d_totalLemmas += totalInst;
Trace("fmf-exh-inst-debug") << std::endl;
}
//create a rep set iterator and iterate over the (relevant) domain of the quantifier
- RepSetIterator riter( d_quantEngine, &(d_quantEngine->getModel()->d_rep_set) );
+ RepSetIterator riter(d_quantEngine,
+ d_quantEngine->getModel()->getRepSetPtr());
if( riter.setQuantifier( f ) ){
Trace("fmf-exh-inst") << "...exhaustive instantiation set, incomplete=" << riter.isIncomplete() << "..." << std::endl;
if( !riter.isIncomplete() ){
eq::EqualityEngine* QuantifiersEngine::getActiveEqualityEngine() {
if( d_useModelEe ){
- return d_model->d_equalityEngine;
+ return d_model->getEqualityEngine();
}else{
return d_te->getMasterEqualityEngine();
}
** \brief Implementation of representative set
**/
+#include <unordered_set>
+
#include "theory/rep_set.h"
#include "theory/type_enumerator.h"
#include "theory/quantifiers/bounded_integers.h"
d_values_to_terms.clear();
}
-bool RepSet::hasRep( TypeNode tn, Node n ) {
- std::map< TypeNode, std::vector< Node > >::iterator it = d_type_reps.find( tn );
+bool RepSet::hasRep(TypeNode tn, Node n) const
+{
+ std::map<TypeNode, std::vector<Node> >::const_iterator it =
+ d_type_reps.find(tn);
if( it==d_type_reps.end() ){
return false;
}else{
}
}
-int RepSet::getNumRepresentatives( TypeNode tn ) const{
+unsigned RepSet::getNumRepresentatives(TypeNode tn) const
+{
std::map< TypeNode, std::vector< Node > >::const_iterator it = d_type_reps.find( tn );
if( it!=d_type_reps.end() ){
- return (int)it->second.size();
+ return it->second.size();
}else{
return 0;
}
}
-bool containsStoreAll( Node n, std::vector< Node >& cache ){
+Node RepSet::getRepresentative(TypeNode tn, unsigned i) const
+{
+ std::map<TypeNode, std::vector<Node> >::const_iterator it =
+ d_type_reps.find(tn);
+ Assert(it != d_type_reps.end());
+ Assert(i < it->second.size());
+ return it->second[i];
+}
+
+bool containsStoreAll(Node n, std::unordered_set<Node, NodeHashFunction>& cache)
+{
if( std::find( cache.begin(), cache.end(), n )==cache.end() ){
- cache.push_back( n );
+ cache.insert(n);
if( n.getKind()==STORE_ALL ){
return true;
}else{
void RepSet::add( TypeNode tn, Node n ){
//for now, do not add array constants FIXME
if( tn.isArray() ){
- std::vector< Node > cache;
+ std::unordered_set<Node, NodeHashFunction> cache;
if( containsStoreAll( n, cache ) ){
return;
}
}
}
+Node RepSet::getTermForRepresentative(Node n) const
+{
+ std::map<Node, Node>::const_iterator it = d_values_to_terms.find(n);
+ if (it != d_values_to_terms.end())
+ {
+ return it->second;
+ }
+ else
+ {
+ return Node::null();
+ }
+}
+
+void RepSet::setTermForRepresentative(Node n, Node t)
+{
+ d_values_to_terms[n] = t;
+}
+
+Node RepSet::getDomainValue(TypeNode tn, const std::vector<Node>& exclude) const
+{
+ std::map<TypeNode, std::vector<Node> >::const_iterator it =
+ d_type_reps.find(tn);
+ if (it != d_type_reps.end())
+ {
+ // try to find a pre-existing arbitrary element
+ for (size_t i = 0; i < it->second.size(); i++)
+ {
+ if (std::find(exclude.begin(), exclude.end(), it->second[i])
+ == exclude.end())
+ {
+ return it->second[i];
+ }
+ }
+ }
+ return Node::null();
+}
+
void RepSet::toStream(std::ostream& out){
for( std::map< TypeNode, std::vector< Node > >::iterator it = d_type_reps.begin(); it != d_type_reps.end(); ++it ){
if( !it->first.isFunction() && !it->first.isPredicate() ){
#ifndef __CVC4__THEORY__REP_SET_H
#define __CVC4__THEORY__REP_SET_H
-#include "expr/node.h"
#include <map>
+#include <vector>
+
+#include "expr/node.h"
+#include "expr/type_node.h"
namespace CVC4 {
namespace theory {
class QuantifiersEngine;
-/** this class stores a representative set */
+/** representative set
+ *
+ * This class contains finite lists of values for types, typically values and
+ * types that exist
+ * in the equality engine of a model object. In the following, "representative"
+ * means a value that exists in this set.
+ *
+ * This class is used for finite model finding and other exhaustive
+ * instantiation-based
+ * methods. The class goes beyond just maintaining a list of values that occur
+ * in the equality engine in the following ways:
+
+ * (1) It maintains a partial mapping from representatives to a term that has
+ * that value in the current
+ * model. This is important because algorithms like the instantiation method in
+ * Reynolds et al CADE 2013
+ * act on "term models" where domains in models are interpreted as a set of
+ * representative terms. Hence,
+ * instead of instantiating with e.g. uninterpreted constants u, we instantiate
+ * with the corresponding term that is interpreted as u.
+
+ * (2) It is mutable, calls to add(...) and complete(...) may modify this class
+ * as necessary, for instance
+ * in the case that there are no ground terms of a type that occurs in a
+ * quantified formula, or for
+ * exhaustive instantiation strategies that enumerate over small interpreted
+ * finite types.
+ */
class RepSet {
public:
RepSet(){}
~RepSet(){}
+ /** map from types to the list of representatives
+ * TODO : as part of #1199, encapsulate this
+ */
std::map< TypeNode, std::vector< Node > > d_type_reps;
- std::map< TypeNode, bool > d_type_complete;
- std::map< Node, int > d_tmap;
- // map from values to terms they were assigned for
- std::map< Node, Node > d_values_to_terms;
/** clear the set */
void clear();
- /** has type */
+ /** does this set have representatives of type tn? */
bool hasType( TypeNode tn ) const { return d_type_reps.find( tn )!=d_type_reps.end(); }
- /** has rep */
- bool hasRep( TypeNode tn, Node n );
- /** get cardinality for type */
- int getNumRepresentatives( TypeNode tn ) const;
- /** add representative for type */
+ /** does this set have representative n of type tn? */
+ bool hasRep(TypeNode tn, Node n) const;
+ /** get the number of representatives for type */
+ unsigned getNumRepresentatives(TypeNode tn) const;
+ /** get representative at index */
+ Node getRepresentative(TypeNode tn, unsigned i) const;
+ /** add representative n for type tn, where n has type tn */
void add( TypeNode tn, Node n );
/** returns index in d_type_reps for node n */
int getIndexFor( Node n ) const;
- /** complete all values */
+ /** complete the list for type t
+ * Resets d_type_reps[tn] and repopulates by running the type enumerator for
+ * that type exhaustively.
+ * This should only be called for small finite interpreted types.
+ */
bool complete( TypeNode t );
+ /** get term for representative
+ * Returns a term that is interpreted as representative n in the current
+ * model, null otherwise.
+ */
+ Node getTermForRepresentative(Node n) const;
+ /** set term for representative
+ * Called when t is interpreted as value n. Subsequent class to
+ * getTermForRepresentative( n ) will return t.
+ */
+ void setTermForRepresentative(Node n, Node t);
+ /** get existing domain value, with possible exclusions
+ * This function returns a term in d_type_reps[tn] but not in exclude
+ */
+ Node getDomainValue(TypeNode tn, const std::vector<Node>& exclude) const;
/** debug print */
void toStream(std::ostream& out);
+
+ private:
+ /** whether the list of representatives for types are complete */
+ std::map<TypeNode, bool> d_type_complete;
+ /** map from representatives to their index in d_type_reps */
+ std::map<Node, int> d_tmap;
+ /** map from values to terms they were assigned for */
+ std::map<Node, Node> d_values_to_terms;
};/* class RepSet */
//representative domain
// TODO: if func models not enabled, throw an error?
Unreachable();
}
- }else if(t.isRegExp()) {
+ }
+ else if (!t.isFirstClass())
+ {
+ // this is the class for regular expressions
+ // we simply invoke the rewriter on them
ret = Rewriter::rewrite(ret);
} else {
if (options::omitDontCares() && useDontCares) {
return ret;
}
-Node TheoryModel::getDomainValue( TypeNode tn, std::vector< Node >& exclude ){
- if( d_rep_set.d_type_reps.find( tn )!=d_rep_set.d_type_reps.end() ){
- //try to find a pre-existing arbitrary element
- for( size_t i=0; i<d_rep_set.d_type_reps[tn].size(); i++ ){
- if( std::find( exclude.begin(), exclude.end(), d_rep_set.d_type_reps[tn][i] )==exclude.end() ){
- return d_rep_set.d_type_reps[tn][i];
- }
- }
- }
- return Node::null();
-}
-
/** add substitution */
void TheoryModel::addSubstitution( TNode x, TNode t, bool invalidateCache ){
if( !d_substitutions.hasSubstitution( x ) ){
if (first) {
rep = (*eqc_i);
//add the term (this is specifically for the case of singleton equivalence classes)
- if( !rep.getType().isRegExp() ){
+ if (rep.getType().isFirstClass())
+ {
d_equalityEngine->addTerm( rep );
Trace("model-builder-debug") << "Add term to ee within assertEqualityEngine: " << rep << std::endl;
}
void TheoryEngineModelBuilder::assignConstantRep( TheoryModel* tm, Node eqc, Node const_rep ) {
d_constantReps[eqc] = const_rep;
Trace("model-builder") << " Assign: Setting constant rep of " << eqc << " to " << const_rep << endl;
- tm->d_rep_set.d_values_to_terms[const_rep] = eqc;
+ tm->d_rep_set.setTermForRepresentative(const_rep, eqc);
}
bool TheoryEngineModelBuilder::isExcludedCdtValue( Node val, std::set<Node>* repSet, std::map< Node, Node >& assertedReps, Node eqc ) {
retNode = NodeManager::currentNM()->mkNode( r.getKind(), children );
if (childrenConst) {
retNode = Rewriter::rewrite(retNode);
- Assert(retNode.getKind()==kind::APPLY_UF || retNode.getType().isRegExp() || retNode.isConst());
+ Assert(retNode.getKind() == kind::APPLY_UF
+ || !retNode.getType().isFirstClass()
+ || retNode.isConst());
}
}
d_normalizedCache[r] = retNode;
class TheoryModel : public Model
{
friend class TheoryEngineModelBuilder;
-protected:
- /** substitution map for this model */
- SubstitutionMap d_substitutions;
- bool d_modelBuilt;
+
public:
TheoryModel(context::Context* c, std::string name, bool enableFuncModels);
virtual ~TheoryModel() throw();
- /** special local context for our equalityEngine so we can clear it independently of search context */
- context::Context* d_eeContext;
- /** equality engine containing all known equalities/disequalities */
- eq::EqualityEngine* d_equalityEngine;
- /** map of representatives of equality engine to used representatives in representative set */
- std::map< Node, Node > d_reps;
- /** stores set of representatives for each type */
- RepSet d_rep_set;
- /** true/false nodes */
- Node d_true;
- Node d_false;
- mutable std::unordered_map<Node, Node, NodeHashFunction> d_modelCache;
-public:
- /** comment stream to include in printing */
- std::stringstream d_comment_str;
/** get comments */
void getComments(std::ostream& out) const;
-private:
- /** information for separation logic */
- Node d_sep_heap;
- Node d_sep_nil_eq;
-public:
- void setHeapModel( Node h, Node neq );
- bool getHeapModel( Expr& h, Expr& neq ) const;
-protected:
- /** reset the model */
- virtual void reset();
- /**
- * Get model value function. This function is called by getValue
- */
- Node getModelValue(TNode n, bool hasBoundVars = false, bool useDontCares = false) const;
-public:
/** is built */
bool isBuilt() { return d_modelBuilt; }
/** set need build */
*/
Node getValue( TNode n, bool useDontCares = false ) const;
- /** get existing domain value, with possible exclusions
- * This function returns a term in d_rep_set.d_type_reps[tn] but not in exclude
- */
- Node getDomainValue( TypeNode tn, std::vector< Node >& exclude );
-public:
+ //---------------------------- separation logic
+ /** set the heap and value sep.nil is equal to */
+ void setHeapModel(Node h, Node neq);
+ /** get the heap and value sep.nil is equal to */
+ bool getHeapModel(Expr& h, Expr& neq) const;
+ //---------------------------- end separation logic
+
/** Adds a substitution from x to t. */
void addSubstitution(TNode x, TNode t, bool invalidateCache = true);
/** add term function
* functions.
*/
void assertRepresentative(TNode n);
-public:
- /** general queries */
+
+ // ------------------- general equality queries
+ /** does the equality engine of this model have term a? */
bool hasTerm(TNode a);
+ /** get the representative of a in the equality engine of this model */
Node getRepresentative(TNode a);
+ /** are a and b equal in the equality engine of this model? */
bool areEqual(TNode a, TNode b);
+ /** are a and b disequal in the equality engine of this model? */
bool areDisequal(TNode a, TNode b);
-public:
+ /** get the equality engine for this model */
+ eq::EqualityEngine* getEqualityEngine() { return d_equalityEngine; }
+ // ------------------- end general equality queries
+
+ /** get the representative set object */
+ const RepSet* getRepSet() const { return &d_rep_set; }
+ /** get the representative set object (FIXME: remove this, see #1199) */
+ RepSet* getRepSetPtr() { return &d_rep_set; }
/** return whether this node is a don't-care */
bool isDontCare(Expr expr) const;
/** get value function for Exprs. */
Expr getValue( Expr expr ) const;
/** get cardinality for sort */
Cardinality getCardinality( Type t ) const;
-public:
/** print representative debug function */
void printRepresentativeDebug( const char* c, Node r );
/** print representative function */
void printRepresentative( std::ostream& out, Node r );
-private:
- /** map from function terms to the (lambda) definitions
- * After the model is built, the domain of this map is all terms of function type
- * that appear as terms in d_equalityEngine.
- */
- std::map< Node, Node > d_uf_models;
-public:
- /** whether function models are enabled */
- bool d_enableFuncModels;
+
+ //---------------------------- function values
/** a map from functions f to a list of all APPLY_UF terms with operator f */
std::map< Node, std::vector< Node > > d_uf_terms;
/** a map from functions f to a list of all HO_APPLY terms with first argument f */
* which is required for "dag form" model construction (see TheoryModelBuilder::assignHoFunction).
*/
std::vector< Node > getFunctionsToAssign();
+ //---------------------------- end function values
+ protected:
+ /** substitution map for this model */
+ SubstitutionMap d_substitutions;
+ /** whether this model has been built */
+ bool d_modelBuilt;
+ /** special local context for our equalityEngine so we can clear it
+ * independently of search context */
+ context::Context* d_eeContext;
+ /** equality engine containing all known equalities/disequalities */
+ eq::EqualityEngine* d_equalityEngine;
+ /** map of representatives of equality engine to used representatives in
+ * representative set */
+ std::map<Node, Node> d_reps;
+ /** stores set of representatives for each type */
+ RepSet d_rep_set;
+ /** true/false nodes */
+ Node d_true;
+ Node d_false;
+ mutable std::unordered_map<Node, Node, NodeHashFunction> d_modelCache;
+ /** comment stream to include in printing */
+ std::stringstream d_comment_str;
+ /** reset the model */
+ virtual void reset();
+ /**
+ * Get model value function. This function is called by getValue
+ */
+ Node getModelValue(TNode n,
+ bool hasBoundVars = false,
+ bool useDontCares = false) const;
+
+ private:
+ //---------------------------- separation logic
+ /** the value of the heap */
+ Node d_sep_heap;
+ /** the value of the nil element */
+ Node d_sep_nil_eq;
+ //---------------------------- end separation logic
+
+ //---------------------------- function values
+ /** whether function models are enabled */
+ bool d_enableFuncModels;
+ /** map from function terms to the (lambda) definitions
+ * After the model is built, the domain of this map is all terms of function
+ * type
+ * that appear as terms in d_equalityEngine.
+ */
+ std::map<Node, Node> d_uf_models;
+ //---------------------------- end function values
};/* class TheoryModel */
/*
//consider finding another value, if possible
Debug("fmf-model-cons-debug") << "Poor choice for default value, score = " << maxScore << std::endl;
TypeNode tn = defaultTerm.getType();
- Node newDefaultVal = m->getDomainValue( tn, d_values );
+ Node newDefaultVal = m->getRepSet()->getDomainValue(tn, d_values);
if( !newDefaultVal.isNull() ){
defaultVal = newDefaultVal;
Debug("fmf-model-cons-debug") << "-> Change default value to ";
#if 0
// ensure that the constructed model is minimal
// if the model has terms that the strong solver does not know about
- if( (int)m->d_rep_set.d_type_reps[ d_type ].size()>d_cardinality ){
- eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &m->d_equalityEngine );
+ if( (int)rs->d_type_reps[ d_type ].size()>d_cardinality ){
+ eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &m->getEqualityEngine() );
while( !eqcs_i.isFinished() ){
Node eqc = (*eqcs_i);
if( eqc.getType()==d_type ){
bool SortModel::debugModel( TheoryModel* m ){
if( Trace.isOn("uf-ss-warn") ){
std::vector< Node > eqcs;
- eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( m->d_equalityEngine );
+ eq::EqClassesIterator eqcs_i =
+ eq::EqClassesIterator(m->getEqualityEngine());
while( !eqcs_i.isFinished() ){
Node eqc = (*eqcs_i);
if( eqc.getType()==d_type ){
++eqcs_i;
}
}
- int nReps = m->d_rep_set.d_type_reps.find( d_type )==m->d_rep_set.d_type_reps.end() ? 0 : (int)m->d_rep_set.d_type_reps[d_type].size();
+ RepSet* rs = m->getRepSetPtr();
+ int nReps = (int)rs->getNumRepresentatives(d_type);
if( nReps!=(d_maxNegCard+1) ){
Trace("uf-ss-warn") << "WARNING : Model does not have same # representatives as cardinality for " << d_type << "." << std::endl;
Trace("uf-ss-warn") << " Max neg cardinality : " << d_maxNegCard << std::endl;
/*
for( unsigned i=0; i<d_fresh_aloc_reps.size(); i++ ){
if( add>0 && !m->d_equalityEngine->hasTerm( d_fresh_aloc_reps[i] ) ){
- m->d_rep_set.d_type_reps[d_type].push_back( d_fresh_aloc_reps[i] );
+ rs->d_type_reps[d_type].push_back( d_fresh_aloc_reps[i] );
add--;
}
}
for( int i=0; i<add; i++ ){
std::stringstream ss;
ss << "r_" << d_type << "_";
- Node nn = NodeManager::currentNM()->mkSkolem( ss.str(), d_type, "enumeration to meet negative card constraint" );
+ Node nn = NodeManager::currentNM()->mkSkolem( ss.str(), d_type,
+ "enumeration to meet negative card constraint" );
d_fresh_aloc_reps.push_back( nn );
- m->d_rep_set.d_type_reps[d_type].push_back( nn );
+ rs->d_type_reps[d_type].push_back( nn );
}
*/
while( (int)d_fresh_aloc_reps.size()<=d_maxNegCard ){
d_fresh_aloc_reps.push_back( nn );
}
if( d_maxNegCard==0 ){
- m->d_rep_set.d_type_reps[d_type].push_back( d_fresh_aloc_reps[0] );
+ rs->d_type_reps[d_type].push_back(d_fresh_aloc_reps[0]);
}else{
//must add lemma
std::vector< Node > force_cl;
projects / cvc5.git / commitdiff