From c938a904ea20f8511ae3344a9e9246a792d01a2d Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 27 Apr 2022 14:12:07 -0500 Subject: [PATCH] Add option to apply constant propagation for all learned literals (#8668) Adds `--simplification-bcp`, disabled by default. --- src/options/smt_options.toml | 8 ++++++ src/preprocessing/passes/non_clausal_simp.cpp | 25 +++++++++++++---- src/smt/set_defaults.cpp | 28 +++++++++++++++++++ src/smt/set_defaults.h | 7 +++++ 4 files changed, 62 insertions(+), 6 deletions(-) diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 7aaf05f93..b24e48644 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -25,6 +25,14 @@ name = "SMT Layer" name = "batch" help = "Save up all ASSERTions; run nonclausal simplification and clausal (MiniSat) propagation for all of them only after reaching a querying command (CHECKSAT or QUERY or predicate SUBTYPE declaration)." +[[option]] + name = "simplificationBoolConstProp" + category = "expert" + long = "simplification-bcp" + type = "bool" + default = "false" + help = "apply Boolean constant propagation as a substituion during simplification" + [[option]] name = "doStaticLearning" category = "regular" diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp index 72d2d8947..cca0f72b9 100644 --- a/src/preprocessing/passes/non_clausal_simp.cpp +++ b/src/preprocessing/passes/non_clausal_simp.cpp @@ -116,6 +116,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal( << "Iterate through " << propagator->getLearnedLiterals().size() << " learned literals." << std::endl; // No conflict, go through the literals and solve them + NodeManager* nm = NodeManager::currentNM(); context::Context* u = userContext(); Rewriter* rw = d_env.getRewriter(); TrustSubstitutionMap& ttls = d_preprocContext->getTopLevelSubstitutions(); @@ -173,7 +174,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal( Trace("non-clausal-simplify") << "conflict with " << learned_literals[i].getNode() << std::endl; assertionsToPreprocess->clear(); - Node n = NodeManager::currentNM()->mkConst(false); + Node n = nm->mkConst(false); assertionsToPreprocess->push_back(n, false, false, d_llpg.get()); return PreprocessingPassResult::CONFLICT; } @@ -206,17 +207,17 @@ PreprocessingPassResult NonClausalSimp::applyInternal( Trace("non-clausal-simplify") << "conflict while solving " << learnedLiteral << std::endl; assertionsToPreprocess->clear(); - Node n = NodeManager::currentNM()->mkConst(false); + Node n = nm->mkConst(false); assertionsToPreprocess->push_back(n); return PreprocessingPassResult::CONFLICT; } default: + TNode t; + TNode c; if (learnedLiteral.getKind() == kind::EQUAL && (learnedLiteral[0].isConst() || learnedLiteral[1].isConst())) { // constant propagation - TNode t; - TNode c; if (learnedLiteral[0].isConst()) { t = learnedLiteral[1]; @@ -227,6 +228,18 @@ PreprocessingPassResult NonClausalSimp::applyInternal( t = learnedLiteral[0]; c = learnedLiteral[1]; } + } + else if (options().smt.simplificationBoolConstProp) + { + // From non-equalities, learn the Boolean equality. Notice that + // the equality case above is strictly more powerful that this, since + // e.g. (= t c) * { t -> c } also simplifies to true. + bool pol = learnedLiteral.getKind() != kind::NOT; + c = nm->mkConst(pol); + t = pol ? learnedLiteral : learnedLiteral[0]; + } + if (!t.isNull()) + { Assert(!t.isConst()); Assert(rewrite(cps.apply(t)) == t); Assert(top_level_substs.apply(t) == t); @@ -244,7 +257,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal( } else { - // Keep the literal + // Keep the learned literal learned_literals[j++] = learned_literals[i]; } // Its a literal that could not be processed as a substitution or @@ -400,7 +413,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal( if (!learnedLitsToConjoin.empty()) { size_t replIndex = assertionsToPreprocess->getRealAssertionsEnd() - 1; - Node newConj = NodeManager::currentNM()->mkAnd(learnedLitsToConjoin); + Node newConj = nm->mkAnd(learnedLitsToConjoin); Trace("non-clausal-simplify") << "non-clausal simplification, reassert: " << newConj << std::endl; ProofGenerator* pg = nullptr; diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 9acdec976..e28459708 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -380,6 +380,18 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const throw OptionException(ss.str()); } } + // check if we have separation logic heap types + if (d_env.hasSepHeap()) + { + std::stringstream reasonNoSepLogic; + if (incompatibleWithSeparationLogic(opts, reasonNoSepLogic)) + { + std::stringstream ss; + ss << reasonNoSepLogic.str() + << " not supported when using separation logic."; + throw OptionException(ss.str()); + } + } } void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const @@ -1274,6 +1286,22 @@ bool SetDefaults::incompatibleWithQuantifiers(Options& opts, return false; } +bool SetDefaults::incompatibleWithSeparationLogic(Options& opts, + std::ostream& reason) const +{ + if (options().smt.simplificationBoolConstProp) + { + // Spatial formulas in separation logic have a semantics that depends on + // their position in the AST (e.g. their nesting beneath separation + // conjunctions). Thus, we cannot apply BCP as a substitution for spatial + // predicates to the input formula. We disable this option altogether to + // ensure this is the case + notifyModifyOption("simplification-bcp", "false", "separation logic"); + options().smt.simplificationBoolConstProp = false; + } + return false; +} + void SetDefaults::widenLogic(LogicInfo& logic, const Options& opts) const { bool needsUf = false; diff --git a/src/smt/set_defaults.h b/src/smt/set_defaults.h index 671af8e7e..cee7dd3ab 100644 --- a/src/smt/set_defaults.h +++ b/src/smt/set_defaults.h @@ -111,6 +111,13 @@ class SetDefaults : protected EnvObj * The output stream reason is similar to above. */ bool incompatibleWithQuantifiers(Options& opts, std::ostream& reason) const; + /** + * Check if incompatible with separation logic. Notice this method may + * modify the options to ensure that we are compatible with separation logic. + * The output stream reason is similar to above. + */ + bool incompatibleWithSeparationLogic(Options& opts, + std::ostream& reason) const; //------------------------- options setting, prior finalization of logic /** * Set defaults pre, which sets all options prior to finalizing the logic. -- 2.30.2