From: Andrew Reynolds Date: Tue, 14 Apr 2020 20:27:33 +0000 (-0500) Subject: Remove a few options (#4295) X-Git-Tag: cvc5-1.0.0~3376 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c3f7c3c9203a355a9c45bf820e3fea0e29b439de;p=cvc5.git Remove a few options (#4295) These options are not robust and are not used. Fixes #4282 and fixes #4291. --- diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 5f07e687e..74b3ceca8 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -641,15 +641,6 @@ header = "options/quantifiers_options.h" read_only = true help = "find models for recursively defined functions, assumes functions are admissible, allows empty type when function is irrelevant" -[[option]] - name = "fmfEmptySorts" - category = "regular" - long = "fmf-empty-sorts" - type = "bool" - default = "false" - read_only = true - help = "allow finite model finding to assume sorts that do not occur in ground assertions are empty" - [[option]] name = "mbqiMode" category = "regular" diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml index 49c304bab..44ca2c390 100644 --- a/src/options/strings_options.toml +++ b/src/options/strings_options.toml @@ -72,15 +72,6 @@ header = "options/strings_options.h" read_only = true help = "strings length normalization lemma" -[[option]] - name = "stringSplitEmp" - category = "regular" - long = "strings-sp-emp" - type = "bool" - default = "true" - read_only = true - help = "strings split on empty string" - [[option]] name = "stringInferSym" category = "regular" diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index 3e5d36a7d..af3a94d96 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -321,13 +321,14 @@ bool FullModelChecker::preProcessBuildModel(TheoryModel* m) { } Trace("fmc") << "Finish preInitialize types" << std::endl; //do not have to introduce terms for sorts of domains of quantified formulas if we are allowed to assume empty sorts - if( !options::fmfEmptySorts() ){ - for( unsigned i=0; igetNumAssertedQuantifiers(); i++ ){ - Node q = fm->getAssertedQuantifier( i ); - //make sure all types are set - for( unsigned j=0; jgetNumAssertedQuantifiers(); i < nquant; + i++) + { + Node q = fm->getAssertedQuantifier(i); + // make sure all types are set + for (const Node& v : q[0]) + { + preInitializeType(fm, v.getType()); } } return true; diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp index 5ae05f2a7..a3dc50dd1 100644 --- a/src/theory/quantifiers/fmf/model_builder.cpp +++ b/src/theory/quantifiers/fmf/model_builder.cpp @@ -47,7 +47,8 @@ bool QModelBuilder::preProcessBuildModel(TheoryModel* m) { bool QModelBuilder::preProcessBuildModelStd(TheoryModel* m) { d_addedLemmas = 0; d_triedLemmas = 0; - if( options::fmfEmptySorts() || options::fmfFunWellDefinedRelevant() ){ + if (options::fmfFunWellDefinedRelevant()) + { FirstOrderModel * fm = (FirstOrderModel*)m; //traverse equality engine std::map< TypeNode, bool > eqc_usort; @@ -63,28 +64,19 @@ bool QModelBuilder::preProcessBuildModelStd(TheoryModel* m) { Node q = fm->getAssertedQuantifier( i, true ); if( fm->isQuantifierActive( q ) ){ //check if any of these quantified formulas can be set inactive - if( options::fmfEmptySorts() ){ - for (const Node& var : q[0]) + if (q[0].getNumChildren() == 1) + { + TypeNode tn = q[0][0].getType(); + if (tn.getAttribute(AbsTypeFunDefAttribute())) { - TypeNode tn = var.getType(); - //we are allowed to assume the type is empty - if( tn.isSort() && eqc_usort.find( tn )==eqc_usort.end() ){ - Trace("model-engine-debug") << "Empty domain quantified formula : " << q << std::endl; + // we are allowed to assume the introduced type is empty + if (eqc_usort.find(tn) == eqc_usort.end()) + { + Trace("model-engine-debug") + << "Irrelevant function definition : " << q << std::endl; fm->setQuantifierActive( q, false ); } } - }else if( options::fmfFunWellDefinedRelevant() ){ - if( q[0].getNumChildren()==1 ){ - TypeNode tn = q[0][0].getType(); - if( tn.getAttribute(AbsTypeFunDefAttribute()) ){ - //Trace("model-engine-debug2") << "...possible irrelevant function def : " << q << ", #rr = " << d_quantEngine->getModel()->d_rep_set.getNumRelevantGroundReps( tn ) << std::endl; - //we are allowed to assume the introduced type is empty - if( eqc_usort.find( tn )==eqc_usort.end() ){ - Trace("model-engine-debug") << "Irrelevant function definition : " << q << std::endl; - fm->setQuantifierActive( q, false ); - } - } - } } } } diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp index f262a2c7d..088bc4a16 100644 --- a/src/theory/strings/inference_manager.cpp +++ b/src/theory/strings/inference_manager.cpp @@ -473,44 +473,41 @@ Node InferenceManager::getRegisterTermAtomicLemma( Assert(s == LENGTH_SPLIT); std::vector lems; - if (options::stringSplitEmp() || !options::stringLenGeqZ()) - { - Node n_len_eq_z = n_len.eqNode(d_zero); - Node n_len_eq_z_2 = n.eqNode(d_emptyString); - Node case_empty = nm->mkNode(AND, n_len_eq_z, n_len_eq_z_2); - case_empty = Rewriter::rewrite(case_empty); - Node case_nempty = nm->mkNode(GT, n_len, d_zero); - if (!case_empty.isConst()) - { - Node lem = nm->mkNode(OR, case_empty, case_nempty); - lems.push_back(lem); - Trace("strings-lemma") - << "Strings::Lemma LENGTH >= 0 : " << lem << std::endl; - // prefer trying the empty case first - // notice that requirePhase must only be called on rewritten literals that - // occur in the CNF stream. - n_len_eq_z = Rewriter::rewrite(n_len_eq_z); - Assert(!n_len_eq_z.isConst()); - reqPhase[n_len_eq_z] = true; - n_len_eq_z_2 = Rewriter::rewrite(n_len_eq_z_2); - Assert(!n_len_eq_z_2.isConst()); - reqPhase[n_len_eq_z_2] = true; - } - else if (!case_empty.getConst()) - { - // the rewriter knows that n is non-empty - Trace("strings-lemma") - << "Strings::Lemma LENGTH > 0 (non-empty): " << case_nempty - << std::endl; - lems.push_back(case_nempty); - } - else - { - // If n = "" ---> true or len( n ) = 0 ----> true, then we expect that - // n ---> "". Since this method is only called on non-constants n, it must - // be that n = "" ^ len( n ) = 0 does not rewrite to true. - Assert(false); - } + // split whether the string is empty + Node n_len_eq_z = n_len.eqNode(d_zero); + Node n_len_eq_z_2 = n.eqNode(d_emptyString); + Node case_empty = nm->mkNode(AND, n_len_eq_z, n_len_eq_z_2); + case_empty = Rewriter::rewrite(case_empty); + Node case_nempty = nm->mkNode(GT, n_len, d_zero); + if (!case_empty.isConst()) + { + Node lem = nm->mkNode(OR, case_empty, case_nempty); + lems.push_back(lem); + Trace("strings-lemma") << "Strings::Lemma LENGTH >= 0 : " << lem + << std::endl; + // prefer trying the empty case first + // notice that requirePhase must only be called on rewritten literals that + // occur in the CNF stream. + n_len_eq_z = Rewriter::rewrite(n_len_eq_z); + Assert(!n_len_eq_z.isConst()); + reqPhase[n_len_eq_z] = true; + n_len_eq_z_2 = Rewriter::rewrite(n_len_eq_z_2); + Assert(!n_len_eq_z_2.isConst()); + reqPhase[n_len_eq_z_2] = true; + } + else if (!case_empty.getConst()) + { + // the rewriter knows that n is non-empty + Trace("strings-lemma") << "Strings::Lemma LENGTH > 0 (non-empty): " + << case_nempty << std::endl; + lems.push_back(case_nempty); + } + else + { + // If n = "" ---> true or len( n ) = 0 ----> true, then we expect that + // n ---> "". Since this method is only called on non-constants n, it must + // be that n = "" ^ len( n ) = 0 does not rewrite to true. + Assert(false); } // additionally add len( x ) >= 0 ?