diff options
Diffstat (limited to 'src/theory/quantifiers/full_model_check.cpp')
| -rwxr-xr-x | src/theory/quantifiers/full_model_check.cpp | 326 |
1 files changed, 219 insertions, 107 deletions
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index 7f30a045e..ed5dea679 100755 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -59,22 +59,24 @@ bool EntryTrie::hasGeneralization( FirstOrderModelFmc * m, Node c, int index ) { return true;
}
}
- //for star: check if all children are defined and have generalizations
- if( options::fmfFmcCoverSimplify() && 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.hasGeneralization(m, c, index+1) ){
- complete = false;
- break;
+ if( !options::fmfFmcInterval() || !c[index].getType().isInteger() ){
+ //for star: check if all children are defined and have generalizations
+ if( options::fmfFmcCoverSimplify() && 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.hasGeneralization(m, c, index+1) ){
+ complete = false;
+ break;
+ }
}
}
- }
- if( complete ){
- return true;
+ if( complete ){
+ return true;
+ }
}
}
}
@@ -88,15 +90,41 @@ int EntryTrie::getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node> return d_data;
}else{
int minIndex = -1;
- Node st = m->getStar(inst[index].getType());
- if(d_child.find(st)!=d_child.end()) {
- minIndex = d_child[st].getGeneralizationIndex(m, inst, index+1);
- }
- Node cc = inst[index];
- 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;
+ if( options::fmfFmcInterval() && inst[index].getType().isInteger() ){
+ for( std::map<Node,EntryTrie>::iterator it = d_child.begin(); it != d_child.end(); ++it ){
+ if( !m->isInterval( it->first ) ){
+ std::cout << "Not an interval during getGenIndex " << it->first << std::endl;
+ exit( 11 );
+ }
+ //check if it is in the range
+ bool inRange = true;
+ for( unsigned b=0; b<2; b++ ){
+ if( !m->isStar( it->first[b] ) ){
+ if( ( b==0 && it->first[b].getConst<Rational>() > inst[index].getConst<Rational>() ) ||
+ ( b==1 && it->first[b].getConst<Rational>() <= inst[index].getConst<Rational>() ) ){
+ inRange = false;
+ break;
+ }
+ }
+ }
+ if( inRange ){
+ int gindex = it->second.getGeneralizationIndex(m, inst, index+1);
+ if( minIndex==-1 || (gindex!=-1 && gindex<minIndex) ){
+ minIndex = gindex;
+ }
+ }
+ }
+ }else{
+ Node st = m->getStar(inst[index].getType());
+ if(d_child.find(st)!=d_child.end()) {
+ minIndex = d_child[st].getGeneralizationIndex(m, inst, index+1);
+ }
+ Node cc = inst[index];
+ 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;
+ }
}
}
return minIndex;
@@ -143,39 +171,6 @@ void EntryTrie::getEntries( FirstOrderModelFmc * m, Node c, std::vector<int> & c }
}
-
-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;
- }
- }
- }
- if( complete ){
- 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 ){
@@ -209,12 +204,6 @@ 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;
@@ -247,6 +236,7 @@ Node Def::evaluate( FirstOrderModelFmc * m, std::vector<Node>& inst ) { if (gindex!=-1) {
return d_value[gindex];
}else{
+ Trace("fmc-warn") << "Warning : evaluation came up null!" << std::endl;
return Node::null();
}
}
@@ -280,7 +270,7 @@ void Def::simplify(FullModelChecker * mc, FirstOrderModelFmc * m) { 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]) ){
+ if( !m->isInterval(cc[i]) && !m->isStar(cc[i]) ){
last_all_stars = false;
break;
}
@@ -475,10 +465,12 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ for( unsigned i=0; i<c.getNumChildren(); i++) {
Node ri = fm->getUsedRepresentative( c[i]);
children.push_back(ri);
- if (fm->isModelBasisTerm(ri)) {
- ri = fm->getStar( ri.getType() );
- }else{
- hasNonStar = true;
+ if( !options::fmfFmcInterval() || !ri.getType().isInteger() ){
+ if (fm->isModelBasisTerm(ri) ) {
+ ri = fm->getStar( ri.getType() );
+ }else{
+ hasNonStar = true;
+ }
}
entry_children.push_back(ri);
}
@@ -510,8 +502,7 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ for (int i=0; i<(int)indices.size(); i++) {
fm->d_models[op]->addEntry(fm, entry_conds[indices[i]], values[indices[i]]);
}
- fm->d_models[op]->debugPrint("fmc-model", op, this);
- Trace("fmc-model") << std::endl;
+
if( options::fmfFmcInterval() ){
Trace("fmc-interval-model") << "Changing to interval model, Before : " << std::endl;
@@ -523,21 +514,45 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ }
std::map< int, std::map< int, Node > > changed_vals;
makeIntervalModel( fm, op, indices, 0, changed_vals );
- for( std::map< int, std::map< int, Node > >::iterator it = changed_vals.begin(); it != changed_vals.end(); ++it ){
- Trace("fmc-interval-model") << "Entry #" << it->first << " changed : ";
- for( std::map< int, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
- Trace("fmc-interval-model") << it2->first << " -> " << it2->second << ", ";
+
+ std::vector< Node > conds;
+ std::vector< Node > values;
+ for( unsigned i=0; i<fm->d_models[op]->d_cond.size(); i++ ){
+ if( changed_vals.find(i)==changed_vals.end() ){
+ conds.push_back( fm->d_models[op]->d_cond[i] );
+ }else{
+ std::vector< Node > children;
+ children.push_back( op );
+ for( unsigned j=0; j<fm->d_models[op]->d_cond[i].getNumChildren(); j++ ){
+ if( changed_vals[i].find(j)==changed_vals[i].end() ){
+ children.push_back( fm->d_models[op]->d_cond[i][j] );
+ }else{
+ children.push_back( changed_vals[i][j] );
+ }
+ }
+ Node nc = NodeManager::currentNM()->mkNode( APPLY_UF, children );
+ conds.push_back( nc );
+ Trace("fmc-interval-model") << "Interval : Entry #" << i << " changed to ";
+ debugPrintCond("fmc-interval-model", nc, true );
+ Trace("fmc-interval-model") << std::endl;
}
- Trace("fmc-interval-model") << std::endl;
+ values.push_back( fm->d_models[op]->d_value[i] );
+ }
+ fm->d_models[op]->reset();
+ for( unsigned i=0; i<conds.size(); i++ ){
+ fm->d_models[op]->addEntry(fm, conds[i], values[i] );
}
}
+ Trace("fmc-model-simplify") << "Before simplification : " << std::endl;
+ fm->d_models[op]->debugPrint("fmc-model-simplify", op, this);
+ Trace("fmc-model-simplify") << std::endl;
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;
+
+ fm->d_models[op]->debugPrint("fmc-model", op, this);
+ Trace("fmc-model") << std::endl;
}
}
}
@@ -600,7 +615,8 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, Trace("fmc") << "Definition for quantifier " << f << " is : " << std::endl;
d_quant_models[f].debugPrint("fmc", Node::null(), this);
Trace("fmc") << std::endl;
- //consider all entries going to false
+
+ //consider all entries going to non-true
for (unsigned i=0; i<d_quant_models[f].d_cond.size(); i++) {
if( d_quant_models[f].d_value[i]!=d_true) {
Trace("fmc-inst") << "Instantiate based on " << d_quant_models[f].d_cond[i] << "..." << std::endl;
@@ -610,6 +626,21 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, if (fmfmc->isStar(d_quant_models[f].d_cond[i][j])) {
hasStar = true;
inst.push_back(fmfmc->getModelBasisTerm(d_quant_models[f].d_cond[i][j].getType()));
+ }else if( fmfmc->isInterval(d_quant_models[f].d_cond[i][j])){
+ hasStar = true;
+ //if interval, find a sample point
+ if( fmfmc->isStar(d_quant_models[f].d_cond[i][j][0]) ){
+ if( fmfmc->isStar(d_quant_models[f].d_cond[i][j][1]) ){
+ inst.push_back(fmfmc->getModelBasisTerm(d_quant_models[f].d_cond[i][j][1].getType()));
+ }else{
+ Node nn = NodeManager::currentNM()->mkNode( MINUS, d_quant_models[f].d_cond[i][j][1],
+ NodeManager::currentNM()->mkConst( Rational(1) ) );
+ nn = Rewriter::rewrite( nn );
+ inst.push_back( nn );
+ }
+ }else{
+ inst.push_back(d_quant_models[f].d_cond[i][j][0]);
+ }
}else{
inst.push_back(d_quant_models[f].d_cond[i][j]);
}
@@ -683,13 +714,24 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No Trace("fmc-exh") << "Exhaustive instantiate based on index " << c_index << " : " << c << " ";
debugPrintCond("fmc-exh", c, true);
Trace("fmc-exh")<< std::endl;
+ //set the bounds on the iterator based on intervals
+ for( unsigned i=0; i<c.getNumChildren(); i++ ){
+ if( fm->isInterval(c[i]) ){
+ for( unsigned b=0; b<2; b++ ){
+ if( !fm->isStar(c[i][b]) ){
+ riter.d_bounds[b][i] = c[i][b];
+ }
+ }
+ }
+ }
+ //initialize
if( riter.setQuantifier( f ) ){
//set the domains based on the entry
for (unsigned i=0; i<c.getNumChildren(); i++) {
if (riter.d_enum_type[i]==RepSetIterator::ENUM_DOMAIN_ELEMENTS) {
TypeNode tn = c[i].getType();
if( d_rep_ids.find(tn)!=d_rep_ids.end() ){
- if( fm->isStar(c[i]) ){
+ if( fm->isInterval(c[i]) || fm->isStar(c[i]) ){
//add the full range
}else{
if (d_rep_ids[tn].find(c[i])!=d_rep_ids[tn].end()) {
@@ -704,8 +746,10 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No }
}
}
+ int addedLemmas = 0;
//now do full iteration
while( !riter.isFinished() ){
+ d_triedLemmas++;
Trace("fmc-exh-debug") << "Inst : ";
std::vector< Node > inst;
for( int i=0; i<riter.getNumTerms(); i++ ){
@@ -719,29 +763,27 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No int ev_index = d_quant_models[f].getGeneralizationIndex(fm, inst);
Trace("fmc-exh-debug") << ", index = " << ev_index;
Node ev = ev_index==-1 ? Node::null() : d_quant_models[f].d_value[ev_index];
- bool successAdd = false;
if (ev!=d_true) {
InstMatch m;
for( int i=0; i<riter.getNumTerms(); i++ ){
m.set( d_qe, f, i, riter.getTerm( i ) );
}
Trace("fmc-exh-debug") << ", add!";
- d_triedLemmas++;
//add as instantiation
if( d_qe->addInstantiation( f, m ) ){
Trace("fmc-exh-debug") << " ...success.";
- d_addedLemmas++;
- successAdd = true;
+ addedLemmas++;
}
}
Trace("fmc-exh-debug") << std::endl;
int index = riter.increment();
Trace("fmc-exh-debug") << "Incremented index " << index << std::endl;
- if (index>=0 && successAdd && riter.d_enum_type[index]==RepSetIterator::ENUM_RANGE) {
+ if (index>=0 && riter.d_index[index]>0 && addedLemmas>0 && riter.d_enum_type[index]==RepSetIterator::ENUM_RANGE) {
Trace("fmc-exh-debug") << "Since this is a range enumeration, skip to the next..." << std::endl;
riter.increment2( index-1 );
}
}
+ d_addedLemmas += addedLemmas;
return true;
}else{
return false;
@@ -750,9 +792,12 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n ) {
Trace("fmc-debug") << "Check " << n << " " << n.getKind() << std::endl;
- if( n.getKind() == kind::BOUND_VARIABLE ){
+ //first check if it is a bounding literal
+ if( n.hasAttribute(BoundIntLitAttribute()) ){
+ Trace("fmc-debug") << "It is a bounding literal, polarity = " << n.getAttribute(BoundIntLitAttribute()) << std::endl;
+ d.addEntry(fm, mkCondDefault(fm, f), n.getAttribute(BoundIntLitAttribute())==1 ? d_false : d_true );
+ }else if( n.getKind() == kind::BOUND_VARIABLE ){
d.addEntry(fm, mkCondDefault(fm, f), n);
- Trace("fmc-debug") << "Done with " << n << " " << n.getKind() << std::endl;
}
else if( n.getKind() == kind::NOT ){
//just do directly
@@ -792,10 +837,12 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n }
else if( n.getNumChildren()==0 ){
Node r = n;
- if( !fm->hasTerm(n) ){
- r = getSomeDomainElement(fm, n.getType() );
+ if( !n.isConst() ){
+ if( !fm->hasTerm(n) ){
+ r = getSomeDomainElement(fm, n.getType() );
+ }
+ r = fm->getUsedRepresentative( r );
}
- r = fm->getUsedRepresentative( r);
d.addEntry(fm, mkCondDefault(fm, f), r);
}
else{
@@ -983,7 +1030,7 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f, if( !v.isNull() && v.getKind()==kind::BOUND_VARIABLE ){
int j = getVariableId(f, v);
Trace("fmc-uf-process") << v << " is variable #" << j << std::endl;
- if (!fm->isStar(cond[j+1])) {
+ if (!fm->isStar(cond[j+1]) && !fm->isInterval(cond[j+1])) {
v = cond[j+1];
}else{
bind_var = true;
@@ -992,18 +1039,30 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f, if (bind_var) {
Trace("fmc-uf-process") << "bind variable..." << std::endl;
int j = getVariableId(f, v);
- for (std::map<Node, EntryTrie>::iterator it = curr.d_child.begin(); it != curr.d_child.end(); ++it) {
- cond[j+1] = it->first;
- doUninterpretedCompose2(fm, f, entries, index+1, cond, val, it->second);
+ if( fm->isStar(cond[j+1]) ){
+ for (std::map<Node, EntryTrie>::iterator it = curr.d_child.begin(); it != curr.d_child.end(); ++it) {
+ cond[j+1] = it->first;
+ doUninterpretedCompose2(fm, f, entries, index+1, cond, val, it->second);
+ }
+ cond[j+1] = fm->getStar(v.getType());
+ }else{
+ Node orig = cond[j+1];
+ for (std::map<Node, EntryTrie>::iterator it = curr.d_child.begin(); it != curr.d_child.end(); ++it) {
+ Node nw = doIntervalMeet( fm, it->first, orig );
+ if( !nw.isNull() ){
+ cond[j+1] = nw;
+ doUninterpretedCompose2(fm, f, entries, index+1, cond, val, it->second);
+ }
+ }
+ cond[j+1] = orig;
}
- cond[j+1] = fm->getStar(v.getType());
}else{
if( !v.isNull() ){
if (curr.d_child.find(v)!=curr.d_child.end()) {
Trace("fmc-uf-process") << "follow value..." << std::endl;
doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[v]);
}
- Node st = fm->getStar(v.getType());
+ Node st = fm->getStarElement(v.getType());
if (curr.d_child.find(st)!=curr.d_child.end()) {
Trace("fmc-uf-process") << "follow star..." << std::endl;
doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[st]);
@@ -1050,29 +1109,73 @@ void FullModelChecker::doInterpretedCompose( FirstOrderModelFmc * fm, Node f, De }
int FullModelChecker::isCompat( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c ) {
+ Trace("fmc-debug2") << "isCompat " << c << std::endl;
Assert(cond.size()==c.getNumChildren()+1);
for (unsigned i=1; i<cond.size(); i++) {
- if( cond[i]!=c[i-1] && !fm->isStar(cond[i]) && !fm->isStar(c[i-1]) ) {
- return 0;
+ if( options::fmfFmcInterval() && cond[i].getType().isInteger() ){
+ Node iv = doIntervalMeet( fm, cond[i], c[i-1], false );
+ if( iv.isNull() ){
+ return 0;
+ }
+ }else{
+ if( cond[i]!=c[i-1] && !fm->isStar(cond[i]) && !fm->isStar(c[i-1]) ) {
+ return 0;
+ }
}
}
return 1;
}
bool FullModelChecker::doMeet( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c ) {
+ Trace("fmc-debug2") << "doMeet " << c << std::endl;
Assert(cond.size()==c.getNumChildren()+1);
for (unsigned i=1; i<cond.size(); i++) {
if( cond[i]!=c[i-1] ) {
- if( fm->isStar(cond[i]) ){
- cond[i] = c[i-1];
- }else if( !fm->isStar(c[i-1]) ){
- return false;
+ if( options::fmfFmcInterval() && cond[i].getType().isInteger() ){
+ Node iv = doIntervalMeet( fm, cond[i], c[i-1] );
+ if( !iv.isNull() ){
+ cond[i] = iv;
+ }else{
+ return false;
+ }
+ }else{
+ if( fm->isStar(cond[i]) ){
+ cond[i] = c[i-1];
+ }else if( !fm->isStar(c[i-1]) ){
+ return false;
+ }
}
}
}
return true;
}
+Node FullModelChecker::doIntervalMeet( FirstOrderModelFmc * fm, Node i1, Node i2, bool mk ) {
+ if( !fm->isInterval( i1 ) || !fm->isInterval( i2 ) ){
+ std::cout << "Not interval during meet! " << i1 << " " << i2 << std::endl;
+ exit( 0 );
+ }
+ Node b[2];
+ for( unsigned j=0; j<2; j++ ){
+ Node b1 = i1[j];
+ Node b2 = i2[j];
+ if( fm->isStar( b1 ) ){
+ b[j] = b2;
+ }else if( fm->isStar( b2 ) ){
+ b[j] = b1;
+ }else if( b1.getConst<Rational>() < b2.getConst<Rational>() ){
+ b[j] = j==0 ? b2 : b1;
+ }else{
+ b[j] = j==0 ? b1 : b2;
+ }
+ }
+ if( fm->isStar( b[0] ) || fm->isStar( b[1] ) || b[0].getConst<Rational>() < b[1].getConst<Rational>() ){
+ return mk ? fm->getInterval( b[0], b[1] ) : i1;
+ }else{
+ return Node::null();
+ }
+}
+
Node FullModelChecker::mkCond( std::vector< Node > & cond ) {
return NodeManager::currentNM()->mkNode(APPLY_UF, cond);
}
@@ -1087,7 +1190,7 @@ void FullModelChecker::mkCondDefaultVec( FirstOrderModelFmc * fm, Node f, std::v //get function symbol for f
cond.push_back(d_quant_cond[f]);
for (unsigned i=0; i<f[0].getNumChildren(); i++) {
- Node ts = fm->getStar( f[0][i].getType() );
+ Node ts = fm->getStarElement( f[0][i].getType() );
cond.push_back(ts);
}
}
@@ -1189,7 +1292,7 @@ void FullModelChecker::makeIntervalModel( FirstOrderModelFmc * fm, Node op, std: std::map< Node, std::vector< int > > new_indices;
for( unsigned i=0; i<indices.size(); i++ ){
Node v = fm->d_models[op]->d_cond[indices[i]][index];
- new_indices[v].push_back( i );
+ new_indices[v].push_back( indices[i] );
}
for( std::map< Node, std::vector< int > >::iterator it = new_indices.begin(); it != new_indices.end(); ++it ){
@@ -1201,21 +1304,29 @@ void FullModelChecker::makeIntervalModel( FirstOrderModelFmc * fm, Node op, std: void FullModelChecker::makeIntervalModel2( FirstOrderModelFmc * fm, Node op, std::vector< int > & indices, int index,
std::map< int, std::map< int, Node > >& changed_vals ) {
+ Debug("fmc-interval-model-debug") << "Process " << index << " with indicies : ";
+ for( unsigned i=0; i<indices.size(); i++ ){
+ Debug("fmc-interval-model-debug") << indices[i] << " ";
+ }
+ Debug("fmc-interval-model-debug") << std::endl;
+
if( index<(int)fm->d_models[op]->d_cond[0].getNumChildren() ){
TypeNode tn = fm->d_models[op]->d_cond[0][index].getType();
if( tn.isInteger() ){
std::map< Node, std::vector< int > > new_indices;
for( unsigned i=0; i<indices.size(); i++ ){
Node v = fm->d_models[op]->d_cond[indices[i]][index];
- new_indices[v].push_back( i );
+ new_indices[v].push_back( indices[i] );
+ if( !v.isConst() ){
+ Trace("fmc-warn") << "WARNING: for interval, model has non-constant : " << v << std::endl;
+ Trace("fmc-warn") << "From condition : " << fm->d_models[op]->d_cond[indices[i]] << std::endl;
+ }
}
std::vector< Node > values;
for( std::map< Node, std::vector< int > >::iterator it = new_indices.begin(); it != new_indices.end(); ++it ){
makeIntervalModel2( fm, op, it->second, index+1, changed_vals );
- if( !fm->isStar(it->first) ){
- values.push_back( it->first );
- }
+ values.push_back( it->first );
}
if( tn.isInteger() ){
@@ -1236,6 +1347,7 @@ void FullModelChecker::makeIntervalModel2( FirstOrderModelFmc * fm, Node op, std }
Node interval = fm->getInterval( lb, ub );
for( unsigned j=0; j<new_indices[values[sindices[i]]].size(); j++ ){
+ Debug("fmc-interval-model-debug") << "Change " << new_indices[values[sindices[i]]][j] << ", " << index << " to " << interval << std::endl;
changed_vals[new_indices[values[sindices[i]]][j]][index] = interval;
}
ub = lb;
|