diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-05-11 17:36:07 -0500 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-05-11 17:36:07 -0500 |
| commit | 24d60fa5654a32b09dc8de79b7704fbf40051478 (patch) | |
| tree | d3bce397adceb1407764a54489c191aea06d134a /src/theory/quantifiers/full_model_check.cpp | |
| parent | f6d24c56905449e68ee23a9cea54985eacd24aa3 (diff) | |
Preliminary version of finite model finding over bounded integer quantification. Minor update to casc script.
Diffstat (limited to 'src/theory/quantifiers/full_model_check.cpp')
| -rwxr-xr-x | src/theory/quantifiers/full_model_check.cpp | 20 |
1 files changed, 11 insertions, 9 deletions
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index 4ce9dba21..4904368a2 100755 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -535,31 +535,33 @@ int FullModelChecker::exhaustiveInstantiate(FirstOrderModel * fm, Node f, Node c Trace("fmc-exh") << "Exhaustive instantiate based on index " << c_index << " : " << c << " ";
debugPrintCond("fmc-exh", c, true);
Trace("fmc-exh")<< std::endl;
- if( riter.setQuantifier( f ) ){
+ if( riter.setQuantifier( d_qe, f ) ){
std::vector< RepDomain > dom;
for (unsigned i=0; i<c.getNumChildren(); i++) {
TypeNode tn = c[i].getType();
if( d_rep_ids.find(tn)!=d_rep_ids.end() ){
- RepDomain rd;
+ //RepDomain rd;
if( isStar(c[i]) ){
//add the full range
- for( std::map< Node, int >::iterator it = d_rep_ids[tn].begin();
- it != d_rep_ids[tn].end(); ++it ){
- rd.push_back(it->second);
- }
+ //for( std::map< Node, int >::iterator it = d_rep_ids[tn].begin();
+ // it != d_rep_ids[tn].end(); ++it ){
+ // rd.push_back(it->second);
+ //}
}else{
if (d_rep_ids[tn].find(c[i])!=d_rep_ids[tn].end()) {
- rd.push_back(d_rep_ids[tn][c[i]]);
+ //rd.push_back(d_rep_ids[tn][c[i]]);
+ riter.d_domain[i].clear();
+ riter.d_domain[i].push_back(d_rep_ids[tn][c[i]]);
}else{
return -1;
}
}
- dom.push_back(rd);
+ //dom.push_back(rd);
}else{
return -1;
}
}
- riter.setDomain(dom);
+ //riter.setDomain(dom);
//now do full iteration
while( !riter.isFinished() ){
Trace("fmc-exh-debug") << "Inst : ";
|