void FullModelChecker::initializeType( FirstOrderModelFmc * fm, TypeNode tn ){
if( fm->d_model_basis_rep.find( tn )==fm->d_model_basis_rep.end() ){
- Trace("fmc") << "Initialize type " << tn << std::endl;
+ Trace("fmc") << "Initialize type " << tn << " hasType = " << fm->d_rep_set.hasType(tn) << std::endl;\r
Node mbn;
if (!fm->d_rep_set.hasType(tn)) {
mbn = fm->getSomeDomainElement(tn);
}
d_triedLemmas++;
if( d_qe->addInstantiation( f, m ) ){
+ Trace("fmc-debug-inst") << "** Added instantiation." << std::endl;\r
d_addedLemmas++;
}else{
+ Trace("fmc-debug-inst") << "** Instantiation was duplicate." << std::endl;\r
//this can happen if evaluation is unknown
//might try it next effort level
d_star_insts[f].push_back(i);
}
}else{
+ Trace("fmc-debug-inst") << "** Instantiation was already true." << std::endl;\r
//might try it next effort level
d_star_insts[f].push_back(i);
}
}
int FullModelChecker::isCompat( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c ) {
- Trace("fmc-debug2") << "isCompat " << c << std::endl;
+ Trace("fmc-debug3") << "isCompat " << c << std::endl;\r
Assert(cond.size()==c.getNumChildren()+1);
for (unsigned i=1; i<cond.size(); i++) {
if( options::fmfFmcInterval() && cond[i].getType().isInteger() ){
}
bool FullModelChecker::doMeet( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c ) {
- Trace("fmc-debug2") << "doMeet " << c << std::endl;
+ Trace("fmc-debug3") << "doMeet " << c << std::endl;\r
Assert(cond.size()==c.getNumChildren()+1);
for (unsigned i=1; i<cond.size(); i++) {
if( cond[i]!=c[i-1] ) {
Node TermDb::getModelBasisTerm( TypeNode tn, int i ){
if( d_model_basis_term.find( tn )==d_model_basis_term.end() ){
Node mbt;
- if( options::fmfFreshDistConst() || d_type_map[ tn ].empty() ){
- if( tn.isInteger() || tn.isReal() ){
- mbt = NodeManager::currentNM()->mkConst( Rational( 0 ) );
- }else{
+ if( tn.isInteger() || tn.isReal() ){
+ mbt = NodeManager::currentNM()->mkConst( Rational( 0 ) );
+ }else if( !tn.isSort() ){
+ mbt = tn.mkGroundTerm();
+ }else{
+ if( options::fmfFreshDistConst() || d_type_map[ tn ].empty() ){
std::stringstream ss;
ss << Expr::setlanguage(options::outputLanguage());
ss << "e_" << tn;
mbt = NodeManager::currentNM()->mkSkolem( ss.str(), tn, "is a model basis term" );
Trace("mkVar") << "ModelBasis:: Make variable " << mbt << " : " << tn << std::endl;
+ }else{
+ mbt = d_type_map[ tn ][ 0 ];
}
- }else{
- mbt = d_type_map[ tn ][ 0 ];
}
ModelBasisAttribute mba;
mbt.setAttribute(mba,true);