From e4926117ce53433e59f4b1a86892ea43a01f709d Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 2 Jun 2020 12:22:17 -0500 Subject: [PATCH] Do not handle universal quantification on functions in model-based FMF (#4226) Fixes #4225, fixes CVC4/cvc4-projects#159, fixes CVC4/cvc4-projects#157, fixes #4289, fixes #4483. This makes it so that the main model-based instantiation algorithm is not applied to quantified formulas with universally quantified functions. Identation changed in a FMF function, this was refactored to conform to guidelines, and further cleaned. --- .../quantifiers/fmf/full_model_check.cpp | 295 +++++++++++------- src/theory/quantifiers/fmf/full_model_check.h | 19 ++ test/regress/CMakeLists.txt | 1 + .../regress1/fmf/issue4225-univ-fun.smt2 | 6 + 4 files changed, 203 insertions(+), 118 deletions(-) create mode 100644 test/regress/regress1/fmf/issue4225-univ-fun.smt2 diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index af3a94d96..91cacdc2e 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -592,139 +592,168 @@ void FullModelChecker::debugPrint(const char * tr, Node n, bool dispStar) { int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { Trace("fmc") << "Full model check " << f << ", effort = " << effort << "..." << std::endl; + // register the quantifier + registerQuantifiedFormula(f); Assert(!d_qe->inConflict()); - if( optUseModel() ){ - FirstOrderModelFmc * fmfmc = fm->asFirstOrderModelFmc(); - if (effort==0) { - //register the quantifier - if (d_quant_cond.find(f)==d_quant_cond.end()) { - std::vector< TypeNode > types; - for(unsigned i=0; iasFirstOrderModelFmc(); + if (effort == 0) + { + if (options::mbqiMode() == options::MbqiMode::NONE) + { + // just exhaustive instantiate + Node c = mkCondDefault(fmfmc, f); + d_quant_models[f].addEntry(fmfmc, c, d_false); + if (!exhaustiveInstantiate(fmfmc, f, c, -1)) + { + return 0; + } + return 1; + } + // model check the quantifier + doCheck(fmfmc, f, d_quant_models[f], f[1]); + std::vector& mcond = d_quant_models[f].d_cond; + Trace("fmc") << "Definition for quantifier " << f << " is : " << std::endl; + Assert(!mcond.empty()); + d_quant_models[f].debugPrint("fmc", Node::null(), this); + Trace("fmc") << std::endl; + + // consider all entries going to non-true + Instantiate* instq = d_qe->getInstantiate(); + for (unsigned i = 0, msize = mcond.size(); i < msize; i++) + { + if (d_quant_models[f].d_value[i] == d_true) + { + // already satisfied + continue; + } + Trace("fmc-inst") << "Instantiate based on " << mcond[i] << "..." + << std::endl; + bool hasStar = false; + std::vector inst; + for (unsigned j = 0, nchild = mcond[i].getNumChildren(); j < nchild; j++) + { + if (fmfmc->isStar(mcond[i][j])) + { + hasStar = true; + inst.push_back(fmfmc->getModelBasisTerm(mcond[i][j].getType())); + } + else + { + inst.push_back(mcond[i][j]); } - TypeNode typ = NodeManager::currentNM()->mkFunctionType( types, NodeManager::currentNM()->booleanType() ); - Node op = NodeManager::currentNM()->mkSkolem( "qfmc", typ, "op created for full-model checking" ); - d_quant_cond[f] = op; } - - if (options::mbqiMode() == options::MbqiMode::NONE) + bool addInst = true; + if (hasStar) { - //just exhaustive instantiate - Node c = mkCondDefault( fmfmc, f ); - d_quant_models[f].addEntry( fmfmc, c, d_false ); - return exhaustiveInstantiate( fmfmc, f, c, -1); + // try obvious (specified by inst) + Node ev = d_quant_models[f].evaluate(fmfmc, inst); + if (ev == d_true) + { + addInst = false; + Trace("fmc-debug") + << "...do not instantiate, evaluation was " << ev << std::endl; + } } else { - //model check the quantifier - doCheck(fmfmc, f, d_quant_models[f], f[1]); - Trace("fmc") << "Definition for quantifier " << f << " is : " << std::endl; - Assert(!d_quant_models[f].d_cond.empty()); - d_quant_models[f].debugPrint("fmc", Node::null(), this); - Trace("fmc") << std::endl; - - //consider all entries going to non-true - for (unsigned i=0; i inst; - for (unsigned j=0; jisStar(d_quant_models[f].d_cond[i][j])) { - hasStar = true; - inst.push_back(fmfmc->getModelBasisTerm(d_quant_models[f].d_cond[i][j].getType())); - }else{ - inst.push_back(d_quant_models[f].d_cond[i][j]); - } - } - bool addInst = true; - if( hasStar ){ - //try obvious (specified by inst) - Node ev = d_quant_models[f].evaluate(fmfmc, inst); - if (ev==d_true) { - addInst = false; - Trace("fmc-debug") << "...do not instantiate, evaluation was " << ev << std::endl; - } - }else{ - //for debugging - if (Trace.isOn("fmc-test-inst")) { - Node ev = d_quant_models[f].evaluate(fmfmc, inst); - if( ev==d_true ){ - Message() << "WARNING: instantiation was true! " << f << " " - << d_quant_models[f].d_cond[i] << std::endl; - AlwaysAssert(false); - }else{ - Trace("fmc-test-inst") << "...instantiation evaluated to false." << std::endl; - } - } - } - if( addInst ){ - if( options::fmfBound() ){ - std::vector< Node > cond; - cond.push_back(d_quant_cond[f]); - cond.insert( cond.end(), inst.begin(), inst.end() ); - //need to do exhaustive instantiate algorithm to set things properly (should only add one instance) - Node c = mkCond( cond ); - unsigned prevInst = d_addedLemmas; - exhaustiveInstantiate( fmfmc, f, c, -1 ); - if( d_addedLemmas==prevInst ){ - d_star_insts[f].push_back(i); - } - }else{ - //just add the instance - d_triedLemmas++; - if (d_qe->getInstantiate()->addInstantiation(f, inst, true)) - { - Trace("fmc-debug-inst") << "** Added instantiation." << std::endl; - d_addedLemmas++; - if( d_qe->inConflict() || options::fmfOneInstPerRound() ){ - break; - } - }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; - //} - //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); - } - } - }else{ - Trace("fmc-debug-inst") << "** Instantiation was already true." << std::endl; - //might try it next effort level - d_star_insts[f].push_back(i); - } + // for debugging + if (Trace.isOn("fmc-test-inst")) + { + Node ev = d_quant_models[f].evaluate(fmfmc, inst); + if (ev == d_true) + { + Message() << "WARNING: instantiation was true! " << f << " " + << mcond[i] << std::endl; + AlwaysAssert(false); + } + else + { + Trace("fmc-test-inst") + << "...instantiation evaluated to false." << std::endl; } } } - }else{ - if (!d_star_insts[f].empty()) { - Trace("fmc-exh") << "Exhaustive instantiate " << f << std::endl; - Trace("fmc-exh") << "Definition was : " << std::endl; - d_quant_models[f].debugPrint("fmc-exh", Node::null(), this); - Trace("fmc-exh") << std::endl; - Def temp; - //simplify the exceptions? - for( int i=(d_star_insts[f].size()-1); i>=0; i--) { - //get witness for d_star_insts[f][i] - int j = d_star_insts[f][i]; - if( temp.addEntry(fmfmc, d_quant_models[f].d_cond[j], d_quant_models[f].d_value[j] ) ){ - if( !exhaustiveInstantiate(fmfmc, f, d_quant_models[f].d_cond[j], j ) ){ - //something went wrong, resort to exhaustive instantiation - return 0; - } - } + if (!addInst) + { + Trace("fmc-debug-inst") + << "** Instantiation was already true." << std::endl; + // might try it next effort level + d_star_insts[f].push_back(i); + continue; + } + if (options::fmfBound()) + { + std::vector cond; + cond.push_back(d_quant_cond[f]); + cond.insert(cond.end(), inst.begin(), inst.end()); + // need to do exhaustive instantiate algorithm to set things properly + // (should only add one instance) + Node c = mkCond(cond); + unsigned prevInst = d_addedLemmas; + exhaustiveInstantiate(fmfmc, f, c, -1); + if (d_addedLemmas == prevInst) + { + d_star_insts[f].push_back(i); } + continue; + } + // just add the instance + d_triedLemmas++; + if (instq->addInstantiation(f, inst, true)) + { + Trace("fmc-debug-inst") << "** Added instantiation." << std::endl; + d_addedLemmas++; + if (d_qe->inConflict() || options::fmfOneInstPerRound()) + { + break; + } + } + else + { + Trace("fmc-debug-inst") + << "** Instantiation was duplicate." << std::endl; + // might try it next effort level + d_star_insts[f].push_back(i); } } return 1; - }else{ - return 0; } + // Get the list of instantiation regions (described by "star entries" in the + // definition) that were not tried at the previous effort level. For each + // of these, we add one instantiation. + std::vector& mcond = d_quant_models[f].d_cond; + if (!d_star_insts[f].empty()) + { + if (Trace.isOn("fmc-exh")) + { + Trace("fmc-exh") << "Exhaustive instantiate " << f << std::endl; + Trace("fmc-exh") << "Definition was : " << std::endl; + d_quant_models[f].debugPrint("fmc-exh", Node::null(), this); + Trace("fmc-exh") << std::endl; + } + Def temp; + // simplify the exceptions? + for (int i = (d_star_insts[f].size() - 1); i >= 0; i--) + { + // get witness for d_star_insts[f][i] + int j = d_star_insts[f][i]; + if (temp.addEntry(fmfmc, mcond[j], d_quant_models[f].d_value[j])) + { + if (!exhaustiveInstantiate(fmfmc, f, mcond[j], j)) + { + // something went wrong, resort to exhaustive instantiation + return 0; + } + } + } + } + return 1; } /** Representative bound fmc entry @@ -1290,3 +1319,33 @@ Node FullModelChecker::getFunctionValue(FirstOrderModelFmc * fm, Node op, const bool FullModelChecker::useSimpleModels() { return options::fmfFmcSimple(); } + +void FullModelChecker::registerQuantifiedFormula(Node q) +{ + if (d_quant_cond.find(q) != d_quant_cond.end()) + { + return; + } + NodeManager* nm = NodeManager::currentNM(); + std::vector types; + for (const Node& v : q[0]) + { + TypeNode tn = v.getType(); + if (tn.isFunction()) + { + // we will not use model-based quantifier instantiation for q, since + // the model-based instantiation algorithm does not handle (universally + // quantified) functions + d_unhandledQuant.insert(q); + } + types.push_back(tn); + } + TypeNode typ = nm->mkFunctionType(types, nm->booleanType()); + Node op = nm->mkSkolem("qfmc", typ, "op for full-model checking"); + d_quant_cond[q] = op; +} + +bool FullModelChecker::isHandled(Node q) const +{ + return d_unhandledQuant.find(q) == d_unhandledQuant.end(); +} diff --git a/src/theory/quantifiers/fmf/full_model_check.h b/src/theory/quantifiers/fmf/full_model_check.h index 7dd1991f5..60de5d1eb 100644 --- a/src/theory/quantifiers/fmf/full_model_check.h +++ b/src/theory/quantifiers/fmf/full_model_check.h @@ -86,7 +86,16 @@ protected: Node d_false; std::map > d_rep_ids; std::map d_quant_models; + /** + * The predicate for the quantified formula. This is used to express + * conditions under which the quantified formula is false in the model. + * For example, for quantified formula (forall x:Int, y:U. P), this is + * a predicate of type (Int x U) -> Bool. + */ std::map d_quant_cond; + /** A set of quantified formulas that cannot be handled by model-based + * quantifier instantiation */ + std::unordered_set d_unhandledQuant; std::map< TypeNode, Node > d_array_cond; std::map< Node, Node > d_array_term_cond; std::map< Node, std::vector< int > > d_star_insts; @@ -155,6 +164,16 @@ public: bool processBuildModel(TheoryModel* m) override; bool useSimpleModels(); + + private: + /** + * Register quantified formula. + * This checks whether q can be handled by model-based instantiation and + * initializes the necessary information if so. + */ + void registerQuantifiedFormula(Node q); + /** Is quantified formula q handled by model-based instantiation? */ + bool isHandled(Node q) const; };/* class FullModelChecker */ }/* CVC4::theory::quantifiers::fmcheck namespace */ diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 0f1b090d4..2b587c93a 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1315,6 +1315,7 @@ set(regress_1_tests regress1/fmf/issue3626.smt2 regress1/fmf/issue3689.smt2 regress1/fmf/issue4068-si-qf.smt2 + regress1/fmf/issue4225-univ-fun.smt2 regress1/fmf/issue916-fmf-or.smt2 regress1/fmf/jasmin-cdt-crash.smt2 regress1/fmf/ko-bound-set.cvc diff --git a/test/regress/regress1/fmf/issue4225-univ-fun.smt2 b/test/regress/regress1/fmf/issue4225-univ-fun.smt2 new file mode 100644 index 000000000..9946a4567 --- /dev/null +++ b/test/regress/regress1/fmf/issue4225-univ-fun.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --finite-model-find --uf-ho +; EXPECT: unknown +(set-logic ALL) +; this is not handled by fmf +(assert (forall ((a (-> Int Int)) (b Int)) (not (= (a b) 0)))) +(check-sat) -- 2.30.2