diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-06-02 12:15:48 -0500 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-06-02 10:15:48 -0700 |
commit | 806f4071423ee1bf8f02f1836843de73faabb952 (patch) | |
tree | c50e9261633d5e31a7beb3b4a7f20b10ddcd641d /src | |
parent | e0e63f746fb0f022fa6594dcc701a2d881155f9b (diff) |
Fix preinitialization pass for finite model finding (#2047)
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/quantifiers/fmf/full_model_check.cpp | 35 | ||||
-rw-r--r-- | src/theory/quantifiers/fmf/full_model_check.h | 19 |
2 files changed, 47 insertions, 7 deletions
diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index e97f716cb..9e77a31c1 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -339,12 +339,14 @@ bool FullModelChecker::preProcessBuildModel(TheoryModel* m) { FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc(); Trace("fmc") << "---Full Model Check preprocess() " << std::endl; + d_preinitialized_eqc.clear(); d_preinitialized_types.clear(); //traverse equality engine eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( fm->d_equalityEngine ); while( !eqcs_i.isFinished() ){ - TypeNode tr = (*eqcs_i).getType(); - d_preinitialized_types[tr] = true; + Node r = *eqcs_i; + TypeNode tr = r.getType(); + d_preinitialized_eqc[tr] = r; ++eqcs_i; } @@ -352,8 +354,10 @@ bool FullModelChecker::preProcessBuildModel(TheoryModel* m) { fm->initialize(); for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) { Node op = it->first; + Trace("fmc") << "preInitialize types for " << op << std::endl; TypeNode tno = op.getType(); for( unsigned i=0; i<tno.getNumChildren(); i++) { + Trace("fmc") << "preInitializeType " << tno[i] << std::endl; preInitializeType( fm, tno[i] ); } } @@ -461,6 +465,8 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){ for( size_t i=0; i<add_conds.size(); i++ ){ Node c = add_conds[i]; Node v = add_values[i]; + Trace("fmc-model-debug") + << "Add cond/value : " << c << " -> " << v << std::endl; std::vector< Node > children; std::vector< Node > entry_children; children.push_back(op); @@ -486,6 +492,8 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){ } Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children ); Node nv = fm->getRepresentative( v ); + Trace("fmc-model-debug") + << "Representative of " << v << " is " << nv << std::endl; if( !nv.isConst() ){ Trace("fmc-warn") << "Warning : model for " << op << " has non-constant value in model " << nv << std::endl; Assert( false ); @@ -562,11 +570,26 @@ void FullModelChecker::preInitializeType( FirstOrderModelFmc * fm, TypeNode tn ) if (!tn.isFunction() || options::ufHo()) { Node mb = fm->getModelBasisTerm(tn); - if (!mb.isConst()) + // if the model basis term does not exist in the model, + // either add it directly to the model's equality engine if no other terms + // of this type exist, or otherwise assert that it is equal to the first + // equivalence class of its type. + if (!fm->hasTerm(mb) && !mb.isConst()) { - Trace("fmc") << "...add model basis term to EE of model " << mb << " " - << tn << std::endl; - fm->d_equalityEngine->addTerm(mb); + std::map<TypeNode, Node>::iterator itpe = d_preinitialized_eqc.find(tn); + if (itpe == d_preinitialized_eqc.end()) + { + Trace("fmc") << "...add model basis term to EE of model " << mb << " " + << tn << std::endl; + fm->d_equalityEngine->addTerm(mb); + } + else + { + Trace("fmc") << "...add model basis eqc equality to model " << mb + << " == " << itpe->second << " " << tn << std::endl; + bool ret = fm->assertEquality(mb, itpe->second, true); + AlwaysAssert(ret); + } } } } diff --git a/src/theory/quantifiers/fmf/full_model_check.h b/src/theory/quantifiers/fmf/full_model_check.h index a64c33303..852f96e4c 100644 --- a/src/theory/quantifiers/fmf/full_model_check.h +++ b/src/theory/quantifiers/fmf/full_model_check.h @@ -93,8 +93,25 @@ protected: std::map< TypeNode, Node > d_array_cond; std::map< Node, Node > d_array_term_cond; std::map< Node, std::vector< int > > d_star_insts; - std::map< TypeNode, bool > d_preinitialized_types; + //--------------------for preinitialization + /** preInitializeType + * + * This function ensures that the model fm is properly initialized with + * respect to type tn. + * + * In particular, this class relies on the use of "model basis" terms, which + * are distinguished terms that are used to specify default values for + * uninterpreted functions. This method enforces that the model basis term + * occurs in the model for each relevant type T, where a type T is relevant + * if a bound variable is of type T, or an uninterpreted function has an + * argument or a return value of type T. + */ void preInitializeType( FirstOrderModelFmc * fm, TypeNode tn ); + /** for each type, an equivalence class of that type from the model */ + std::map<TypeNode, Node> d_preinitialized_eqc; + /** map from types to whether we have called the method above */ + std::map<TypeNode, bool> d_preinitialized_types; + //--------------------end for preinitialization Node normalizeArgReps(FirstOrderModelFmc * fm, Node op, Node n); bool exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index); protected: |