From: Andrew Reynolds Date: Sat, 2 Jun 2018 17:15:48 +0000 (-0500) Subject: Fix preinitialization pass for finite model finding (#2047) X-Git-Tag: cvc5-1.0.0~4985 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=806f4071423ee1bf8f02f1836843de73faabb952;p=cvc5.git Fix preinitialization pass for finite model finding (#2047) --- 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::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 " << 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::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 d_preinitialized_eqc; + /** map from types to whether we have called the method above */ + std::map 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: diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index d235f27d3..0e0cee7f8 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1085,6 +1085,7 @@ REG1_TESTS = \ regress1/fmf/german169.smt2 \ regress1/fmf/german73.smt2 \ regress1/fmf/issue916-fmf-or.smt2 \ + regress1/fmf/issue2034-preinit.smt2 \ regress1/fmf/jasmin-cdt-crash.smt2 \ regress1/fmf/ko-bound-set.cvc \ regress1/fmf/loopy_coda.smt2 \ @@ -1589,7 +1590,6 @@ REG2_TESTS = \ regress2/ooo.tag10.smt2 \ regress2/piVC_5581bd.smt2 \ regress2/quantifiers/AdditiveMethods_AdditiveMethods..ctor.smt2 \ - regress2/quantifiers/ForElimination-scala-9.smt2 \ regress2/quantifiers/javafe.ast.ArrayInit.35.smt2 \ regress2/quantifiers/javafe.ast.StandardPrettyPrint.319.smt2 \ regress2/quantifiers/javafe.ast.WhileStmt.447.smt2 \ @@ -1958,6 +1958,7 @@ DISABLED_TESTS = \ regress2/bug396.smt2 \ regress2/nl/dumortier-050317.smt2 \ regress2/nl/nt-lemmas-bad.smt2 \ + regress2/quantifiers/ForElimination-scala-9.smt2 \ regress2/quantifiers/small-bug1-fixpoint-3.smt2 \ regress2/xs-11-20-5-2-5-3.smt \ regress2/xs-11-20-5-2-5-3.smt2 diff --git a/test/regress/regress1/fmf/issue2034-preinit.smt2 b/test/regress/regress1/fmf/issue2034-preinit.smt2 new file mode 100644 index 000000000..e80e698fd --- /dev/null +++ b/test/regress/regress1/fmf/issue2034-preinit.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --finite-model-find +; EXPECT: unknown +(set-logic AUFLIRA) +(set-info :status unknown) +(declare-fun _substvar_1_ () Int) +(declare-fun tptp_const_array1 (Int Real) (Array Int Real)) +(assert (forall ((?I_4 Int) (?L_5 Int) (?U_6 Int) (?Val_7 Real)) (=> true (= (select (tptp_const_array1 _substvar_1_ ?Val_7) 0) ?Val_7)))) +(check-sat) \ No newline at end of file