diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-11 14:36:50 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-11 14:36:50 -0500 |
commit | 0b2f9943d55152e0958369083649dd71340864c9 (patch) | |
tree | cd040f1dd12816c6af37548597bd674cafb45271 /src/theory/quantifiers/full_model_check.cpp | |
parent | 8ebd49cb903ba19f9330820d02af08e226c9b791 (diff) |
More preparation for CASC proofs. Minor fix for sort inference (rewrite new assertions). Bug fix for ambqi : simplify correctly for multi-sorted case. Bug fix for fmc : only do exh-simplification for uninterpreted sorts, ensure reps are enumerated for quantification over Real.
Diffstat (limited to 'src/theory/quantifiers/full_model_check.cpp')
-rw-r--r-- | src/theory/quantifiers/full_model_check.cpp | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index 0f3e53827..63df56392 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -61,7 +61,7 @@ bool EntryTrie::hasGeneralization( FirstOrderModelFmc * m, Node c, int index ) { return true; } } - if( options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL || !c[index].getType().isInteger() ){ + if( c[index].getType().isSort() ){ //for star: check if all children are defined and have generalizations if( c[index]==st ){ ///options::fmfFmcCoverSimplify() //check if all children exist and are complete @@ -537,7 +537,9 @@ void FullModelChecker::initializeType( FirstOrderModelFmc * fm, TypeNode tn ){ }else{ mbn = d_qe->getTermDatabase()->getModelBasisTerm(tn); } + Trace("fmc") << "Get used rep for " << mbn << std::endl; Node mbnr = fm->getUsedRepresentative( mbn ); + Trace("fmc") << "...got " << mbnr << std::endl; fm->d_model_basis_rep[tn] = mbnr; Trace("fmc") << "Add model basis for type " << tn << " : " << mbn << " " << mbnr << std::endl; } |