diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-12-02 11:12:10 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-12-02 17:12:10 +0000 |
commit | 4270c3d6b8fa45e66a79c928267a0757954d8004 (patch) | |
tree | ce94eadad454d448cf0da2e42d5b1c9cca5ac0d2 | |
parent | 9d563b2963835b2a4e6ab19bdf5a5b21d934416e (diff) |
Fixes for sygus-rr-synth-input (#7716)
Includes aborting when no non-constant subterms exist, a spurious assertion failure, and bad variable names.
Fixes cvc5/cvc5-projects#351
Fixes cvc5/cvc5-projects#353
-rw-r--r-- | src/preprocessing/passes/synth_rew_rules.cpp | 21 |
1 files changed, 15 insertions, 6 deletions
diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp index a54d220e5..4adfa1fd6 100644 --- a/src/preprocessing/passes/synth_rew_rules.cpp +++ b/src/preprocessing/passes/synth_rew_rules.cpp @@ -146,13 +146,13 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal( Trace("srs-input") << "Make synth variables for types..." << std::endl; // We will generate a fixed number of variables per type. These are the // variables that appear as free variables in the rewrites we generate. - unsigned nvars = options().quantifiers.sygusRewSynthInputNVars; + uint64_t nvars = options().quantifiers.sygusRewSynthInputNVars; // must have at least one variable per type nvars = nvars < 1 ? 1 : nvars; std::map<TypeNode, std::vector<Node> > tvars; std::vector<TypeNode> allVarTypes; std::vector<Node> allVars; - unsigned varCounter = 0; + uint64_t varCounter = 0; for (std::pair<const TypeNode, bool> tfp : typesFound) { TypeNode tn = tfp.first; @@ -161,11 +161,11 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal( // This ensures that no type in our grammar has zero constructors. If // our input does not contain a Boolean variable, we need not allocate any // Boolean variables here. - unsigned useNVars = + uint64_t useNVars = (options().quantifiers.sygusRewSynthInputUseBool || !tn.isBoolean()) ? nvars : (hasBoolVar ? 1 : 0); - for (unsigned i = 0; i < useNVars; i++) + for (uint64_t i = 0; i < useNVars; i++) { // We must have a good name for these variables, these are // the ones output in rewrite rules. We choose @@ -173,7 +173,7 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal( std::stringstream ssv; if (varCounter < 26) { - ssv << static_cast<char>(varCounter + 61); + ssv << static_cast<char>(varCounter + static_cast<uint64_t>('A')); } else { @@ -188,6 +188,14 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal( } Trace("srs-input") << "...finished." << std::endl; + // if the problem is trivial, e.g. contains no non-constant terms, then we + // exit with an exception. + if (allVars.empty()) + { + throw Exception("No terms to consider for synthesizing rewrites"); + return PreprocessingPassResult::NO_CONFLICT; + } + Trace("srs-input") << "Convert subterms to free variable form..." << std::endl; // Replace all free variables with bound variables. This ensures that @@ -271,7 +279,6 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal( // add the variables for the type TypeNode ctt = ct.getType(); - Assert(tvars.find(ctt) != tvars.end()); std::vector<TypeNode> argList; // we add variable constructors if we are not Boolean, we are interested // in purely propositional rewrites (via the option), or this term is @@ -279,6 +286,8 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal( if (!ctt.isBoolean() || options().quantifiers.sygusRewSynthInputUseBool || ct.getKind() == BOUND_VARIABLE) { + Assert(tvars.find(ctt) != tvars.end()) + << "Unexpected type " << ctt << " for " << ct; for (const Node& v : tvars[ctt]) { std::stringstream ssc; |