diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-01-20 16:55:02 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-01-20 16:55:02 -0600 |
commit | 7006d5ba2f68c01638a2ab2c98a86b41dcf4467c (patch) | |
tree | ecb2f69f3cbe1a2cabde21a9e9e4e08691c2b734 /src | |
parent | bbcf8ccc012caf6ad54b7ec2b91a9886fb6021e6 (diff) |
Fix bug in fmc mbqi where modelscomputed for mbqi could involve non-constant values. Add regression.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/quantifiers/first_order_model.cpp | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/full_model_check.cpp | 2 |
2 files changed, 5 insertions, 0 deletions
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 027a4573b..018a0c3e0 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -574,6 +574,7 @@ Node FirstOrderModelFmc::getUsedRepresentative(Node n, bool strict) { Trace("fmc-warn") << "WARNING : no representative for " << n << std::endl; } } +/* Node r = getRepresentative(n); if( d_model_basis_rep.find(tn)!=d_model_basis_rep.end() ){ if (r==d_model_basis_rep[tn]) { @@ -581,6 +582,8 @@ Node FirstOrderModelFmc::getUsedRepresentative(Node n, bool strict) { } } return r; +*/ + return getRepresentative(n); } } diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index 02c6bbba8..f0858f4e9 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -436,6 +436,7 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ Node ri = fm->getUsedRepresentative( c[i]); if( !ri.getType().isSort() && !ri.isConst() ){ Trace("fmc-warn") << "Warning : model has non-constant argument in model " << ri << std::endl; + Assert( false ); } children.push_back(ri); if( options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL || !ri.getType().isInteger() ){ @@ -451,6 +452,7 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ Node nv = fm->getUsedRepresentative( v ); if( !nv.getType().isSort() && !nv.isConst() ){ Trace("fmc-warn") << "Warning : model has non-constant value in model " << nv << std::endl; + Assert( false ); } Node en = (useSimpleModels() && hasNonStar) ? n : NodeManager::currentNM()->mkNode( APPLY_UF, entry_children ); if( std::find(conds.begin(), conds.end(), n )==conds.end() ){ |