From 442ab0cdd8578631974318c17dd8ace59d145839 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 13 Mar 2020 14:53:00 -0500 Subject: [PATCH] Removing a few deprecated options (#4052) --- src/options/datatypes_options.toml | 9 --- src/options/quantifiers_options.toml | 63 ------------------- src/options/strings_options.toml | 20 ------ src/theory/datatypes/sygus_extension.cpp | 37 ++--------- src/theory/quantifiers/fmf/model_engine.cpp | 8 +-- src/theory/quantifiers/fmf/model_engine.h | 3 - .../sygus/ce_guided_single_inv.cpp | 9 +-- src/theory/quantifiers/sygus/cegis.cpp | 3 +- src/theory/strings/core_solver.cpp | 30 ++++----- 9 files changed, 25 insertions(+), 157 deletions(-) diff --git a/src/options/datatypes_options.toml b/src/options/datatypes_options.toml index 7eb9d30c5..82e833506 100644 --- a/src/options/datatypes_options.toml +++ b/src/options/datatypes_options.toml @@ -119,15 +119,6 @@ header = "options/datatypes_options.h" type = "bool" default = "true" help = "sygus symmetry breaking lemmas based on pbe conjectures" - -[[option]] - name = "sygusOpt1" - category = "regular" - long = "sygus-opt1" - type = "bool" - default = "false" - read_only = true - help = "sygus experimental option" [[option]] name = "sygusSymBreakLazy" diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 6e0460ae9..12549152d 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -676,15 +676,6 @@ header = "options/quantifiers_options.h" default = "false" help = "only add one instantiation per quantifier per round for mbqi" -[[option]] - name = "fmfOneQuantPerRound" - category = "regular" - long = "mbqi-one-quant-per-round" - type = "bool" - default = "false" - read_only = true - help = "only add instantiations for one quantifier per round for mbqi" - [[option]] name = "mbqiInterleave" category = "regular" @@ -702,24 +693,6 @@ header = "options/quantifiers_options.h" default = "false" help = "use instantiation engine in conjunction with finite model finding" -[[option]] - name = "fmfInstGen" - category = "regular" - long = "fmf-inst-gen" - type = "bool" - default = "true" - read_only = true - help = "enable Inst-Gen instantiation techniques for finite model finding" - -[[option]] - name = "fmfInstGenOneQuantPerRound" - category = "regular" - long = "fmf-inst-gen-one-quant-per-round" - type = "bool" - default = "false" - read_only = true - help = "only perform Inst-Gen instantiation techniques on one quantifier per round" - [[option]] name = "fmfFreshDistConst" category = "regular" @@ -870,14 +843,6 @@ header = "options/quantifiers_options.h" default = "false" help = "do not consider instances of quantified formulas that are currently true in model, if it is available" -[[option]] - name = "instPropagate" - category = "regular" - long = "inst-prop" - type = "bool" - default = "false" - help = "internal propagation for instantiations for selecting relevant instances" - [[option]] name = "qcfEagerTest" category = "regular" @@ -905,17 +870,6 @@ header = "options/quantifiers_options.h" read_only = true help = "optimization, skip instances based on possibly irrelevant portions of quantified formulas" -### Rewrite rules options - -[[option]] - name = "rrOneInstPerRound" - category = "regular" - long = "rr-one-inst-per-round" - type = "bool" - default = "false" - read_only = true - help = "add one instance of rewrite rule per round" - ### Induction options [[option]] @@ -1377,15 +1331,6 @@ header = "options/quantifiers_options.h" read_only = true help = "do unfolding of Boolean evaluation functions that appear in refinement lemmas" -[[option]] - name = "sygusRefEval" - category = "regular" - long = "sygus-ref-eval" - type = "bool" - default = "true" - read_only = true - help = "direct evaluation of refinement lemmas for conflict analysis" - [[option]] name = "sygusStream" category = "regular" @@ -1428,14 +1373,6 @@ header = "options/quantifiers_options.h" name = "trust" help = "Trust that when a solution for a conjecture is always true under sampling, then it is indeed a solution. Note this option may print out spurious solutions for synthesis conjectures." -[[option]] - name = "minSynthSol" - category = "regular" - long = "min-synth-sol" - type = "bool" - default = "true" - help = "Minimize synthesis solutions" - [[option]] name = "sygusEvalOpt" category = "regular" diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml index f51c4ce67..49c304bab 100644 --- a/src/options/strings_options.toml +++ b/src/options/strings_options.toml @@ -10,17 +10,6 @@ header = "options/strings_options.h" default = "false" help = "experimental features in the theory of strings" -[[option]] - name = "stringLB" - smt_name = "strings-lb" - category = "regular" - long = "strings-lb=N" - type = "unsigned" - default = "0" - predicates = ["unsignedLessEqual2"] - read_only = true - help = "the strategy of LB rule application: 0-lazy, 1-eager, 2-no" - [[option]] name = "stdPrintASCII" category = "regular" @@ -47,15 +36,6 @@ header = "options/strings_options.h" read_only = true help = "strings eager check" -[[option]] - name = "stringEIT" - category = "regular" - long = "strings-eit" - type = "bool" - default = "false" - read_only = true - help = "the eager intersection used by the theory of strings" - [[option]] name = "stringIgnNegMembership" category = "regular" diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp index 24288216f..d962ad189 100644 --- a/src/theory/datatypes/sygus_extension.cpp +++ b/src/theory/datatypes/sygus_extension.cpp @@ -130,39 +130,10 @@ void SygusExtension::assertFact( Node n, bool polarity, std::vector< Node >& lem Node SygusExtension::getTermOrderPredicate( Node n1, Node n2 ) { NodeManager* nm = NodeManager::currentNM(); std::vector< Node > comm_disj; - // (1) size of left is greater than size of right - Node sz_less = - nm->mkNode(GT, nm->mkNode(DT_SIZE, n1), nm->mkNode(DT_SIZE, n2)); - comm_disj.push_back( sz_less ); - // (2) ...or sizes are equal and first child is less by term order - std::vector sz_eq_cases; - Node sz_eq = - nm->mkNode(EQUAL, nm->mkNode(DT_SIZE, n1), nm->mkNode(DT_SIZE, n2)); - sz_eq_cases.push_back( sz_eq ); - if( options::sygusOpt1() ){ - TypeNode tnc = n1.getType(); - const DType& cdt = tnc.getDType(); - for( unsigned j=0; j case_conj; - for (unsigned k = 0; k < j; k++) - { - case_conj.push_back(utils::mkTester(n2, k, cdt).negate()); - } - if (!case_conj.empty()) - { - Node corder = nm->mkNode( - OR, - utils::mkTester(n1, j, cdt).negate(), - case_conj.size() == 1 ? case_conj[0] : nm->mkNode(AND, case_conj)); - sz_eq_cases.push_back(corder); - } - } - } - Node sz_eqc = sz_eq_cases.size() == 1 ? sz_eq_cases[0] - : nm->mkNode(kind::AND, sz_eq_cases); - comm_disj.push_back( sz_eqc ); - - return nm->mkNode(kind::OR, comm_disj); + // size of left is greater than or equal to the size of right + Node szGeq = + nm->mkNode(GEQ, nm->mkNode(DT_SIZE, n1), nm->mkNode(DT_SIZE, n2)); + return szGeq; } void SygusExtension::registerTerm( Node n, std::vector< Node >& lemmas ) { diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index 5b2931e42..4012f687f 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -163,11 +163,6 @@ void ModelEngine::assertNode( Node f ){ } -bool ModelEngine::optOneQuantPerRound(){ - return options::fmfOneQuantPerRound(); -} - - int ModelEngine::checkModel(){ FirstOrderModel* fm = d_quantEngine->getModel(); @@ -230,7 +225,8 @@ int ModelEngine::checkModel(){ //determine if we should check this quantifier if( d_quantEngine->getModel()->isQuantifierActive( q ) && d_quantEngine->hasOwnership( q, this ) ){ exhaustiveInstantiate( q, e ); - if( d_quantEngine->inConflict() || ( optOneQuantPerRound() && d_addedLemmas>0 ) ){ + if (d_quantEngine->inConflict()) + { break; } }else{ diff --git a/src/theory/quantifiers/fmf/model_engine.h b/src/theory/quantifiers/fmf/model_engine.h index b39dd03f8..3165b01db 100644 --- a/src/theory/quantifiers/fmf/model_engine.h +++ b/src/theory/quantifiers/fmf/model_engine.h @@ -28,9 +28,6 @@ namespace quantifiers { class ModelEngine : public QuantifiersModule { friend class RepSetIterator; -private: - //options - bool optOneQuantPerRound(); private: //check model int checkModel(); diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index f81d2455c..2e5a834b1 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -556,12 +556,9 @@ Node CegSingleInv::reconstructToSyntax(Node s, }else{ Trace("csi-sol") << "Post-process solution..." << std::endl; Node prev = d_solution; - if (options::minSynthSol()) - { - d_solution = - d_qe->getTermDatabaseSygus()->getExtRewriter()->extendedRewrite( - d_solution); - } + d_solution = + d_qe->getTermDatabaseSygus()->getExtRewriter()->extendedRewrite( + d_solution); if( prev!=d_solution ){ Trace("csi-sol") << "Solution (after post process) : " << d_solution << std::endl; } diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index 3ef3a3edc..57fe40517 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -136,8 +136,7 @@ bool Cegis::addEvalLemmas(const std::vector& candidates, bool addedEvalLemmas = false; // Refinement evaluation should not be done for grammars with symbolic // constructors. - bool doRefEval = options::sygusRefEval() && !d_usingSymCons; - if (doRefEval) + if (!d_usingSymCons) { Trace("cegqi-engine") << " *** Do refinement lemma evaluation" << (doGen ? " with conjecture-specific refinement" diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index e2cafa4d3..723a8c08e 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -1484,22 +1484,22 @@ bool CoreSolver::detectLoop(NormalForm& nfi, unsigned rproc) { int has_loop[2] = { -1, -1 }; - if( options::stringLB() != 2 ) { - for( unsigned r=0; r<2; r++ ) { - NormalForm& nf = r == 0 ? nfi : nfj; - NormalForm& nfo = r == 0 ? nfj : nfi; - std::vector& nfv = nf.d_nf; - std::vector& nfov = nfo.d_nf; - if (!nfov[index].isConst()) + for (unsigned r = 0; r < 2; r++) + { + NormalForm& nf = r == 0 ? nfi : nfj; + NormalForm& nfo = r == 0 ? nfj : nfi; + std::vector& nfv = nf.d_nf; + std::vector& nfov = nfo.d_nf; + if (nfov[index].isConst()) + { + continue; + } + for (unsigned lp = index + 1, lpEnd = nfv.size() - rproc; lp < lpEnd; lp++) + { + if (nfv[lp] == nfov[index]) { - for (unsigned lp = index + 1; lp < nfv.size() - rproc; lp++) - { - if (nfv[lp] == nfov[index]) - { - has_loop[r] = lp; - break; - } - } + has_loop[r] = lp; + break; } } } -- 2.30.2