diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-03-07 12:39:50 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-03-07 12:39:50 -0600 |
| commit | b4c7be882b88c6741212ecd9c6be4e91fec76087 (patch) | |
| tree | 0f96427e0e6f84ff6ac60ac81ff6f13459515295 /src/theory/quantifiers/full_model_check.cpp | |
| parent | ea514f2aa787998ac31f8546bd202890f6bac056 (diff) | |
Minor change to F-Length inference in strings. No internal tracking of cardinality assertions in uf. Change fullModel false array collectModelInfo to assign constants.
Diffstat (limited to 'src/theory/quantifiers/full_model_check.cpp')
| -rw-r--r-- | src/theory/quantifiers/full_model_check.cpp | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index e44a322b5..98cd175fd 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -461,7 +461,7 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ } } if( !isStar && !ri.isConst() ){ - Trace("fmc-warn") << "Warning : model has non-constant argument in model " << ri << " (from " << c[i] << ")" << std::endl; + Trace("fmc-warn") << "Warning : model for " << op << " has non-constant argument in model " << ri << " (from " << c[i] << ")" << std::endl; Assert( false ); } entry_children.push_back(ri); @@ -469,7 +469,7 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children ); Node nv = fm->getUsedRepresentative( v ); if( !nv.isConst() ){ - Trace("fmc-warn") << "Warning : model has non-constant value in model " << nv << std::endl; + Trace("fmc-warn") << "Warning : model for " << op << " has non-constant value in model " << nv << std::endl; Assert( false ); } Node en = (useSimpleModels() && hasNonStar) ? n : NodeManager::currentNM()->mkNode( APPLY_UF, entry_children ); @@ -690,10 +690,12 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, }else{ Trace("fmc-debug-inst") << "** Instantiation was duplicate." << std::endl; //this can happen if evaluation is unknown, or if we are generalizing a star that already has a value - if( !hasStar && d_quant_models[f].d_value[i]==d_false ){ - Trace("fmc-warn") << "**** FMC warning: inconsistent duplicate instantiation." << std::endl; - } - Assert( hasStar || d_quant_models[f].d_value[i]!=d_false ); + //if( !hasStar && d_quant_models[f].d_value[i]==d_false ){ + // Trace("fmc-warn") << "**** FMC warning: inconsistent duplicate instantiation." << std::endl; + //} + //this assertion can happen if two instantiations from this round are identical + // (0,1)->false (1,0)->false for forall xy. f( x, y ) = f( y, x ) + //Assert( hasStar || d_quant_models[f].d_value[i]!=d_false ); //might try it next effort level d_star_insts[f].push_back(i); } |