From ece17ee2c38fa5769ae3ab7fa3607c0e88c0021f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 8 Aug 2018 17:09:18 -0500 Subject: Disable argument relevance for sygus by default (#2288) --- src/options/quantifiers_options.toml | 8 +++ .../quantifiers/sygus/sygus_process_conj.cpp | 59 +++++++++++++--------- test/regress/regress1/sygus/process-10-vars.sy | 2 +- .../regress/regress2/sygus/process-10-vars-2fun.sy | 2 +- .../regress2/sygus/process-arg-invariance.sy | 2 +- 5 files changed, 45 insertions(+), 28 deletions(-) diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index aac84e92c..5f6638dce 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1175,6 +1175,14 @@ header = "options/quantifiers_options.h" default = "true" help = "use optimized approach for evaluation in sygus" +[[option]] + name = "sygusArgRelevant" + category = "regular" + long = "sygus-arg-relevant" + type = "bool" + default = "false" + help = "static inference techniques for computing whether arguments of functions-to-synthesize are relevant" + # Internal uses of sygus [[option]] diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.cpp b/src/theory/quantifiers/sygus/sygus_process_conj.cpp index 76e484549..b0b6159be 100644 --- a/src/theory/quantifiers/sygus/sygus_process_conj.cpp +++ b/src/theory/quantifiers/sygus/sygus_process_conj.cpp @@ -17,6 +17,7 @@ #include #include "expr/datatype.h" +#include "options/quantifiers_options.h" #include "theory/datatypes/datatypes_rewriter.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" @@ -533,39 +534,43 @@ Node CegConjectureProcess::postSimplify(Node q) Trace("sygus-process") << "Post-simplify conjecture : " << q << std::endl; Assert(q.getKind() == FORALL); - // initialize the information about each function to synthesize - for (unsigned i = 0; i < q[0].getNumChildren(); i++) + if (options::sygusArgRelevant()) { - Node f = q[0][i]; - if (f.getType().isFunction()) + // initialize the information about each function to synthesize + for (unsigned i = 0, size = q[0].getNumChildren(); i < size; i++) { - d_sf_info[f].init(f); + Node f = q[0][i]; + if (f.getType().isFunction()) + { + d_sf_info[f].init(f); + } } - } - // get the base on the conjecture - Node base = q[1]; - std::unordered_set synth_fv; - if (base.getKind() == NOT && base[0].getKind() == FORALL) - { - for (unsigned j = 0; j < base[0][0].getNumChildren(); j++) + // get the base on the conjecture + Node base = q[1]; + std::unordered_set synth_fv; + if (base.getKind() == NOT && base[0].getKind() == FORALL) { - synth_fv.insert(base[0][0][j]); + for (unsigned j = 0, size = base[0][0].getNumChildren(); j < size; j++) + { + synth_fv.insert(base[0][0][j]); + } + base = base[0][1]; } - base = base[0][1]; - } - std::vector conjuncts; - getComponentVector(AND, base, conjuncts); + std::vector conjuncts; + getComponentVector(AND, base, conjuncts); - // process the conjunctions - for (std::map::iterator it = d_sf_info.begin(); - it != d_sf_info.end(); - ++it) - { - Node f = it->first; - for (unsigned i = 0; i < conjuncts.size(); i++) + // process the conjunctions + for (std::map::iterator it = + d_sf_info.begin(); + it != d_sf_info.end(); + ++it) { - processConjunct(conjuncts[i], f, synth_fv); + Node f = it->first; + for (const Node& conj : conjuncts) + { + processConjunct(conj, f, synth_fv); + } } } @@ -587,6 +592,10 @@ void CegConjectureProcess::initialize(Node n, std::vector& candidates) bool CegConjectureProcess::isArgRelevant(Node f, unsigned i) { + if (!options::sygusArgRelevant()) + { + return true; + } std::map::iterator its = d_sf_info.find(f); if (its != d_sf_info.end()) { diff --git a/test/regress/regress1/sygus/process-10-vars.sy b/test/regress/regress1/sygus/process-10-vars.sy index 523abd70d..77990473f 100644 --- a/test/regress/regress1/sygus/process-10-vars.sy +++ b/test/regress/regress1/sygus/process-10-vars.sy @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cegqi-si=none --sygus-out=status +; COMMAND-LINE: --cegqi-si=none --sygus-out=status --sygus-arg-relevant ; EXPECT: unsat (set-logic LIA) diff --git a/test/regress/regress2/sygus/process-10-vars-2fun.sy b/test/regress/regress2/sygus/process-10-vars-2fun.sy index a107fd88b..214da82c8 100644 --- a/test/regress/regress2/sygus/process-10-vars-2fun.sy +++ b/test/regress/regress2/sygus/process-10-vars-2fun.sy @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cegqi-si=none --sygus-out=status --no-sygus-repair-const +; COMMAND-LINE: --cegqi-si=none --sygus-out=status --no-sygus-repair-const --sygus-arg-relevant ; EXPECT: unsat (set-logic LIA) diff --git a/test/regress/regress2/sygus/process-arg-invariance.sy b/test/regress/regress2/sygus/process-arg-invariance.sy index 3c18b6c75..2f1b74ddf 100644 --- a/test/regress/regress2/sygus/process-arg-invariance.sy +++ b/test/regress/regress2/sygus/process-arg-invariance.sy @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cegqi-si=none --sygus-out=status --no-sygus-add-const-grammar +; COMMAND-LINE: --cegqi-si=none --sygus-out=status --no-sygus-add-const-grammar --sygus-arg-relevant ; EXPECT: unsat (set-logic LIA) -- cgit v1.2.3