From 189a5dd7d07c1374db96f3f725477b61ff323dd4 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 27 Feb 2024 12:05:20 -0600 Subject: [PATCH 1/5] Add lemma inprocessing technique (#10319) This can be used to minimize the number of new SAT literals introduced in quantifier instantiations. It has a positive overall impact on SMT-LIB quantifiers, but is disabled by default for now. --- src/CMakeLists.txt | 2 + src/options/theory_options.toml | 41 ++++ src/proof/trust_node.cpp | 5 + src/proof/trust_node.h | 4 + src/prop/lemma_inprocess.cpp | 175 ++++++++++++++++++ src/prop/lemma_inprocess.h | 86 +++++++++ src/prop/prop_engine.cpp | 14 +- src/prop/prop_engine.h | 3 +- src/prop/theory_proxy.cpp | 13 +- src/prop/theory_proxy.h | 7 + src/prop/zero_level_learner.cpp | 86 +++++++-- src/prop/zero_level_learner.h | 16 ++ src/smt/set_defaults.cpp | 7 + src/theory/lemma_property.cpp | 9 + src/theory/lemma_property.h | 6 +- src/theory/quantifiers/instantiate.cpp | 6 +- test/regress/cli/CMakeLists.txt | 1 + .../quantifiers/dd.german169-lemma-inp.smt2 | 14 ++ 18 files changed, 475 insertions(+), 20 deletions(-) create mode 100644 src/prop/lemma_inprocess.cpp create mode 100644 src/prop/lemma_inprocess.h create mode 100644 test/regress/cli/regress0/quantifiers/dd.german169-lemma-inp.smt2 diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 6cf57b46340..0c263215563 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -246,6 +246,8 @@ libcvc5_add_sources( prop/kissat.h prop/learned_db.cpp prop/learned_db.h + prop/lemma_inprocess.cpp + prop/lemma_inprocess.h prop/minisat/core/Dimacs.h prop/minisat/core/Solver.cc prop/minisat/core/Solver.h diff --git a/src/options/theory_options.toml b/src/options/theory_options.toml index 46123ded697..3e29e30b9b8 100644 --- a/src/options/theory_options.toml +++ b/src/options/theory_options.toml @@ -66,3 +66,44 @@ name = "Theory Layer" [[option.mode.CARE_GRAPH]] name = "care-graph" help = "Use care graphs for theory combination." + +[[option]] + name = "lemmaInprocess" + category = "expert" + long = "lemma-inprocess=MODE" + type = "LemmaInprocessMode" + default = "NONE" + help = "Modes for inprocessing lemmas." + help_mode = "Modes for inprocessing lemmas." +[[option.mode.FULL]] + name = "full" + help = "Full inprocessing." +[[option.mode.LIGHT]] + name = "light" + help = "Light inprocessing." +[[option.mode.NONE]] + name = "none" + help = "No inprocessing." + +[[option]] + name = "lemmaInprocessSubsMode" + category = "expert" + long = "lemma-inprocess-subs=MODE" + type = "LemmaInprocessSubsMode" + default = "SIMPLE" + help = "Modes for substitutions for inprocessing lemmas." + help_mode = "Modes for substitutions for inprocessing lemmas." +[[option.mode.ALL]] + name = "all" + help = "All substitutions." +[[option.mode.SIMPLE]] + name = "simple" + help = "Simple substitutions." + +[[option]] + name = "lemmaInprocessInferEqLit" + category = "expert" + long = "lemma-inprocess-infer-eq-lit" + type = "bool" + default = "false" + help = "Infer equivalent literals when using lemma inprocess" diff --git a/src/proof/trust_node.cpp b/src/proof/trust_node.cpp index 5866bc3aa3b..dbff46a7fda 100644 --- a/src/proof/trust_node.cpp +++ b/src/proof/trust_node.cpp @@ -74,6 +74,11 @@ TrustNode TrustNode::mkReplaceGenTrustNode(const TrustNode& orig, return TrustNode(orig.getKind(), orig.getProven(), g); } +TrustNode TrustNode::mkTrustNode(TrustNodeKind tnk, Node p, ProofGenerator* g) +{ + return TrustNode(tnk, p, g); +} + TrustNode TrustNode::null() { return TrustNode(TrustNodeKind::INVALID, Node::null()); diff --git a/src/proof/trust_node.h b/src/proof/trust_node.h index a41fc35e862..dd3e4ab2172 100644 --- a/src/proof/trust_node.h +++ b/src/proof/trust_node.h @@ -96,6 +96,10 @@ class TrustNode /** Make a trust node, replacing the original generator */ static TrustNode mkReplaceGenTrustNode(const TrustNode& orig, ProofGenerator* g); + /** Make a trust node with the given explicit arguments. */ + static TrustNode mkTrustNode(TrustNodeKind tnk, + Node p, + ProofGenerator* g = nullptr); /** The null proven node */ static TrustNode null(); ~TrustNode() {} diff --git a/src/prop/lemma_inprocess.cpp b/src/prop/lemma_inprocess.cpp new file mode 100644 index 00000000000..dbf235de667 --- /dev/null +++ b/src/prop/lemma_inprocess.cpp @@ -0,0 +1,175 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2023 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Learner for literals asserted at level zero. + */ + +#include "prop/lemma_inprocess.h" + +#include "expr/node_algorithm.h" +#include "options/theory_options.h" +#include "prop/zero_level_learner.h" +#include "smt/env.h" + +namespace cvc5::internal { +namespace prop { + +LemmaInprocess::LemmaInprocess(Env& env, CnfStream* cs, ZeroLevelLearner& zll) + : EnvObj(env), + d_cs(cs), + d_tsmap(zll.getSimplifications()), + d_subsLitMap(userContext()), + d_eqLitLemmas(userContext()) +{ +} +TrustNode LemmaInprocess::inprocessLemma(TrustNode& trn) +{ + if (trn.getKind() == TrustNodeKind::CONFLICT) + { + return trn; + } + const Node& proven = trn.getProven(); + Node provenp = processInternal(proven); + if (provenp != proven) + { + Trace("lemma-inprocess-lemma") + << "Inprocess " << proven << " returns " << provenp << std::endl; + // proofs not supported + return TrustNode::mkTrustNode(trn.getKind(), provenp); + } + return trn; +} + +Node LemmaInprocess::processInternal(const Node& lem) +{ + std::vector eqLitLemmas; + NodeManager* nm = NodeManager::currentNM(); + std::unordered_map visited; + std::unordered_map::iterator it; + std::vector visit; + context::CDHashMap::iterator its; + TNode cur; + visit.emplace_back(lem); + do + { + cur = visit.back(); + Trace("lemma-inprocess-visit") << "visit " << cur << std::endl; + Assert(cur.getType().isBoolean()); + it = visited.find(cur); + if (it == visited.end()) + { + if (expr::isBooleanConnective(cur)) + { + visited[cur] = Node::null(); + visit.insert(visit.end(), cur.begin(), cur.end()); + } + else + { + visit.pop_back(); + // literal case + bool prevLit = d_cs->hasLiteral(cur); + Node scur = d_tsmap.get().apply(cur, d_env.getRewriter()); + its = d_subsLitMap.find(scur); + if (its != d_subsLitMap.end()) + { + if (cur != its->second) + { + Trace("lemma-inprocess") + << "Replace (indirect): " << cur << " -> " << its->second + << ", prevLit = " << prevLit << std::endl; + visited[cur] = its->second; + continue; + } + } + else + { + bool currLit = prevLit; + if (scur != cur) + { + currLit = d_cs->hasLiteral(scur); + scur = rewrite(scur); + Trace("lemma-inprocess-debug") + << "Inprocess " << cur << " -> " << scur << std::endl; + bool doReplace = false; + switch (options().theory.lemmaInprocess) + { + case options::LemmaInprocessMode::FULL: + doReplace = (scur.isConst() || currLit || !prevLit); + break; + case options::LemmaInprocessMode::LIGHT: + doReplace = (scur.isConst() || (currLit && !prevLit)); + break; + default: break; + } + if (doReplace) + { + if (options().theory.lemmaInprocessInferEqLit + && ((scur.isConst() || currLit) && prevLit)) + { + // inferred they are equivalent? maybe should send clause here? + Node eql = rewrite(scur.eqNode(cur)); + if (d_eqLitLemmas.find(eql) == d_eqLitLemmas.end()) + { + d_eqLitLemmas.insert(eql); + eqLitLemmas.emplace_back(eql); + } + } + Trace("lemma-inprocess") + << "Replace: " << cur << " -> " << scur + << ", currLit = " << currLit << ", prevLit = " << prevLit + << std::endl; + visited[cur] = scur; + d_subsLitMap[scur] = scur; + continue; + } + } + d_subsLitMap[scur] = cur; + } + visited[cur] = cur; + } + continue; + } + visit.pop_back(); + if (it->second.isNull()) + { + Node ret = cur; + bool childChanged = false; + std::vector children; + for (const Node& cn : cur) + { + it = visited.find(cn); + Assert(it != visited.end()); + Assert(!it->second.isNull()); + childChanged = childChanged || cn != it->second; + children.push_back(it->second); + } + if (childChanged) + { + ret = nm->mkNode(cur.getKind(), children); + ret = rewrite(ret); + } + visited[cur] = ret; + } + } while (!visit.empty()); + Assert(visited.find(lem) != visited.end()); + Assert(!visited.find(lem)->second.isNull()); + Node ret = visited[lem]; + if (!eqLitLemmas.empty()) + { + eqLitLemmas.emplace_back(ret); + return nm->mkAnd(eqLitLemmas); + } + return ret; +} + +} // namespace prop +} // namespace cvc5::internal diff --git a/src/prop/lemma_inprocess.h b/src/prop/lemma_inprocess.h new file mode 100644 index 00000000000..badeea58ea4 --- /dev/null +++ b/src/prop/lemma_inprocess.h @@ -0,0 +1,86 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2023 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Learner for literals asserted at level zero. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__PROP__LEMMA_INPROCESS_H +#define CVC5__PROP__LEMMA_INPROCESS_H + +#include + +#include "context/cdhashset.h" +#include "context/cdo.h" +#include "expr/node.h" +#include "prop/cnf_stream.h" +#include "smt/env_obj.h" +#include "theory/trust_substitutions.h" + +namespace cvc5::internal { + +class TheoryEngine; + +namespace prop { + +class ZeroLevelLearner; + +/** + * Lemma inprocess, which heuristically simplifies lemmas to an equivalent + * form based on the current simplifications stored by the zero level learner. + * + * The intution of this class is to increase the likelihood that literals in the + * SAT solver are reused. For example if a = 0 is learned at decision level + * zero, and there is a SAT literal P(0), if P(a) is introduced as a new literal + * in a lemma, we may replace it by P(0). + * + * As another example, if we learn a=b, c=b and we have a literal P(a), then + * we may replace P(c) with P(a). + * + * This simplification is done selectively and will never replace a known SAT + * literal by a new SAT literal. Further policies are determined by + * lemma-inprocess-mode. + * + * Generally this method can only be applied to lemmas where the structure of + * the lemma is not important. This includes quantifier instantiation lemmas + * for example. + */ +class LemmaInprocess : protected EnvObj +{ + using NodeSet = context::CDHashSet; + + public: + LemmaInprocess(Env& env, CnfStream* cs, ZeroLevelLearner& zll); + ~LemmaInprocess() {} + /** Inprocess lemma */ + TrustNode inprocessLemma(TrustNode& trn); + + private: + /** + * Process internal, returns an equivalent formula to lem, assuming d_tsmap. + */ + Node processInternal(const Node& lem); + /** Pointer to CNF stream */ + CnfStream* d_cs; + /** Reference to the current available simplification */ + theory::TrustSubstitutionMap& d_tsmap; + /** Mapping from simplified literals to a known SAT literal */ + context::CDHashMap d_subsLitMap; + /** Equivalent literal lemmas we have sent */ + context::CDHashSet d_eqLitLemmas; +}; + +} // namespace prop +} // namespace cvc5::internal + +#endif diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index ad08acd347a..a0946acdc1b 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -175,6 +175,7 @@ void PropEngine::assertInputFormulas( void PropEngine::assertLemma(TrustNode tlemma, theory::LemmaProperty p) { bool removable = isLemmaPropertyRemovable(p); + bool inprocess = isLemmaPropertyInprocess(p); // call preprocessor std::vector ppLemmas; @@ -208,7 +209,7 @@ void PropEngine::assertLemma(TrustNode tlemma, theory::LemmaProperty p) } // now, assert the lemmas - assertLemmasInternal(tplemma, ppLemmas, removable); + assertLemmasInternal(tplemma, ppLemmas, removable, inprocess); } void PropEngine::assertTrustedLemmaInternal(TrustNode trn, bool removable) @@ -274,7 +275,8 @@ void PropEngine::assertInternal( void PropEngine::assertLemmasInternal( TrustNode trn, const std::vector& ppLemmas, - bool removable) + bool removable, + bool inprocess) { if (!removable) { @@ -290,6 +292,12 @@ void PropEngine::assertLemmasInternal( Trace("prop") << "Push to SAT..." << std::endl; if (!trn.isNull()) { + // inprocess + if (inprocess + && options().theory.lemmaInprocess != options::LemmaInprocessMode::NONE) + { + trn = d_theoryProxy->inprocessLemma(trn); + } assertTrustedLemmaInternal(trn, removable); } for (const theory::SkolemLemma& lem : ppLemmas) @@ -558,7 +566,7 @@ Node PropEngine::getPreprocessedTerm(TNode n) TrustNode tpn = d_theoryProxy->preprocess(n, newLemmas); // send lemmas corresponding to the skolems introduced by preprocessing n TrustNode trnNull; - assertLemmasInternal(trnNull, newLemmas, false); + assertLemmasInternal(trnNull, newLemmas, false, false); return tpn.isNull() ? Node(n) : tpn.getNode(); } diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 41f5ee11e8e..89ff845bf48 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -397,7 +397,8 @@ class PropEngine : protected EnvObj */ void assertLemmasInternal(TrustNode trn, const std::vector& ppLemmas, - bool removable); + bool removable, + bool inprocess); /** * Indicates that the SAT solver is currently solving something and we should diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index e11fe8d9ad2..316b538bbdb 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -61,7 +61,8 @@ TheoryProxy::TheoryProxy(Env& env, options().smt.deepRestartMode != options::DeepRestartMode::NONE || isOutputOn(OutputTag::LEARNED_LITS) || options().smt.produceLearnedLiterals - || options().parallel.computePartitions > 0; + || options().parallel.computePartitions > 0 + || options().theory.lemmaInprocess != options::LemmaInprocessMode::NONE; if (trackZeroLevel) { d_zll = std::make_unique(env, theoryEngine); @@ -91,6 +92,10 @@ void TheoryProxy::finishInit(CDCLTSatSolver* ss, CnfStream* cs) // compute if we need to track skolem definitions d_trackActiveSkDefs = d_decisionEngine->needsActiveSkolemDefs() || d_prr->needsActiveSkolemDefs(); + if (options().theory.lemmaInprocess != options::LemmaInprocessMode::NONE) + { + d_lemip.reset(new LemmaInprocess(d_env, cs, *d_zll.get())); + } d_cnfStream = cs; } @@ -473,5 +478,11 @@ std::vector TheoryProxy::getLearnedZeroLevelLiteralsForRestart() const return {}; } +TrustNode TheoryProxy::inprocessLemma(TrustNode& trn) +{ + Assert(d_lemip != nullptr); + return d_lemip->inprocessLemma(trn); +} + } // namespace prop } // namespace cvc5::internal diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index 89a53ef85e1..03e1274211c 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -26,6 +26,7 @@ #include "expr/node.h" #include "proof/trust_node.h" #include "prop/learned_db.h" +#include "prop/lemma_inprocess.h" #include "prop/registrar.h" #include "prop/sat_solver_types.h" #include "prop/theory_preregistrar.h" @@ -198,6 +199,9 @@ class TheoryProxy : protected EnvObj, public Registrar /** Get literal type using ZLL utility */ modes::LearnedLitType getLiteralType(const Node& lit) const; + /** Inprocess lemma */ + TrustNode inprocessLemma(TrustNode& trn); + private: /** The prop engine we are using. */ PropEngine* d_propEngine; @@ -229,6 +233,9 @@ class TheoryProxy : protected EnvObj, public Registrar /** The zero level learner */ std::unique_ptr d_zll; + /** The inprocess utility */ + std::unique_ptr d_lemip; + /** Preregister policy */ std::unique_ptr d_prr; diff --git a/src/prop/zero_level_learner.cpp b/src/prop/zero_level_learner.cpp index 40b0b98b6dd..7783b428cd4 100644 --- a/src/prop/zero_level_learner.cpp +++ b/src/prop/zero_level_learner.cpp @@ -18,6 +18,7 @@ #include "expr/node_algorithm.h" #include "expr/skolem_manager.h" #include "options/base_options.h" +#include "options/prop_options.h" #include "options/smt_options.h" #include "smt/env.h" #include "theory/theory_engine.h" @@ -35,7 +36,8 @@ ZeroLevelLearner::ZeroLevelLearner(Env& env, TheoryEngine* theoryEngine) d_ppnAtoms(userContext()), d_ppnTerms(userContext()), d_ppnSyms(userContext()), - d_assertNoLearnCount(0) + d_assertNoLearnCount(0), + d_tsmap(env, userContext(), "ZllSimplificationMap") { // get the learned types options::DeepRestartMode lmode = options().smt.deepRestartMode; @@ -58,6 +60,7 @@ ZeroLevelLearner::ZeroLevelLearner(Env& env, TheoryEngine* theoryEngine) d_learnedTypes.insert(modes::LearnedLitType::CONSTANT_PROP); } } + d_trackSimplifications = true; } ZeroLevelLearner::~ZeroLevelLearner() {} @@ -128,6 +131,10 @@ void ZeroLevelLearner::notifyInputFormulas(const std::vector& assertions) if (!lit.isConst() || !lit.getConst()) { // output learned literals from preprocessing + if (d_trackSimplifications) + { + computeLearnedLiteralType(lit); + } processLearnedLiteral(lit, modes::LearnedLitType::PREPROCESS); // also get its symbols expr::getSymbols(atom, inputSymbols, visitedWithinAtom); @@ -216,7 +223,7 @@ bool ZeroLevelLearner::notifyAsserted(TNode assertion, int32_t alevel) } if (TraceIsOn("level-zero-debug")) { - if (d_assertNoLearnCount > 0 + if (d_assertNoLearnCount > 0 && d_deepRestartThreshold > 0 && d_assertNoLearnCount % d_deepRestartThreshold == 0) { Trace("level-zero-debug") @@ -229,45 +236,96 @@ bool ZeroLevelLearner::notifyAsserted(TNode assertion, int32_t alevel) } modes::LearnedLitType ZeroLevelLearner::computeLearnedLiteralType( - const Node& lit) + const Node& input) { // literal was learned, determine its type + // apply substitutions first + Node lit = d_tsmap.apply(input, d_env.getRewriter()); TNode aatom = lit.getKind() == Kind::NOT ? lit[0] : lit; bool internal = d_ppnAtoms.find(aatom) == d_ppnAtoms.end(); modes::LearnedLitType ltype = internal ? modes::LearnedLitType::INTERNAL : modes::LearnedLitType::INPUT; // compute if solvable - if (internal) + if (internal || d_trackSimplifications) { Subs ss; + bool processed = false; if (getSolved(lit, ss)) { // if we solved for any variable from input, we are SOLVABLE. - for (const Node& v : ss.d_vars) + for (size_t i = 0, nvars = ss.d_vars.size(); i < nvars; i++) { + Node v = ss.d_vars[i]; if (d_ppnSyms.find(v) != d_ppnSyms.end()) { Trace("level-zero-assert") << "...solvable due to " << v << std::endl; - ltype = modes::LearnedLitType::SOLVABLE; - break; + if (ltype == modes::LearnedLitType::INTERNAL) + { + ltype = modes::LearnedLitType::SOLVABLE; + } + } + if (d_trackSimplifications) + { + bool addSubs = true; + switch (options().theory.lemmaInprocessSubsMode) + { + case options::LemmaInprocessSubsMode::SIMPLE: + addSubs = ss.d_subs[i].getNumChildren() == 0; + break; + default: break; + } + if (addSubs) + { + processed = true; + Trace("lemma-inprocess-subs") + << "Add subs: " << v << " -> " << ss.d_subs[i] << std::endl; + d_tsmap.addSubstitution(v, ss.d_subs[i]); + } } } } - if (ltype != modes::LearnedLitType::SOLVABLE) + if ((d_trackSimplifications && !processed) + || ltype != modes::LearnedLitType::SOLVABLE) { // maybe a constant prop? if (lit.getKind() == Kind::EQUAL) { for (size_t i = 0; i < 2; i++) { - if (lit[i].isConst() - && d_ppnTerms.find(lit[1 - i]) != d_ppnTerms.end()) + // Only consider substitutions whose RHS are constants. + // A more general policy could consider lit[i].getNumChildren()==0. + if (lit[i].isConst()) { - ltype = modes::LearnedLitType::CONSTANT_PROP; + if (ltype == modes::LearnedLitType::INTERNAL + && d_ppnTerms.find(lit[1 - i]) != d_ppnTerms.end()) + { + ltype = modes::LearnedLitType::CONSTANT_PROP; + } + if (d_trackSimplifications && !processed) + { + Trace("lemma-inprocess-subs") + << "Add cp: " << lit[1 - i] << " -> " << lit[i] << std::endl; + d_tsmap.addSubstitution(lit[1 - i], lit[i]); + processed = true; + } + break; + } + else if ((d_trackSimplifications && !processed) + && expr::hasSubterm(lit[1 - i], lit[i])) + { + Trace("lemma-inprocess-subs") << "Add cp subterm: " << lit[1 - i] + << " -> " << lit[i] << std::endl; + d_tsmap.addSubstitution(lit[1 - i], lit[i]); + processed = true; break; } } } + if (!processed) + { + Trace("lemma-inprocess-subs-n") + << "Unused unit learned: " << lit << std::endl; + } } } Trace("level-zero-assert") @@ -275,6 +333,12 @@ modes::LearnedLitType ZeroLevelLearner::computeLearnedLiteralType( return ltype; } +theory::TrustSubstitutionMap& ZeroLevelLearner::getSimplifications() +{ + Assert(d_trackSimplifications); + return d_tsmap; +} + void ZeroLevelLearner::processLearnedLiteral(const Node& lit, modes::LearnedLitType ltype) { diff --git a/src/prop/zero_level_learner.h b/src/prop/zero_level_learner.h index 923e5c5cbba..bcc2ac201e3 100644 --- a/src/prop/zero_level_learner.h +++ b/src/prop/zero_level_learner.h @@ -26,6 +26,7 @@ #include "expr/subs.h" #include "prop/learned_db.h" #include "smt/env_obj.h" +#include "theory/trust_substitutions.h" namespace cvc5::internal { @@ -69,6 +70,13 @@ class ZeroLevelLearner : protected EnvObj /** compute type for learned literal */ modes::LearnedLitType computeLearnedLiteralType(const Node& lit); + /** + * Get inferred simplifications. This is a (term) substitution that can be + * applied to construct simpler terms that are equivalent based on + * literals learned at decision level zero. + */ + theory::TrustSubstitutionMap& getSimplifications(); + private: static void getAtoms(TNode a, std::unordered_set& visited, @@ -109,6 +117,14 @@ class ZeroLevelLearner : protected EnvObj size_t d_deepRestartThreshold; /** learnable learned literal types (for deep restart), based on option */ std::unordered_set d_learnedTypes; + /** Should we track the simplification map? */ + bool d_trackSimplifications; + /** + * Simplification map. This is a substitution that is globally valid based + * on the literals learned at decision level zero. + */ + theory::TrustSubstitutionMap d_tsmap; + }; /* class ZeroLevelLearner */ } // namespace prop diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 87c8c60972c..669d1df9f22 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -961,6 +961,13 @@ bool SetDefaults::incompatibleWithProofs(Options& opts, reason << "deep restarts"; return true; } + if (options().theory.lemmaInprocess != options::LemmaInprocessMode::NONE) + { + // lemma inprocessing introduces depencencies from learned unit literals + // that are not tracked. + reason << "lemma inprocessing"; + return true; + } return false; } diff --git a/src/theory/lemma_property.cpp b/src/theory/lemma_property.cpp index ce48af7640b..efe66fde85a 100644 --- a/src/theory/lemma_property.cpp +++ b/src/theory/lemma_property.cpp @@ -53,6 +53,11 @@ bool isLemmaPropertyNeedsJustify(LemmaProperty p) return (p & LemmaProperty::NEEDS_JUSTIFY) != LemmaProperty::NONE; } +bool isLemmaPropertyInprocess(LemmaProperty p) +{ + return (p & LemmaProperty::INPROCESS) != LemmaProperty::NONE; +} + std::ostream& operator<<(std::ostream& out, LemmaProperty p) { if (p == LemmaProperty::NONE) @@ -74,6 +79,10 @@ std::ostream& operator<<(std::ostream& out, LemmaProperty p) { out << " NEEDS_JUSTIFY"; } + if (isLemmaPropertyInprocess(p)) + { + out << " INPROCESS"; + } out << " }"; } return out; diff --git a/src/theory/lemma_property.h b/src/theory/lemma_property.h index 912ad9a21f0..95c10cd06f7 100644 --- a/src/theory/lemma_property.h +++ b/src/theory/lemma_property.h @@ -33,7 +33,9 @@ enum class LemmaProperty : uint32_t // whether the processing of the lemma should send atoms to the caller SEND_ATOMS = 2, // whether the lemma is part of the justification for answering "sat" - NEEDS_JUSTIFY = 4 + NEEDS_JUSTIFY = 4, + // the lemma can be inprocessed + INPROCESS = 8 }; /** Define operator lhs | rhs */ LemmaProperty operator|(LemmaProperty lhs, LemmaProperty rhs); @@ -49,6 +51,8 @@ bool isLemmaPropertyRemovable(LemmaProperty p); bool isLemmaPropertySendAtoms(LemmaProperty p); /** is the needs justify bit set on p? */ bool isLemmaPropertyNeedsJustify(LemmaProperty p); +/** is the inprocess bit set on p? */ +bool isLemmaPropertyInprocess(LemmaProperty p); /** * Writes an lemma property name to a stream. diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index b2da7557c1b..f65e3133313 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -340,12 +340,12 @@ bool Instantiate::addInstantiationInternal( if (hasProof) { // use proof generator - addedLem = - d_qim.addPendingLemma(lem, id, LemmaProperty::NONE, d_pfInst.get()); + addedLem = d_qim.addPendingLemma( + lem, id, LemmaProperty::INPROCESS, d_pfInst.get()); } else { - addedLem = d_qim.addPendingLemma(lem, id); + addedLem = d_qim.addPendingLemma(lem, id, LemmaProperty::INPROCESS); } if (!addedLem) diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index 722b6491763..948f9cbc3fa 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -1358,6 +1358,7 @@ set(regress_0_tests regress0/quantifiers/clock-3.smt2 regress0/quantifiers/cond-var-elim-binary.smt2 regress0/quantifiers/dd.german169-ieval.smt2 + regress0/quantifiers/dd.german169-lemma-inp.smt2 regress0/quantifiers/dd.ho-matching-enum.smt2 regress0/quantifiers/dd.ricart-ieval.smt2 regress0/quantifiers/dd.javafe-ieval.smt2 diff --git a/test/regress/cli/regress0/quantifiers/dd.german169-lemma-inp.smt2 b/test/regress/cli/regress0/quantifiers/dd.german169-lemma-inp.smt2 new file mode 100644 index 00000000000..dfa0cf890ad --- /dev/null +++ b/test/regress/cli/regress0/quantifiers/dd.german169-lemma-inp.smt2 @@ -0,0 +1,14 @@ +; COMMAND-LINE: --lemma-inprocess=full +; COMMAND-LINE: --lemma-inprocess=full --lemma-inprocess-subs=all --lemma-inprocess-infer-eq-lit +; COMMAND-LINE: --lemma-inprocess=light +; EXPECT: unsat +; DISABLE-TESTER: unsat-core +; DISABLE-TESTER: proof +(set-logic ALL) +(declare-sort s 0) +(declare-datatypes ((ms 0)) (((a)))) +(declare-datatypes ((m 0)) (((c (ml ms))))) +(declare-fun sf () s) +(declare-fun h () (Array s m)) +(assert (not (=> (and (forall ((n s)) (not (= a (ml (select h n)))))) (= a (ml (select h sf))) false))) +(check-sat) From f572e0b4da3aec7632686a6294601bd1d76d6dbe Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Tue, 27 Feb 2024 16:01:30 -0600 Subject: [PATCH 2/5] Rename BAG_DUPLICATE_REMOVAL to SETOF and cleanup unused bag operators (#10376) Remove the operators is_singleton, from_set, to_set --- NEWS.md | 2 + docs/theories/bags.rst | 4 +- include/cvc5/cvc5_kind.h | 72 +--------- proofs/alf/cvc5/theories/Bags.smt3 | 2 +- proofs/lfsc/signatures/theory_def.plf | 4 +- src/api/cpp/cvc5.cpp | 11 +- src/parser/smt2/smt2_state.cpp | 5 +- src/printer/smt2/smt2_printer.cpp | 5 +- src/theory/bags/bag_solver.cpp | 8 +- src/theory/bags/bag_solver.h | 4 +- src/theory/bags/bags_rewriter.cpp | 53 +------ src/theory/bags/bags_rewriter.h | 23 +-- src/theory/bags/bags_utils.cpp | 82 +---------- src/theory/bags/bags_utils.h | 19 +-- src/theory/bags/inference_generator.cpp | 6 +- src/theory/bags/inference_generator.h | 6 +- src/theory/bags/kinds | 20 +-- src/theory/bags/rewrites.cpp | 3 +- src/theory/bags/rewrites.h | 2 +- src/theory/bags/theory_bags.cpp | 7 +- src/theory/bags/theory_bags_type_rules.cpp | 85 +---------- src/theory/bags/theory_bags_type_rules.h | 42 +----- src/theory/inference_id.cpp | 2 +- src/theory/inference_id.h | 2 +- test/regress/cli/CMakeLists.txt | 4 +- .../cli/regress1/bags/proj-issue566.smt2 | 2 +- .../{duplicate_removal1.smt2 => setof1.smt2} | 2 +- .../{duplicate_removal2.smt2 => setof2.smt2} | 2 +- .../theory/theory_bags_normal_form_white.cpp | 134 +----------------- .../theory/theory_bags_rewriter_white.cpp | 57 +------- .../theory/theory_bags_type_rules_white.cpp | 23 +-- 31 files changed, 80 insertions(+), 613 deletions(-) rename test/regress/cli/regress1/bags/{duplicate_removal1.smt2 => setof1.smt2} (83%) rename test/regress/cli/regress1/bags/{duplicate_removal2.smt2 => setof2.smt2} (83%) diff --git a/NEWS.md b/NEWS.md index 3ea6df3df88..d797c6f11d3 100644 --- a/NEWS.md +++ b/NEWS.md @@ -11,6 +11,8 @@ This file contains a summary of important user-visible changes. deprecated and replaced by `std::to_string(Kind)` and `std::to_string(SortKind)`. They will be removed in the next minor release. +- Renamed `bag.duplicate_removal` to `bag.setof`. + cvc5 1.1.1 ========== diff --git a/docs/theories/bags.rst b/docs/theories/bags.rst index 87bf47823b7..bba09ea4eb0 100644 --- a/docs/theories/bags.rst +++ b/docs/theories/bags.rst @@ -33,7 +33,7 @@ a `cvc5::Solver solver` object. +----------------------+----------------------------------------------+-------------------------------------------------------------------------+ | Difference subtract | ``(bag.difference_subtract X Y)`` | ``Term t = solver.mkTerm(Kind::BAG_DIFFERENCE_SUBTRACT, {X, Y});`` | +----------------------+----------------------------------------------+-------------------------------------------------------------------------+ -| Duplicate elimination| ``(bag.duplicate_removal X)`` | ``Term t = solver.mkTerm(Kind::BAG_DUPLICATE_REMOVAL, {X});`` | +| Duplicate elimination| ``(bag.setof X)`` | ``Term t = solver.mkTerm(Kind::BAG_SETOF, {X});`` | +----------------------+----------------------------------------------+-------------------------------------------------------------------------+ | Membership | ``(bag.member x X)`` | ``Term x = solver.mkConst(solver.getStringSort(), "x");`` | | | | | @@ -70,7 +70,7 @@ The semantics of supported bag operators is given in the table below. +-----------------------------------------------------+-------------------------+------------------------------------------------------------------------------------+ | difference remove :math:`m_1 \setminus\setminus m_2`| bag.difference_remove | :math:`\forall e. \; (m_1 \setminus\setminus m_2)(e) = ite(m_2(e) = 0, m_1(e), 0)` | +-----------------------------------------------------+-------------------------+------------------------------------------------------------------------------------+ -| duplicate elimination :math:`\delta(m)` | bag.duplicate_removal | :math:`\forall e. \; (\delta(m))(e) = ite(1 \leq m(e), 1, 0)` | +| setof :math:`\delta(m)` | bag.setof | :math:`\forall e. \; (\delta(m))(e) = ite(1 \leq m(e), 1, 0)` | +-----------------------------------------------------+-------------------------+------------------------------------------------------------------------------------+ | subbag :math:`m_1 \subseteq m_2` | bag.subbag | :math:`\forall e. \; m_1(e) \leq m_2(e)` | +-----------------------------------------------------+-------------------------+------------------------------------------------------------------------------------+ diff --git a/include/cvc5/cvc5_kind.h b/include/cvc5/cvc5_kind.h index 57477a4fca8..5fe18fdad32 100644 --- a/include/cvc5/cvc5_kind.h +++ b/include/cvc5/cvc5_kind.h @@ -3812,7 +3812,7 @@ enum ENUM(Kind) : int32_t */ EVALUE(BAG_MEMBER), /** - * Bag duplicate removal. + * Bag setof. * * Eliminate duplicates in a given bag. The returned bag contains exactly the * same elements in the given bag, but with multiplicity one. @@ -3835,7 +3835,7 @@ enum ENUM(Kind) : int32_t * future versions. * \endrst */ - EVALUE(BAG_DUPLICATE_REMOVAL), + EVALUE(BAG_SETOF), /** * Bag make. * @@ -3908,73 +3908,7 @@ enum ENUM(Kind) : int32_t * future versions. * \endrst */ - EVALUE(BAG_CHOOSE), - /** - * Bag is singleton tester. - * - * - Arity: ``1`` - * - * - ``1:`` Term of bag Sort - * - * - Create Term of this Kind with: - * - * - Solver::mkTerm(Kind, const std::vector&) const - * - Solver::mkTerm(const Op&, const std::vector&) const - * - * - Create Op of this kind with: - * - * - Solver::mkOp(Kind, const std::vector&) const - * - * \rst - * .. warning:: This kind is experimental and may be changed or removed in - * future versions. - * \endrst - */ - EVALUE(BAG_IS_SINGLETON), - /** - * Conversion from set to bag. - * - * - Arity: ``1`` - * - * - ``1:`` Term of set Sort - * - * - Create Term of this Kind with: - * - * - Solver::mkTerm(Kind, const std::vector&) const - * - Solver::mkTerm(const Op&, const std::vector&) const - * - * - Create Op of this kind with: - * - * - Solver::mkOp(Kind, const std::vector&) const - * - * \rst - * .. warning:: This kind is experimental and may be changed or removed in - * future versions. - * \endrst - */ - EVALUE(BAG_FROM_SET), - /** - * Conversion from bag to set. - * - * - Arity: ``1`` - * - * - ``1:`` Term of bag Sort - * - * - Create Term of this Kind with: - * - * - Solver::mkTerm(Kind, const std::vector&) const - * - Solver::mkTerm(const Op&, const std::vector&) const - * - * - Create Op of this kind with: - * - * - Solver::mkOp(Kind, const std::vector&) const - * - * \rst - * .. warning:: This kind is experimental and may be changed or removed in - * future versions. - * \endrst - */ - EVALUE(BAG_TO_SET), + EVALUE(BAG_CHOOSE), /** * Bag map. * diff --git a/proofs/alf/cvc5/theories/Bags.smt3 b/proofs/alf/cvc5/theories/Bags.smt3 index 7e72d165edb..6ead5f421ee 100644 --- a/proofs/alf/cvc5/theories/Bags.smt3 +++ b/proofs/alf/cvc5/theories/Bags.smt3 @@ -18,7 +18,7 @@ (declare-const bag.member (-> (! Type :var T :implicit) T (Bag T) Bool)) (declare-const bag.card (-> (! Type :var T :implicit) (Bag T) Int)) (declare-const bag.choose (-> (! Type :var T :implicit) (Bag T) T)) -(declare-const bag.duplicate_removal (-> (! Type :var T :implicit) (Bag T) (Bag T))) +(declare-const bag.setof (-> (! Type :var T :implicit) (Bag T) (Bag T))) (declare-const bag.is_singleton (-> (! Type :var T :implicit) (Bag T) Bool)) (declare-const bag.filter (-> (! Type :var T :implicit) (-> T Bool) (Bag T) (Bag T))) diff --git a/proofs/lfsc/signatures/theory_def.plf b/proofs/lfsc/signatures/theory_def.plf index 137f4495fc4..fe60c119b5d 100644 --- a/proofs/lfsc/signatures/theory_def.plf +++ b/proofs/lfsc/signatures/theory_def.plf @@ -545,8 +545,8 @@ (define bag.count (# x term (# y term (apply (apply f_bag.count x) y)))) (declare f_bag term) (define bag (# x term (# y term (apply (apply f_bag x) y)))) -(declare f_bag.duplicate_removal term) -(define bag.duplicate_removal (# x term (apply f_bag.duplicate_removal x))) +(declare f_bag.setof term) +(define bag.setof (# x term (apply f_bag.setof x))) (declare f_bag.card term) (define bag.card (# x term (apply f_bag.card x))) (declare f_bag.choose term) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 43dc66675b2..2c946b59b62 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -355,15 +355,11 @@ const static std::unordered_map> KIND_ENUM(Kind::BAG_SUBBAG, internal::Kind::BAG_SUBBAG), KIND_ENUM(Kind::BAG_COUNT, internal::Kind::BAG_COUNT), KIND_ENUM(Kind::BAG_MEMBER, internal::Kind::BAG_MEMBER), - KIND_ENUM(Kind::BAG_DUPLICATE_REMOVAL, - internal::Kind::BAG_DUPLICATE_REMOVAL), + KIND_ENUM(Kind::BAG_SETOF, internal::Kind::BAG_SETOF), KIND_ENUM(Kind::BAG_MAKE, internal::Kind::BAG_MAKE), KIND_ENUM(Kind::BAG_EMPTY, internal::Kind::BAG_EMPTY), KIND_ENUM(Kind::BAG_CARD, internal::Kind::BAG_CARD), KIND_ENUM(Kind::BAG_CHOOSE, internal::Kind::BAG_CHOOSE), - KIND_ENUM(Kind::BAG_IS_SINGLETON, internal::Kind::BAG_IS_SINGLETON), - KIND_ENUM(Kind::BAG_FROM_SET, internal::Kind::BAG_FROM_SET), - KIND_ENUM(Kind::BAG_TO_SET, internal::Kind::BAG_TO_SET), KIND_ENUM(Kind::BAG_MAP, internal::Kind::BAG_MAP), KIND_ENUM(Kind::BAG_FILTER, internal::Kind::BAG_FILTER), KIND_ENUM(Kind::BAG_FOLD, internal::Kind::BAG_FOLD), @@ -752,14 +748,11 @@ const static std::unordered_map elements; const set& downwards = d_state.getElements(n); const set& upwards = d_state.getElements(n[0]); @@ -270,7 +270,7 @@ void BagSolver::checkDuplicateRemoval(Node n) for (const Node& e : elements) { - InferInfo i = d_ig.duplicateRemoval(n, d_state.getRepresentative(e)); + InferInfo i = d_ig.setof(n, d_state.getRepresentative(e)); d_im.lemmaTheoryInference(&i); } } diff --git a/src/theory/bags/bag_solver.h b/src/theory/bags/bag_solver.h index 3ac2b3f575e..5fc1f202753 100644 --- a/src/theory/bags/bag_solver.h +++ b/src/theory/bags/bag_solver.h @@ -43,7 +43,7 @@ class BagSolver : protected EnvObj /** * apply inference rules for basic bag operators without quantifiers: * BAG_MAKE, BAG_UNION_DISJOINT, BAG_UNION_MAX, BAG_INTER_MIN, - * BAG_DIFFERENCE_SUBTRACT, BAG_DIFFERENCE_REMOVE, BAG_DUPLICATE_REMOVAL + * BAG_DIFFERENCE_SUBTRACT, BAG_DIFFERENCE_REMOVE, BAG_SETOF */ void checkBasicOperations(); @@ -95,7 +95,7 @@ class BagSolver : protected EnvObj /** apply inference rules for difference remove */ void checkDifferenceRemove(const Node& n); /** apply inference rules for duplicate removal operator */ - void checkDuplicateRemoval(Node n); + void checkSetof(Node n); /** apply non negative constraints for multiplicities */ void checkNonNegativeCountTerms(const Node& bag, const Node& element); /** apply inference rules for disequal bag terms */ diff --git a/src/theory/bags/bags_rewriter.cpp b/src/theory/bags/bags_rewriter.cpp index 1616c7c876e..b799cfba9a9 100644 --- a/src/theory/bags/bags_rewriter.cpp +++ b/src/theory/bags/bags_rewriter.cpp @@ -78,9 +78,7 @@ RewriteResponse BagsRewriter::postRewrite(TNode n) { case Kind::BAG_MAKE: response = rewriteMakeBag(n); break; case Kind::BAG_COUNT: response = rewriteBagCount(n); break; - case Kind::BAG_DUPLICATE_REMOVAL: - response = rewriteDuplicateRemoval(n); - break; + case Kind::BAG_SETOF: response = rewriteSetof(n); break; case Kind::BAG_UNION_MAX: response = rewriteUnionMax(n); break; case Kind::BAG_UNION_DISJOINT: response = rewriteUnionDisjoint(n); break; case Kind::BAG_INTER_MIN: response = rewriteIntersectionMin(n); break; @@ -91,9 +89,6 @@ RewriteResponse BagsRewriter::postRewrite(TNode n) response = rewriteDifferenceRemove(n); break; case Kind::BAG_CARD: response = rewriteCard(n); break; - case Kind::BAG_IS_SINGLETON: response = rewriteIsSingleton(n); break; - case Kind::BAG_FROM_SET: response = rewriteFromSet(n); break; - case Kind::BAG_TO_SET: response = rewriteToSet(n); break; case Kind::BAG_MAP: response = postRewriteMap(n); break; case Kind::BAG_FILTER: response = postRewriteFilter(n); break; case Kind::BAG_FOLD: response = postRewriteFold(n); break; @@ -207,16 +202,16 @@ BagsRewriteResponse BagsRewriter::rewriteBagCount(const TNode& n) const return BagsRewriteResponse(n, Rewrite::NONE); } -BagsRewriteResponse BagsRewriter::rewriteDuplicateRemoval(const TNode& n) const +BagsRewriteResponse BagsRewriter::rewriteSetof(const TNode& n) const { - Assert(n.getKind() == Kind::BAG_DUPLICATE_REMOVAL); + Assert(n.getKind() == Kind::BAG_SETOF); if (n[0].getKind() == Kind::BAG_MAKE && n[0][1].isConst() && n[0][1].getConst().sgn() == 1) { - // (bag.duplicate_removal (bag x n)) = (bag x 1) + // (bag.setof (bag x n)) = (bag x 1) // where n is a positive constant Node bag = d_nm->mkNode(Kind::BAG_MAKE, n[0][0], d_one); - return BagsRewriteResponse(bag, Rewrite::DUPLICATE_REMOVAL_BAG_MAKE); + return BagsRewriteResponse(bag, Rewrite::SETOF_BAG_MAKE); } return BagsRewriteResponse(n, Rewrite::NONE); } @@ -472,44 +467,6 @@ BagsRewriteResponse BagsRewriter::rewriteCard(const TNode& n) const return BagsRewriteResponse(n, Rewrite::NONE); } -BagsRewriteResponse BagsRewriter::rewriteIsSingleton(const TNode& n) const -{ - Assert(n.getKind() == Kind::BAG_IS_SINGLETON); - if (n[0].getKind() == Kind::BAG_MAKE) - { - // (bag.is_singleton (bag x c)) = (c == 1) - Node equal = n[0][1].eqNode(d_one); - return BagsRewriteResponse(equal, Rewrite::IS_SINGLETON_BAG_MAKE); - } - return BagsRewriteResponse(n, Rewrite::NONE); -} - -BagsRewriteResponse BagsRewriter::rewriteFromSet(const TNode& n) const -{ - Assert(n.getKind() == Kind::BAG_FROM_SET); - if (n[0].getKind() == Kind::SET_SINGLETON) - { - // (bag.from_set (set.singleton x)) = (bag x 1) - Node bag = d_nm->mkNode(Kind::BAG_MAKE, n[0][0], d_one); - return BagsRewriteResponse(bag, Rewrite::FROM_SINGLETON); - } - return BagsRewriteResponse(n, Rewrite::NONE); -} - -BagsRewriteResponse BagsRewriter::rewriteToSet(const TNode& n) const -{ - Assert(n.getKind() == Kind::BAG_TO_SET); - if (n[0].getKind() == Kind::BAG_MAKE && n[0][1].isConst() - && n[0][1].getConst().sgn() == 1) - { - // (bag.to_set (bag x n)) = (set.singleton x) - // where n is a positive constant and T is the type of the bag's elements - Node set = d_nm->mkNode(Kind::SET_SINGLETON, n[0][0]); - return BagsRewriteResponse(set, Rewrite::TO_SINGLETON); - } - return BagsRewriteResponse(n, Rewrite::NONE); -} - BagsRewriteResponse BagsRewriter::postRewriteEqual(const TNode& n) const { Assert(n.getKind() == Kind::EQUAL); diff --git a/src/theory/bags/bags_rewriter.h b/src/theory/bags/bags_rewriter.h index fbe688fb41a..c4e2e475be1 100644 --- a/src/theory/bags/bags_rewriter.h +++ b/src/theory/bags/bags_rewriter.h @@ -95,10 +95,10 @@ class BagsRewriter : public TheoryRewriter /** * rewrites for n include: - * - (bag.duplicate_removal (bag x n)) = (bag x 1) + * - (bag.setof (bag x n)) = (bag x 1) * where n is a positive constant */ - BagsRewriteResponse rewriteDuplicateRemoval(const TNode& n) const; + BagsRewriteResponse rewriteSetof(const TNode& n) const; /** * rewrites for n include: @@ -190,25 +190,6 @@ class BagsRewriter : public TheoryRewriter */ BagsRewriteResponse rewriteCard(const TNode& n) const; - /** - * rewrites for n include: - * - (bag.is_singleton (bag x c)) = (c == 1) - */ - BagsRewriteResponse rewriteIsSingleton(const TNode& n) const; - - /** - * rewrites for n include: - * - (bag.from_set (set.singleton x)) = (bag x 1) - */ - BagsRewriteResponse rewriteFromSet(const TNode& n) const; - - /** - * rewrites for n include: - * - (bag.to_set (bag x n)) = (set.singleton x) - * where n is a positive constant and T is the type of the bag's elements - */ - BagsRewriteResponse rewriteToSet(const TNode& n) const; - /** * rewrites for n include: * - (= A A) = true diff --git a/src/theory/bags/bags_utils.cpp b/src/theory/bags/bags_utils.cpp index 1c1accce675..9310c4d1886 100644 --- a/src/theory/bags/bags_utils.cpp +++ b/src/theory/bags/bags_utils.cpp @@ -132,16 +132,13 @@ Node BagsUtils::evaluate(Rewriter* rewriter, TNode n) { case Kind::BAG_MAKE: return evaluateMakeBag(n); case Kind::BAG_COUNT: return evaluateBagCount(n); - case Kind::BAG_DUPLICATE_REMOVAL: return evaluateDuplicateRemoval(n); + case Kind::BAG_SETOF: return evaluateSetof(n); case Kind::BAG_UNION_DISJOINT: return evaluateUnionDisjoint(n); case Kind::BAG_UNION_MAX: return evaluateUnionMax(n); case Kind::BAG_INTER_MIN: return evaluateIntersectionMin(n); case Kind::BAG_DIFFERENCE_SUBTRACT: return evaluateDifferenceSubtract(n); case Kind::BAG_DIFFERENCE_REMOVE: return evaluateDifferenceRemove(n); case Kind::BAG_CARD: return evaluateCard(n); - case Kind::BAG_IS_SINGLETON: return evaluateIsSingleton(n); - case Kind::BAG_FROM_SET: return evaluateFromSet(n); - case Kind::BAG_TO_SET: return evaluateToSet(n); case Kind::BAG_MAP: return evaluateBagMap(n); case Kind::BAG_FILTER: return evaluateBagFilter(n); case Kind::BAG_FOLD: return evaluateBagFold(n); @@ -301,16 +298,16 @@ Node BagsUtils::evaluateBagCount(TNode n) return nm->mkConstInt(Rational(0)); } -Node BagsUtils::evaluateDuplicateRemoval(TNode n) +Node BagsUtils::evaluateSetof(TNode n) { - Assert(n.getKind() == Kind::BAG_DUPLICATE_REMOVAL); + Assert(n.getKind() == Kind::BAG_SETOF); // Examples // -------- - // - (bag.duplicate_removal (as bag.empty (Bag String))) = (as bag.empty (Bag + // - (bag.setof (as bag.empty (Bag String))) = (as bag.empty (Bag // String)) - // - (bag.duplicate_removal (bag "x" 4)) = (bag "x" 1) - // - (bag.duplicate_removal (bag.disjoint_union (bag "x" 3) (bag "y" 5)) = + // - (bag.setof (bag "x" 4)) = (bag "x" 1) + // - (bag.setof (bag.disjoint_union (bag "x" 3) (bag "y" 5)) = // (bag.disjoint_union (bag "x" 1) (bag "y" 1) std::map oldElements = getBagElements(n[0]); @@ -630,73 +627,6 @@ Node BagsUtils::evaluateCard(TNode n) return sumNode; } -Node BagsUtils::evaluateIsSingleton(TNode n) -{ - Assert(n.getKind() == Kind::BAG_IS_SINGLETON); - // Examples - // -------- - // - (bag.is_singleton (as bag.empty (Bag String))) = false - // - (bag.is_singleton (bag "x" 1)) = true - // - (bag.is_singleton (bag "x" 4)) = false - // - (bag.is_singleton (bag.union_disjoint (bag "x" 1) (bag "y" 1))) - // = false - - if (n[0].getKind() == Kind::BAG_MAKE && n[0][1].getConst().isOne()) - { - return NodeManager::currentNM()->mkConst(true); - } - return NodeManager::currentNM()->mkConst(false); -} - -Node BagsUtils::evaluateFromSet(TNode n) -{ - Assert(n.getKind() == Kind::BAG_FROM_SET); - - // Examples - // -------- - // - (bag.from_set (as set.empty (Set String))) = (as bag.empty (Bag String)) - // - (bag.from_set (set.singleton "x")) = (bag "x" 1) - // - (bag.from_set (set.union (set.singleton "x") (set.singleton "y"))) = - // (bag.disjoint_union (bag "x" 1) (bag "y" 1)) - - NodeManager* nm = NodeManager::currentNM(); - std::set setElements = - sets::NormalForm::getElementsFromNormalConstant(n[0]); - Rational one = Rational(1); - std::map bagElements; - for (const Node& element : setElements) - { - bagElements[element] = one; - } - TypeNode bagType = nm->mkBagType(n[0].getType().getSetElementType()); - Node bag = constructConstantBagFromElements(bagType, bagElements); - return bag; -} - -Node BagsUtils::evaluateToSet(TNode n) -{ - Assert(n.getKind() == Kind::BAG_TO_SET); - - // Examples - // -------- - // - (bag.to_set (as bag.empty (Bag String))) = (as set.empty (Set String)) - // - (bag.to_set (bag "x" 4)) = (set.singleton "x") - // - (bag.to_set (bag.disjoint_union (bag "x" 3) (bag "y" 5)) = - // (set.union (set.singleton "x") (set.singleton "y"))) - - NodeManager* nm = NodeManager::currentNM(); - std::map bagElements = getBagElements(n[0]); - std::set setElements; - std::map::const_reverse_iterator it; - for (it = bagElements.rbegin(); it != bagElements.rend(); it++) - { - setElements.insert(it->first); - } - TypeNode setType = nm->mkSetType(n[0].getType().getBagElementType()); - Node set = sets::NormalForm::elementsToSet(setElements, setType); - return set; -} - Node BagsUtils::evaluateBagMap(TNode n) { Assert(n.getKind() == Kind::BAG_MAP); diff --git a/src/theory/bags/bags_utils.h b/src/theory/bags/bags_utils.h index ab2f71d144b..c595a2a8b91 100644 --- a/src/theory/bags/bags_utils.h +++ b/src/theory/bags/bags_utils.h @@ -206,11 +206,11 @@ class BagsUtils static Node evaluateBagCount(TNode n); /** - * @param n has the form (bag.duplicate_removal A) where A is a constant bag + * @param n has the form (bag.setof A) where A is a constant bag * @return a constant bag constructed from the elements in A where each * element has multiplicity one */ - static Node evaluateDuplicateRemoval(TNode n); + static Node evaluateSetof(TNode n); /** * evaluates union disjoint node such that the returned node is a canonical @@ -256,21 +256,6 @@ class BagsUtils * @return the number of elements in bag A */ static Node evaluateCard(TNode n); - /** - * @param n has the form (bag.is_singleton A) where A is a constant bag - * @return whether the bag A has cardinality one. - */ - static Node evaluateIsSingleton(TNode n); - /** - * @param n has the form (bag.from_set A) where A is a constant set - * @return a constant bag that contains exactly the elements in A. - */ - static Node evaluateFromSet(TNode n); - /** - * @param n has the form (bag.to_set A) where A is a constant bag - * @return a constant set constructed from the elements in A. - */ - static Node evaluateToSet(TNode n); /** * @param n has the form (bag.map f A) where A is a constant bag * @return a constant bag constructed from the images of elements in A. diff --git a/src/theory/bags/inference_generator.cpp b/src/theory/bags/inference_generator.cpp index 40ff9e3a2e2..33841d51d62 100644 --- a/src/theory/bags/inference_generator.cpp +++ b/src/theory/bags/inference_generator.cpp @@ -309,13 +309,13 @@ InferInfo InferenceGenerator::differenceRemove(Node n, Node e) return inferInfo; } -InferInfo InferenceGenerator::duplicateRemoval(Node n, Node e) +InferInfo InferenceGenerator::setof(Node n, Node e) { - Assert(n.getKind() == Kind::BAG_DUPLICATE_REMOVAL && n[0].getType().isBag()); + Assert(n.getKind() == Kind::BAG_SETOF && n[0].getType().isBag()); Assert(e.getType() == n[0].getType().getBagElementType()); Node A = n[0]; - InferInfo inferInfo(d_im, InferenceId::BAGS_DUPLICATE_REMOVAL); + InferInfo inferInfo(d_im, InferenceId::BAGS_SETOF); Node countA = getMultiplicityTerm(e, A); Node skolem = registerAndAssertSkolemLemma(n); diff --git a/src/theory/bags/inference_generator.h b/src/theory/bags/inference_generator.h index 8815423b9db..d10799d6bb6 100644 --- a/src/theory/bags/inference_generator.h +++ b/src/theory/bags/inference_generator.h @@ -180,7 +180,7 @@ class InferenceGenerator */ InferInfo differenceRemove(Node n, Node e); /** - * @param n is (bag.duplicate_removal A) where A is a bag of type (Bag E) + * @param n is (bag.setof A) where A is a bag of type (Bag E) * @param e is a node of Type E * @return an inference that represents the following implication * (=> @@ -188,9 +188,9 @@ class InferenceGenerator * (= * (bag.count e skolem) * (ite (>= (bag.count e A) 1) 1 0)))) - * where skolem is a fresh variable equals (bag.duplicate_removal A) + * where skolem is a fresh variable equals (bag.setof A) */ - InferInfo duplicateRemoval(Node n, Node e); + InferInfo setof(Node n, Node e); /** * @param cardTerm a term of the form (bag.card A) where A has type (Bag E) * @param n is (as bag.empty (Bag E)) diff --git a/src/theory/bags/kinds b/src/theory/bags/kinds index cf91ec318d3..e9da9d3c964 100644 --- a/src/theory/bags/kinds +++ b/src/theory/bags/kinds @@ -46,19 +46,14 @@ operator BAG_DIFFERENCE_SUBTRACT 2 "bag difference1 (subtracts multiplicitie # {|("a", 2), ("b", 3)} \\ {("a", 1)|} = {|("b", 3)|} operator BAG_DIFFERENCE_REMOVE 2 "bag difference remove (removes shared elements)" -operator BAG_SUBBAG 2 "inclusion predicate for bags (less than or equal multiplicities)" -operator BAG_COUNT 2 "multiplicity of an element in a bag" -operator BAG_MEMBER 2 "bag membership predicate; is first parameter a member of second?" -operator BAG_DUPLICATE_REMOVAL 1 "eliminate duplicates in a bag (also known as the delta operator,or the squash operator)" +operator BAG_SUBBAG 2 "inclusion predicate for bags (less than or equal multiplicities)" +operator BAG_COUNT 2 "multiplicity of an element in a bag" +operator BAG_MEMBER 2 "bag membership predicate; is first parameter a member of second?" +operator BAG_SETOF 1 "eliminate duplicates in a bag (also known as the delta operator,or the squash operator)" -operator BAG_MAKE 2 "constructs a bag from one element along with its multiplicity" - -# The operator bag-is-singleton returns whether the given bag is a singleton -operator BAG_IS_SINGLETON 1 "return whether the given bag is a singleton" +operator BAG_MAKE 2 "constructs a bag from one element along with its multiplicity" operator BAG_CARD 1 "bag cardinality operator" -operator BAG_FROM_SET 1 "converts a set to a bag" -operator BAG_TO_SET 1 "converts a bag to a set" # The operator choose returns an element from a given bag. # If bag A = {("a", 1)}, then the term (choose A) is equivalent to the term a. @@ -94,14 +89,11 @@ typerule BAG_DIFFERENCE_REMOVE ::cvc5::internal::theory::bags::BinaryOperatorT typerule BAG_SUBBAG ::cvc5::internal::theory::bags::SubBagTypeRule typerule BAG_COUNT ::cvc5::internal::theory::bags::CountTypeRule typerule BAG_MEMBER ::cvc5::internal::theory::bags::MemberTypeRule -typerule BAG_DUPLICATE_REMOVAL ::cvc5::internal::theory::bags::DuplicateRemovalTypeRule +typerule BAG_SETOF ::cvc5::internal::theory::bags::SetofTypeRule typerule BAG_MAKE ::cvc5::internal::theory::bags::BagMakeTypeRule typerule BAG_EMPTY ::cvc5::internal::theory::bags::EmptyBagTypeRule typerule BAG_CARD ::cvc5::internal::theory::bags::CardTypeRule typerule BAG_CHOOSE ::cvc5::internal::theory::bags::ChooseTypeRule -typerule BAG_IS_SINGLETON ::cvc5::internal::theory::bags::IsSingletonTypeRule -typerule BAG_FROM_SET ::cvc5::internal::theory::bags::FromSetTypeRule -typerule BAG_TO_SET ::cvc5::internal::theory::bags::ToSetTypeRule typerule BAG_MAP ::cvc5::internal::theory::bags::BagMapTypeRule typerule BAG_FILTER ::cvc5::internal::theory::bags::BagFilterTypeRule typerule BAG_FOLD ::cvc5::internal::theory::bags::BagFoldTypeRule diff --git a/src/theory/bags/rewrites.cpp b/src/theory/bags/rewrites.cpp index 76e6ca7ebb6..c2625d30c4a 100644 --- a/src/theory/bags/rewrites.cpp +++ b/src/theory/bags/rewrites.cpp @@ -34,8 +34,7 @@ const char* toString(Rewrite r) case Rewrite::CONSTANT_EVALUATION: return "CONSTANT_EVALUATION"; case Rewrite::COUNT_EMPTY: return "COUNT_EMPTY"; case Rewrite::COUNT_BAG_MAKE: return "COUNT_BAG_MAKE"; - case Rewrite::DUPLICATE_REMOVAL_BAG_MAKE: - return "DUPLICATE_REMOVAL_BAG_MAKE"; + case Rewrite::SETOF_BAG_MAKE: return "SETOF_BAG_MAKE"; case Rewrite::EQ_CONST_FALSE: return "EQ_CONST_FALSE"; case Rewrite::EQ_REFL: return "EQ_REFL"; case Rewrite::EQ_SYM: return "EQ_SYM"; diff --git a/src/theory/bags/rewrites.h b/src/theory/bags/rewrites.h index e428ce09a22..c3b1298a6ec 100644 --- a/src/theory/bags/rewrites.h +++ b/src/theory/bags/rewrites.h @@ -39,7 +39,7 @@ enum class Rewrite : uint32_t CONSTANT_EVALUATION, COUNT_EMPTY, COUNT_BAG_MAKE, - DUPLICATE_REMOVAL_BAG_MAKE, + SETOF_BAG_MAKE, EQ_CONST_FALSE, EQ_REFL, EQ_SYM, diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp index 154ae022fb5..4ec195f0bf3 100644 --- a/src/theory/bags/theory_bags.cpp +++ b/src/theory/bags/theory_bags.cpp @@ -76,11 +76,9 @@ void TheoryBags::finishInit() d_equalityEngine->addFunctionKind(Kind::BAG_DIFFERENCE_SUBTRACT); d_equalityEngine->addFunctionKind(Kind::BAG_DIFFERENCE_REMOVE); d_equalityEngine->addFunctionKind(Kind::BAG_COUNT); - d_equalityEngine->addFunctionKind(Kind::BAG_DUPLICATE_REMOVAL); + d_equalityEngine->addFunctionKind(Kind::BAG_SETOF); d_equalityEngine->addFunctionKind(Kind::BAG_MAKE); d_equalityEngine->addFunctionKind(Kind::BAG_CARD); - d_equalityEngine->addFunctionKind(Kind::BAG_FROM_SET); - d_equalityEngine->addFunctionKind(Kind::BAG_TO_SET); d_equalityEngine->addFunctionKind(Kind::BAG_PARTITION); d_equalityEngine->addFunctionKind(Kind::TABLE_PRODUCT); d_equalityEngine->addFunctionKind(Kind::TABLE_PROJECT); @@ -499,9 +497,6 @@ void TheoryBags::preRegisterTerm(TNode n) d_equalityEngine->addTerm(n); break; } - case Kind::BAG_FROM_SET: - case Kind::BAG_TO_SET: - case Kind::BAG_IS_SINGLETON: case Kind::BAG_PARTITION: { std::stringstream ss; diff --git a/src/theory/bags/theory_bags_type_rules.cpp b/src/theory/bags/theory_bags_type_rules.cpp index 6852c3c7b65..9e6d9fd4174 100644 --- a/src/theory/bags/theory_bags_type_rules.cpp +++ b/src/theory/bags/theory_bags_type_rules.cpp @@ -171,24 +171,23 @@ TypeNode MemberTypeRule::computeType(NodeManager* nodeManager, return nodeManager->booleanType(); } -TypeNode DuplicateRemovalTypeRule::preComputeType(NodeManager* nm, TNode n) +TypeNode SetofTypeRule::preComputeType(NodeManager* nm, TNode n) { return TypeNode::null(); } -TypeNode DuplicateRemovalTypeRule::computeType(NodeManager* nodeManager, - TNode n, - bool check, - std::ostream* errOut) +TypeNode SetofTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check, + std::ostream* errOut) { - Assert(n.getKind() == Kind::BAG_DUPLICATE_REMOVAL); + Assert(n.getKind() == Kind::BAG_SETOF); TypeNode bagType = n[0].getType(check); if (check) { if (!bagType.isBag()) { std::stringstream ss; - ss << "Applying BAG_DUPLICATE_REMOVAL on a non-bag argument in term " - << n; + ss << "Applying BAG_SETOF on a non-bag argument in term " << n; throw TypeCheckingExceptionPrivate(n, ss.str()); } } @@ -236,28 +235,6 @@ bool BagMakeTypeRule::computeIsConst(NodeManager* nodeManager, TNode n) && n[1].getConst().sgn() == 1; } -TypeNode IsSingletonTypeRule::preComputeType(NodeManager* nm, TNode n) -{ - return nm->booleanType(); -} -TypeNode IsSingletonTypeRule::computeType(NodeManager* nodeManager, - TNode n, - bool check, - std::ostream* errOut) -{ - Assert(n.getKind() == Kind::BAG_IS_SINGLETON); - TypeNode bagType = n[0].getType(check); - if (check) - { - if (!bagType.isBag()) - { - throw TypeCheckingExceptionPrivate( - n, "BAG_IS_SINGLETON operator expects a bag, a non-bag is found"); - } - } - return nodeManager->booleanType(); -} - TypeNode EmptyBagTypeRule::preComputeType(NodeManager* nm, TNode n) { return TypeNode::null(); @@ -316,54 +293,6 @@ TypeNode ChooseTypeRule::computeType(NodeManager* nodeManager, return bagType.getBagElementType(); } -TypeNode FromSetTypeRule::preComputeType(NodeManager* nm, TNode n) -{ - return TypeNode::null(); -} -TypeNode FromSetTypeRule::computeType(NodeManager* nodeManager, - TNode n, - bool check, - std::ostream* errOut) -{ - Assert(n.getKind() == Kind::BAG_FROM_SET); - TypeNode setType = n[0].getType(check); - if (check) - { - if (!setType.isSet()) - { - throw TypeCheckingExceptionPrivate( - n, "bag.from_set operator expects a set, a non-set is found"); - } - } - TypeNode elementType = setType.getSetElementType(); - TypeNode bagType = nodeManager->mkBagType(elementType); - return bagType; -} - -TypeNode ToSetTypeRule::preComputeType(NodeManager* nm, TNode n) -{ - return TypeNode::null(); -} -TypeNode ToSetTypeRule::computeType(NodeManager* nodeManager, - TNode n, - bool check, - std::ostream* errOut) -{ - Assert(n.getKind() == Kind::BAG_TO_SET); - TypeNode bagType = n[0].getType(check); - if (check) - { - if (!bagType.isBag()) - { - throw TypeCheckingExceptionPrivate( - n, "bag.to_set operator expects a bag, a non-bag is found"); - } - } - TypeNode elementType = bagType.getBagElementType(); - TypeNode setType = nodeManager->mkSetType(elementType); - return setType; -} - TypeNode BagMapTypeRule::preComputeType(NodeManager* nm, TNode n) { return TypeNode::null(); diff --git a/src/theory/bags/theory_bags_type_rules.h b/src/theory/bags/theory_bags_type_rules.h index 7c90a00d27c..1cd2c9c5823 100644 --- a/src/theory/bags/theory_bags_type_rules.h +++ b/src/theory/bags/theory_bags_type_rules.h @@ -83,16 +83,16 @@ struct MemberTypeRule }; /** - * Type rule for bag.duplicate_removal to check the argument is of a bag. + * Type rule for bag.setof to check the argument is of a bag. */ -struct DuplicateRemovalTypeRule +struct SetofTypeRule { static TypeNode preComputeType(NodeManager* nm, TNode n); static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check, std::ostream* errOut); -}; /* struct DuplicateRemovalTypeRule */ +}; /* struct SetofTypeRule */ /** * Type rule for (bag op e) operator to check the sort of e matches the sort @@ -108,18 +108,6 @@ struct BagMakeTypeRule static bool computeIsConst(NodeManager* nodeManager, TNode n); }; /* struct BagMakeTypeRule */ -/** - * Type rule for (bag.is_singleton B) to check the argument B is a bag. - */ -struct IsSingletonTypeRule -{ - static TypeNode preComputeType(NodeManager* nm, TNode n); - static TypeNode computeType(NodeManager* nodeManager, - TNode n, - bool check, - std::ostream* errOut); -}; /* struct IsSingletonTypeRule */ - /** * Type rule for (as bag.empty (Bag T)) where T is a type */ @@ -156,30 +144,6 @@ struct ChooseTypeRule std::ostream* errOut); }; /* struct ChooseTypeRule */ -/** - * Type rule for (bag.from_set ..) to check the argument is of a set. - */ -struct FromSetTypeRule -{ - static TypeNode preComputeType(NodeManager* nm, TNode n); - static TypeNode computeType(NodeManager* nodeManager, - TNode n, - bool check, - std::ostream* errOut); -}; /* struct FromSetTypeRule */ - -/** - * Type rule for (bag.to_set ..) to check the argument is of a bag. - */ -struct ToSetTypeRule -{ - static TypeNode preComputeType(NodeManager* nm, TNode n); - static TypeNode computeType(NodeManager* nodeManager, - TNode n, - bool check, - std::ostream* errOut); -}; /* struct ToSetTypeRule */ - /** * Type rule for (bag.map f B) to make sure f is a unary function of type * (-> T1 T2) where B is a bag of type (Bag T1) diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index 63970290822..a7610361c00 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -136,7 +136,7 @@ const char* toString(InferenceId i) case InferenceId::BAGS_DIFFERENCE_SUBTRACT: return "BAGS_DIFFERENCE_SUBTRACT"; case InferenceId::BAGS_DIFFERENCE_REMOVE: return "BAGS_DIFFERENCE_REMOVE"; - case InferenceId::BAGS_DUPLICATE_REMOVAL: return "BAGS_DUPLICATE_REMOVAL"; + case InferenceId::BAGS_SETOF: return "BAGS_SETOF"; case InferenceId::BAGS_MAP_DOWN: return "BAGS_MAP_DOWN"; case InferenceId::BAGS_MAP_DOWN_INJECTIVE: return "BAGS_MAP_DOWN_INJECTIVE"; case InferenceId::BAGS_MAP_UP1: return "BAGS_MAP_UP1"; diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index 41a4ba91440..1fdb1ef5daa 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -210,7 +210,7 @@ enum class InferenceId BAGS_INTERSECTION_MIN, BAGS_DIFFERENCE_SUBTRACT, BAGS_DIFFERENCE_REMOVE, - BAGS_DUPLICATE_REMOVAL, + BAGS_SETOF, BAGS_MAP_DOWN, BAGS_MAP_DOWN_INJECTIVE, BAGS_MAP_UP1, diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index 948f9cbc3fa..1971ba54f19 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -2146,8 +2146,8 @@ set(regress_1_tests regress1/bags/ctor_previous_sat.smt2 regress1/bags/difference_remove1.smt2 regress1/bags/disequality.smt2 - regress1/bags/duplicate_removal1.smt2 - regress1/bags/duplicate_removal2.smt2 + regress1/bags/setof1.smt2 + regress1/bags/setof2.smt2 regress1/bags/emptybag1.smt2 regress1/bags/filter1.smt2 regress1/bags/filter2.smt2 diff --git a/test/regress/cli/regress1/bags/proj-issue566.smt2 b/test/regress/cli/regress1/bags/proj-issue566.smt2 index 1f11f0073e0..504ee07a06f 100644 --- a/test/regress/cli/regress1/bags/proj-issue566.smt2 +++ b/test/regress/cli/regress1/bags/proj-issue566.smt2 @@ -2,5 +2,5 @@ (set-info :status sat) (set-option :debug-check-models true) (declare-const x (Bag Bool)) -(assert (= (bag.card (bag.union_disjoint x x)) (bag.card (bag.duplicate_removal (bag.union_disjoint x x))))) +(assert (= (bag.card (bag.union_disjoint x x)) (bag.card (bag.setof (bag.union_disjoint x x))))) (check-sat) diff --git a/test/regress/cli/regress1/bags/duplicate_removal1.smt2 b/test/regress/cli/regress1/bags/setof1.smt2 similarity index 83% rename from test/regress/cli/regress1/bags/duplicate_removal1.smt2 rename to test/regress/cli/regress1/bags/setof1.smt2 index 27ce2360b5e..59dcce0bec0 100644 --- a/test/regress/cli/regress1/bags/duplicate_removal1.smt2 +++ b/test/regress/cli/regress1/bags/setof1.smt2 @@ -3,6 +3,6 @@ (set-option :produce-models true) (declare-fun A () (Bag String)) (declare-fun B () (Bag String)) -(assert (= B (bag.duplicate_removal A))) +(assert (= B (bag.setof A))) (assert (distinct (as bag.empty (Bag String)) A B)) (check-sat) diff --git a/test/regress/cli/regress1/bags/duplicate_removal2.smt2 b/test/regress/cli/regress1/bags/setof2.smt2 similarity index 83% rename from test/regress/cli/regress1/bags/duplicate_removal2.smt2 rename to test/regress/cli/regress1/bags/setof2.smt2 index 5382f773f57..943ad6cf473 100644 --- a/test/regress/cli/regress1/bags/duplicate_removal2.smt2 +++ b/test/regress/cli/regress1/bags/setof2.smt2 @@ -2,7 +2,7 @@ (set-info :status unsat) (declare-fun A () (Bag String)) (declare-fun B () (Bag String)) -(assert (= B (bag.duplicate_removal A))) +(assert (= B (bag.setof A))) (assert (distinct (as bag.empty (Bag String)) A B)) (assert (= B (bag.union_max A B))) (check-sat) \ No newline at end of file diff --git a/test/unit/theory/theory_bags_normal_form_white.cpp b/test/unit/theory/theory_bags_normal_form_white.cpp index 03b979ebd56..b180ef2db4b 100644 --- a/test/unit/theory/theory_bags_normal_form_white.cpp +++ b/test/unit/theory/theory_bags_normal_form_white.cpp @@ -137,19 +137,19 @@ TEST_F(TestTheoryWhiteBagsNormalForm, bag_count) ASSERT_EQ(output4, rewrite(input4)); } -TEST_F(TestTheoryWhiteBagsNormalForm, duplicate_removal) +TEST_F(TestTheoryWhiteBagsNormalForm, setof) { // Examples // -------- - // - (bag.duplicate_removal (as bag.empty (Bag String))) = (as bag.empty (Bag + // - (bag.setof (as bag.empty (Bag String))) = (as bag.empty (Bag // String)) - // - (bag.duplicate_removal (bag "x" 4)) = (bag.empty"x" 1) - // - (bag.duplicate_removal (bag.union_disjoint(bag "x" 3) (bag "y" 5)) = + // - (bag.setof (bag "x" 4)) = (bag.empty"x" 1) + // - (bag.setof (bag.union_disjoint(bag "x" 3) (bag "y" 5)) = // (bag.union_disjoint(bag "x" 1) (bag "y" 1) Node emptybag = d_nodeManager->mkConst( EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType()))); - Node input1 = d_nodeManager->mkNode(Kind::BAG_DUPLICATE_REMOVAL, emptybag); + Node input1 = d_nodeManager->mkNode(Kind::BAG_SETOF, emptybag); Node output1 = emptybag; ASSERT_EQ(output1, rewrite(input1)); @@ -166,12 +166,12 @@ TEST_F(TestTheoryWhiteBagsNormalForm, duplicate_removal) Node y_5 = d_nodeManager->mkNode( Kind::BAG_MAKE, y, d_nodeManager->mkConstInt(Rational(5))); - Node input2 = d_nodeManager->mkNode(Kind::BAG_DUPLICATE_REMOVAL, x_4); + Node input2 = d_nodeManager->mkNode(Kind::BAG_SETOF, x_4); Node output2 = x_1; ASSERT_EQ(output2, rewrite(input2)); Node normalBag = d_nodeManager->mkNode(Kind::BAG_UNION_DISJOINT, x_4, y_5); - Node input3 = d_nodeManager->mkNode(Kind::BAG_DUPLICATE_REMOVAL, normalBag); + Node input3 = d_nodeManager->mkNode(Kind::BAG_SETOF, normalBag); Node output3 = d_nodeManager->mkNode(Kind::BAG_UNION_DISJOINT, x_1, y_1); ASSERT_EQ(output3, rewrite(input3)); } @@ -438,125 +438,5 @@ TEST_F(TestTheoryWhiteBagsNormalForm, bag_card) ASSERT_EQ(output3, rewrite(input3)); } -TEST_F(TestTheoryWhiteBagsNormalForm, is_singleton) -{ - // Examples - // -------- - // - (bag.is_singleton (as bag.empty (Bag String))) = false - // - (bag.is_singleton (bag "x" 1)) = true - // - (bag.is_singleton (bag "x" 4)) = false - // - (bag.is_singleton (bag.union_disjoint (bag "x" 1) (bag "y" 1))) = - // false - Node falseNode = d_nodeManager->mkConst(false); - Node trueNode = d_nodeManager->mkConst(true); - Node empty = d_nodeManager->mkConst( - EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType()))); - Node x = d_nodeManager->mkConst(String("x")); - Node y = d_nodeManager->mkConst(String("y")); - Node z = d_nodeManager->mkConst(String("z")); - Node x_1 = d_nodeManager->mkNode( - Kind::BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(1))); - Node x_4 = d_nodeManager->mkNode( - Kind::BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(4))); - Node y_1 = d_nodeManager->mkNode( - Kind::BAG_MAKE, y, d_nodeManager->mkConstInt(Rational(1))); - - Node input1 = d_nodeManager->mkNode(Kind::BAG_IS_SINGLETON, empty); - Node output1 = falseNode; - ASSERT_EQ(output1, rewrite(input1)); - - Node input2 = d_nodeManager->mkNode(Kind::BAG_IS_SINGLETON, x_1); - Node output2 = trueNode; - ASSERT_EQ(output2, rewrite(input2)); - - Node input3 = d_nodeManager->mkNode(Kind::BAG_IS_SINGLETON, x_4); - Node output3 = falseNode; - ASSERT_EQ(output2, rewrite(input2)); - - Node union_disjoint = - d_nodeManager->mkNode(Kind::BAG_UNION_DISJOINT, x_1, y_1); - Node input4 = d_nodeManager->mkNode(Kind::BAG_IS_SINGLETON, union_disjoint); - Node output4 = falseNode; - ASSERT_EQ(output3, rewrite(input3)); -} - -TEST_F(TestTheoryWhiteBagsNormalForm, from_set) -{ - // Examples - // -------- - // - (bag.from_set (as set.empty (Bag String))) = (as bag.empty (Bag String)) - // - (bag.from_set (set.singleton "x")) = (bag "x" 1) - // - (bag.from_set (set.union (set.singleton "x") (set.singleton "y"))) = - // (bag.union_disjoint (bag "x" 1) (bag "y" 1)) - - Node emptyset = d_nodeManager->mkConst( - EmptySet(d_nodeManager->mkSetType(d_nodeManager->stringType()))); - Node emptybag = d_nodeManager->mkConst( - EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType()))); - Node input1 = d_nodeManager->mkNode(Kind::BAG_FROM_SET, emptyset); - Node output1 = emptybag; - ASSERT_EQ(output1, rewrite(input1)); - - Node x = d_nodeManager->mkConst(String("x")); - Node y = d_nodeManager->mkConst(String("y")); - - Node xSingleton = d_nodeManager->mkNode(Kind::SET_SINGLETON, x); - Node ySingleton = d_nodeManager->mkNode(Kind::SET_SINGLETON, y); - - Node x_1 = d_nodeManager->mkNode( - Kind::BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(1))); - Node y_1 = d_nodeManager->mkNode( - Kind::BAG_MAKE, y, d_nodeManager->mkConstInt(Rational(1))); - - Node input2 = d_nodeManager->mkNode(Kind::BAG_FROM_SET, xSingleton); - Node output2 = x_1; - ASSERT_EQ(output2, rewrite(input2)); - - // for normal sets, the first node is the largest, not smallest - Node normalSet = - d_nodeManager->mkNode(Kind::SET_UNION, ySingleton, xSingleton); - Node input3 = d_nodeManager->mkNode(Kind::BAG_FROM_SET, normalSet); - Node output3 = d_nodeManager->mkNode(Kind::BAG_UNION_DISJOINT, x_1, y_1); - ASSERT_EQ(output3, rewrite(input3)); -} - -TEST_F(TestTheoryWhiteBagsNormalForm, to_set) -{ - // Examples - // -------- - // - (bag.to_set (as bag.empty (Bag String))) = (as set.empty (Bag String)) - // - (bag.to_set (bag "x" 4)) = (set.singleton "x") - // - (bag.to_set (bag.union_disjoint(bag "x" 3) (bag "y" 5)) = - // (set.union (set.singleton "x") (set.singleton "y"))) - - Node emptyset = d_nodeManager->mkConst( - EmptySet(d_nodeManager->mkSetType(d_nodeManager->stringType()))); - Node emptybag = d_nodeManager->mkConst( - EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType()))); - Node input1 = d_nodeManager->mkNode(Kind::BAG_TO_SET, emptybag); - Node output1 = emptyset; - ASSERT_EQ(output1, rewrite(input1)); - - Node x = d_nodeManager->mkConst(String("x")); - Node y = d_nodeManager->mkConst(String("y")); - - Node xSingleton = d_nodeManager->mkNode(Kind::SET_SINGLETON, x); - Node ySingleton = d_nodeManager->mkNode(Kind::SET_SINGLETON, y); - - Node x_4 = d_nodeManager->mkNode( - Kind::BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(4))); - Node y_5 = d_nodeManager->mkNode( - Kind::BAG_MAKE, y, d_nodeManager->mkConstInt(Rational(5))); - - Node input2 = d_nodeManager->mkNode(Kind::BAG_TO_SET, x_4); - Node output2 = xSingleton; - ASSERT_EQ(output2, rewrite(input2)); - - // for normal sets, the first node is the largest, not smallest - Node normalBag = d_nodeManager->mkNode(Kind::BAG_UNION_DISJOINT, x_4, y_5); - Node input3 = d_nodeManager->mkNode(Kind::BAG_TO_SET, normalBag); - Node output3 = d_nodeManager->mkNode(Kind::SET_UNION, ySingleton, xSingleton); - ASSERT_EQ(output3, rewrite(input3)); -} } // namespace test } // namespace cvc5::internal diff --git a/test/unit/theory/theory_bags_rewriter_white.cpp b/test/unit/theory/theory_bags_rewriter_white.cpp index 23e547dc82b..280556f4c00 100644 --- a/test/unit/theory/theory_bags_rewriter_white.cpp +++ b/test/unit/theory/theory_bags_rewriter_white.cpp @@ -183,14 +183,14 @@ TEST_F(TestTheoryWhiteBagsRewriter, bag_count) && response2.d_node == three); } -TEST_F(TestTheoryWhiteBagsRewriter, duplicate_removal) +TEST_F(TestTheoryWhiteBagsRewriter, setof) { Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType()); Node bag = d_nodeManager->mkNode( Kind::BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(5))); - // (bag.duplicate_removal (bag x n)) = (bag x 1) - Node n = d_nodeManager->mkNode(Kind::BAG_DUPLICATE_REMOVAL, bag); + // (bag.setof (bag x n)) = (bag x 1) + Node n = d_nodeManager->mkNode(Kind::BAG_SETOF, bag); RewriteResponse response = d_rewriter->postRewrite(n); Node noDuplicate = d_nodeManager->mkNode( Kind::BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(1))); @@ -649,57 +649,6 @@ TEST_F(TestTheoryWhiteBagsRewriter, bag_card) && response2.d_status == REWRITE_AGAIN_FULL); } -TEST_F(TestTheoryWhiteBagsRewriter, is_singleton) -{ - Node emptybag = d_nodeManager->mkConst( - EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType()))); - Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType()); - Node c = d_skolemManager->mkDummySkolem("c", d_nodeManager->integerType()); - Node bag = d_nodeManager->mkNode(Kind::BAG_MAKE, x, c); - - // (bag.is_singleton (as bag.empty (Bag String)) = false - Node n1 = d_nodeManager->mkNode(Kind::BAG_IS_SINGLETON, emptybag); - RewriteResponse response1 = d_rewriter->postRewrite(n1); - ASSERT_TRUE(response1.d_node == d_nodeManager->mkConst(false) - && response1.d_status == REWRITE_AGAIN_FULL); - - // (bag.is_singleton (bag x c) = (c == 1) - Node n2 = d_nodeManager->mkNode(Kind::BAG_IS_SINGLETON, bag); - RewriteResponse response2 = d_rewriter->postRewrite(n2); - Node one = d_nodeManager->mkConstInt(Rational(1)); - Node equal = c.eqNode(one); - ASSERT_TRUE(response2.d_node == equal - && response2.d_status == REWRITE_AGAIN_FULL); -} - -TEST_F(TestTheoryWhiteBagsRewriter, from_set) -{ - Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType()); - Node singleton = d_nodeManager->mkNode(Kind::SET_SINGLETON, x); - - // (bag.from_set (set.singleton (set.singleton_op Int) x)) = (bag x 1) - Node n = d_nodeManager->mkNode(Kind::BAG_FROM_SET, singleton); - RewriteResponse response = d_rewriter->postRewrite(n); - Node one = d_nodeManager->mkConstInt(Rational(1)); - Node bag = d_nodeManager->mkNode(Kind::BAG_MAKE, x, one); - ASSERT_TRUE(response.d_node == bag - && response.d_status == REWRITE_AGAIN_FULL); -} - -TEST_F(TestTheoryWhiteBagsRewriter, to_set) -{ - Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType()); - Node bag = d_nodeManager->mkNode( - Kind::BAG_MAKE, x, d_nodeManager->mkConstInt(Rational(5))); - - // (bag.to_set (bag x n)) = (set.singleton (set.singleton_op T) x) - Node n = d_nodeManager->mkNode(Kind::BAG_TO_SET, bag); - RewriteResponse response = d_rewriter->postRewrite(n); - Node singleton = d_nodeManager->mkNode(Kind::SET_SINGLETON, x); - ASSERT_TRUE(response.d_node == singleton - && response.d_status == REWRITE_AGAIN_FULL); -} - TEST_F(TestTheoryWhiteBagsRewriter, map) { Rewriter* rr = d_slvEngine->getEnv().getRewriter(); diff --git a/test/unit/theory/theory_bags_type_rules_white.cpp b/test/unit/theory/theory_bags_type_rules_white.cpp index 4a04d27fe43..7c129112a47 100644 --- a/test/unit/theory/theory_bags_type_rules_white.cpp +++ b/test/unit/theory/theory_bags_type_rules_white.cpp @@ -60,13 +60,13 @@ TEST_F(TestTheoryWhiteBagsTypeRule, count_operator) TypeCheckingExceptionPrivate); } -TEST_F(TestTheoryWhiteBagsTypeRule, duplicate_removal_operator) +TEST_F(TestTheoryWhiteBagsTypeRule, setof_operator) { std::vector elements = getNStrings(1); Node bag = d_nodeManager->mkNode( Kind::BAG_MAKE, elements[0], d_nodeManager->mkConstInt(Rational(10))); - ASSERT_NO_THROW(d_nodeManager->mkNode(Kind::BAG_DUPLICATE_REMOVAL, bag)); - ASSERT_EQ(d_nodeManager->mkNode(Kind::BAG_DUPLICATE_REMOVAL, bag).getType(), + ASSERT_NO_THROW(d_nodeManager->mkNode(Kind::BAG_SETOF, bag)); + ASSERT_EQ(d_nodeManager->mkNode(Kind::BAG_SETOF, bag).getType(), bag.getType()); } @@ -86,23 +86,6 @@ TEST_F(TestTheoryWhiteBagsTypeRule, mkBag_operator) ASSERT_TRUE(BagMakeTypeRule::computeIsConst(d_nodeManager, positive)); } -TEST_F(TestTheoryWhiteBagsTypeRule, from_set_operator) -{ - std::vector elements = getNStrings(1); - Node set = d_nodeManager->mkNode(Kind::SET_SINGLETON, elements[0]); - ASSERT_NO_THROW(d_nodeManager->mkNode(Kind::BAG_FROM_SET, set)); - ASSERT_TRUE(d_nodeManager->mkNode(Kind::BAG_FROM_SET, set).getType().isBag()); -} - -TEST_F(TestTheoryWhiteBagsTypeRule, to_set_operator) -{ - std::vector elements = getNStrings(1); - Node bag = d_nodeManager->mkNode( - Kind::BAG_MAKE, elements[0], d_nodeManager->mkConstInt(Rational(10))); - ASSERT_NO_THROW(d_nodeManager->mkNode(Kind::BAG_TO_SET, bag)); - ASSERT_TRUE(d_nodeManager->mkNode(Kind::BAG_TO_SET, bag).getType().isSet()); -} - TEST_F(TestTheoryWhiteBagsTypeRule, map_operator) { std::vector elements = getNStrings(1); From 3d74425f9520dee224b15a25b56eacb60b5c06aa Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 28 Feb 2024 09:05:27 -0600 Subject: [PATCH 3/5] Update news (#10434) In preparation for 1.1.2. --- NEWS.md | 28 ++++++++++++++++++++++++++-- 1 file changed, 26 insertions(+), 2 deletions(-) diff --git a/NEWS.md b/NEWS.md index d797c6f11d3..c73e6e19c82 100644 --- a/NEWS.md +++ b/NEWS.md @@ -1,21 +1,45 @@ This file contains a summary of important user-visible changes. +cvc5 1.1.2 +========== + ## New Features -- Added support for nullable sorts and lift operator to the theory of datatypes. +- Added support for **nullable** sorts and lift operator to the theory of **datatypes**. +- Adds a new strategy `--sub-cbqi` (disabled by default) for **quantifier + instantiation** which uses subsolvers to compute unsat cores of instantiations + that are used in proofs of unsatisfiability. ## Changes +- SAT clauses are no longer marked as removable in MiniSat. This change + **improves performance** overall on quantifier-free logics with arithmetic and + strings. - **API** * Functions `kindToString(Kind)` and `sortKindToString(SortKind)` are now deprecated and replaced by `std::to_string(Kind)` and `std::to_string(SortKind)`. They will be removed in the next minor release. - +- Minor changes to the output format for proofs. Proofs in the AletheLF + proof format generated by cvc5 now correspond directly to their representation + in proof objects obtained in via the API (the `Proof` class). Moreover, + proofs now use SMT-LIB compliant syntax for quantified formulas and unary + arithmetic negation. +- The option `--safe-options` now disallows cases where more than one regular + option is used. +- Fixes the parsing of `define-fun-rec` and `define-funs-rec` in interactive + mode. - Renamed `bag.duplicate_removal` to `bag.setof`. cvc5 1.1.1 ========== +## New Features + +- Added support for **forward declarations** (feature `:fwd-decls`) in **SyGuS** + inputs. This allows functions-to-synthesize to include previous + functions-to-synthesize in their grammars. This feature is enabled by default + for all SyGuS inputs. + ## Changes - Fixed a bug when piping input from stdin, which caused cvc5 to have degraded From 77ecb4bad4a66ee25eaccbb0df487b7483840ff0 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Wed, 28 Feb 2024 14:03:21 -0300 Subject: [PATCH 4/5] Migrating fixes and error handling for Alethe from branch --- src/proof/alethe/alethe_node_converter.cpp | 25 +- src/proof/alethe/alethe_node_converter.h | 6 + src/proof/alethe/alethe_post_processor.cpp | 283 ++++++++++++++------- src/proof/alethe/alethe_post_processor.h | 21 +- src/proof/alethe/alethe_printer.cpp | 15 +- src/proof/alethe/alethe_proof_rule.cpp | 3 +- src/proof/proof_checker.cpp | 5 + src/proof/proof_checker.h | 3 + src/smt/proof_manager.cpp | 32 ++- 9 files changed, 289 insertions(+), 104 deletions(-) diff --git a/src/proof/alethe/alethe_node_converter.cpp b/src/proof/alethe/alethe_node_converter.cpp index 66ee699e8ce..e31ddda9f94 100644 --- a/src/proof/alethe/alethe_node_converter.cpp +++ b/src/proof/alethe/alethe_node_converter.cpp @@ -22,12 +22,31 @@ namespace cvc5::internal { namespace proof { +Node AletheNodeConverter::maybeConvert(Node n) +{ + d_error = ""; + Node res = convert(n); + if (!d_error.empty()) + { + return Node::null(); + } + return res; +} + Node AletheNodeConverter::postConvert(Node n) { NodeManager* nm = NodeManager::currentNM(); Kind k = n.getKind(); switch (k) { + case Kind::BITVECTOR_EAGER_ATOM: + { + std::stringstream ss; + ss << "Proof uses eager bit-blasting, which does not have support for " + "Alethe proofs."; + d_error = ss.str(); + return Node::null(); + } case Kind::SKOLEM: { Trace("alethe-conv") << "AletheNodeConverter: handling skolem " << n @@ -108,7 +127,11 @@ Node AletheNodeConverter::postConvert(Node n) return convert(witness); } } - Unreachable() << "Fresh Skolem " << sfi << " is not allowed\n"; + std::stringstream ss; + ss << "Proof contains Skolem (kind " << sfi << ", term " << n + << ") is not supported by Alethe."; + d_error = ss.str(); + return Node::null(); } case Kind::FORALL: { diff --git a/src/proof/alethe/alethe_node_converter.h b/src/proof/alethe/alethe_node_converter.h index 31956fa1d77..652c9c97221 100644 --- a/src/proof/alethe/alethe_node_converter.h +++ b/src/proof/alethe/alethe_node_converter.h @@ -37,6 +37,12 @@ class AletheNodeConverter : public BaseAlfNodeConverter /** convert at post-order traversal */ Node postConvert(Node n) override; + Node maybeConvert(Node n); + + std::string d_error; + + std::map d_convToOriginalAssumption; + private: /** * Make or get an internal symbol with custom name and type. diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp index 41bd3a4b2db..dba170113ea 100644 --- a/src/proof/alethe/alethe_post_processor.cpp +++ b/src/proof/alethe/alethe_post_processor.cpp @@ -59,8 +59,14 @@ std::unordered_map s_bvKindToAletheRule = { }; AletheProofPostprocessCallback::AletheProofPostprocessCallback( - Env& env, AletheNodeConverter& anc, bool resPivots) - : EnvObj(env), d_anc(anc), d_resPivots(resPivots) + Env& env, + AletheNodeConverter& anc, + bool resPivots, + std::string* reasonForConversionFailure) + : EnvObj(env), + d_anc(anc), + d_resPivots(resPivots), + d_reasonForConversionFailure(reasonForConversionFailure) { NodeManager* nm = NodeManager::currentNM(); d_cl = nm->mkBoundVar("cl", nm->sExprType()); @@ -72,13 +78,14 @@ bool AletheProofPostprocessCallback::shouldUpdate(std::shared_ptr pn, const std::vector& fa, bool& continueUpdate) { - return pn->getRule() != ProofRule::ALETHE_RULE; + return d_reasonForConversionFailure->empty() + && pn->getRule() != ProofRule::ALETHE_RULE; } bool AletheProofPostprocessCallback::shouldUpdatePost( std::shared_ptr pn, const std::vector& fa) { - if (pn->getArguments().empty()) + if (!d_reasonForConversionFailure->empty() || pn->getArguments().empty()) { return false; } @@ -262,20 +269,14 @@ bool AletheProofPostprocessCallback::update(Node res, // Build vp1 std::vector negNode{d_cl}; - std::vector sanitized_args; for (const Node& arg : args) { negNode.push_back(arg.notNode()); // (not F1) ... (not Fn) - sanitized_args.push_back(d_anc.convert(arg)); } negNode.push_back(children[0]); // (cl (not F1) ... (not Fn) F) Node vp1 = nm->mkNode(Kind::SEXPR, negNode); - success &= addAletheStep(AletheRule::ANCHOR_SUBPROOF, - vp1, - vp1, - children, - sanitized_args, - *cdp); + success &= addAletheStep( + AletheRule::ANCHOR_SUBPROOF, vp1, vp1, children, args, *cdp); Node andNode, vp3; if (args.size() == 1) @@ -1439,6 +1440,7 @@ bool AletheProofPostprocessCallback::update(Node res, // negation, i.e., (not ...). case ProofRule::SKOLEMIZE: { + bool success = true; AletheRule skoRule; bool isExists; Node quant, skolemized; @@ -1460,9 +1462,15 @@ bool AletheProofPostprocessCallback::update(Node res, quantKind = Kind::FORALL; } // add rfl step for final replacement + Node conv = d_anc.maybeConvert(quant[1].eqNode(skolemized)); + if (conv.isNull()) + { + *d_reasonForConversionFailure = d_anc.d_error; + return false; + } Node premise = nm->mkNode( - Kind::SEXPR, d_cl, d_anc.convert(quant[1].eqNode(skolemized))); - addAletheStep(AletheRule::REFL, premise, premise, {}, {}, *cdp); + Kind::SEXPR, d_cl, conv); + success &= addAletheStep(AletheRule::REFL, premise, premise, {}, {}, *cdp); std::vector bVars{quant[0].begin(), quant[0].end()}; std::vector skoSubstitutions; for (size_t i = 0, size = quant[0].getNumChildren(); i < size; ++i) @@ -1489,17 +1497,18 @@ bool AletheProofPostprocessCallback::update(Node res, // add to the substitution skoSubstitutions.push_back(quant[0][i].eqNode(ithChoice)); } + Assert(!d_anc.convert(quant.eqNode(skolemized)).isNull()); Node conclusion = nm->mkNode( Kind::SEXPR, d_cl, d_anc.convert(quant.eqNode(skolemized))); // add the sko step - addAletheStep( + success &= addAletheStep( skoRule, conclusion, conclusion, {premise}, skoSubstitutions, *cdp); // add congruence step with NOT for the forall case if (!isExists) { Node newConclusion = nm->mkNode( Kind::SEXPR, d_cl, (quant.notNode()).eqNode(skolemized.notNode())); - addAletheStep(AletheRule::CONG, + success &= addAletheStep(AletheRule::CONG, newConclusion, newConclusion, {conclusion}, @@ -1511,17 +1520,18 @@ bool AletheProofPostprocessCallback::update(Node res, Node vp1 = nm->mkNode( Kind::SEXPR, {d_cl, conclusion[1].notNode(), children[0].notNode(), res}); - addAletheStep(AletheRule::EQUIV_POS2, vp1, vp1, {}, {}, *cdp); - addAletheStep( - AletheRule::RESOLUTION, - res, - nm->mkNode(Kind::SEXPR, d_cl, res), - {vp1, conclusion, children[0]}, - d_resPivots - ? std::vector{conclusion[1], d_false, children[0], d_false} - : std::vector(), - *cdp); - return true; + success &= addAletheStep(AletheRule::EQUIV_POS2, vp1, vp1, {}, {}, *cdp); + return success + && addAletheStep(AletheRule::RESOLUTION, + res, + nm->mkNode(Kind::SEXPR, d_cl, res), + {vp1, conclusion, children[0]}, + d_resPivots ? std::vector{conclusion[1], + d_false, + children[0], + d_false} + : std::vector(), + *cdp); } // ======== Bitvector // @@ -1534,7 +1544,15 @@ bool AletheProofPostprocessCallback::update(Node res, || k == Kind::BITVECTOR_SHL || k == Kind::BITVECTOR_LSHR || k == Kind::BITVECTOR_ASHR) { - Unreachable() << "Unsupported bit-blasting in Alethe of " << k << "\n"; + std::stringstream ss; + ss << "Bit-blasting of " << k << " is not supported in Alethe."; + *d_reasonForConversionFailure = ss.str(); + } + Node conv = d_anc.maybeConvert(res); + if (conv.isNull()) + { + *d_reasonForConversionFailure = d_anc.d_error; + return false; } // if the term being bitblasted is a variable or a nonbv term, then this // is a "bitblast var" step @@ -1543,7 +1561,7 @@ bool AletheProofPostprocessCallback::update(Node res, ? AletheRule::BV_BITBLAST_STEP_VAR : it->second, res, - nm->mkNode(Kind::SEXPR, d_cl, d_anc.convert(res)), + nm->mkNode(Kind::SEXPR, d_cl, conv), children, {}, *cdp); @@ -2037,8 +2055,7 @@ bool AletheProofPostprocessCallback::maybeReplacePremiseProof(Node premise, return false; } // If this resolution child is used as a singleton OR but the rule - // justifying it concludes a clause, then we are necessarily in this - // scenario: + // justifying it concludes a clause, then we are often in this scenario: // // (or t1 ... tn) // -------------- OR @@ -2052,55 +2069,108 @@ bool AletheProofPostprocessCallback::maybeReplacePremiseProof(Node premise, // a literal as well, and its node clashed with the conclusion of the // FACTORING/REORDERING step. // - // The solution is to *not* use FACTORING/REORDERING (which in Alethe - // operate on clauses) but generate a proof to obtain (via rewriting) the - // expected node (or t1' ... tn') from the original node (or t1 ... tn). + // When this is happening at one level, as in the example above, a solution is + // to *not* use FACTORING/REORDERING (which in Alethe operate on clauses) but + // generate a proof to obtain (via rewriting) the expected node (or t1' ... + // tn') from the original node (or t1 ... tn). + // + // However, this may have happened in a complex proof in which we'd have no + // easy way to get access to (or t1 ... tn), in which case we delive (cl (or + // t1' ... tn')) by introducing n or_neg steps, similarly to the translation + // of EQ_RESOLVE. NodeManager* nm = NodeManager::currentNM(); Trace("alethe-proof") << "\n"; CVC5_UNUSED AletheRule premiseProofRule = getAletheRule(premisePf->getArguments()[0]); CVC5_UNUSED AletheRule premiseChildProofRule = getAletheRule(premisePf->getChildren()[0]->getArguments()[0]); - Assert((premiseProofRule == AletheRule::CONTRACTION + if ((premiseProofRule == AletheRule::CONTRACTION || premiseProofRule == AletheRule::REORDERING) - && premiseChildProofRule == AletheRule::OR); - // get great grand child - std::shared_ptr premiseChildPf = - premisePf->getChildren()[0]->getChildren()[0]; - Node premiseChildConclusion = premiseChildPf->getResult(); - // Note that we need to add this proof node explicitly to cdp because it does - // not have a step for premiseChildConclusion. Rather it is only present in - // cdp as a descendant of premisePf (which is in cdp), so if premisePf is to - // be lost, then so will premiseChildPf. By adding premiseChildPf explicitly, - // it can be retrieved to justify premiseChildConclusion when requested. - cdp->addProof(premiseChildPf); - // equate it to what we expect, use equiv elim and resolution to - // obtain a proof the expected - Node equiv = premiseChildConclusion.eqNode(premise); - addAletheStep(AletheRule::ALL_SIMPLIFY, - equiv, - nm->mkNode(Kind::SEXPR, d_cl, equiv), - {}, - {}, - *cdp); - Node equivElim = nm->mkNode( - Kind::SEXPR, - {d_cl, equiv.notNode(), premiseChildConclusion.notNode(), premise}); - addAletheStep(AletheRule::EQUIV_POS2, equivElim, equivElim, {}, {}, *cdp); + && premiseChildProofRule == AletheRule::OR) + { + // get great grand child + std::shared_ptr premiseChildPf = + premisePf->getChildren()[0]->getChildren()[0]; + Node premiseChildConclusion = premiseChildPf->getResult(); + // Note that we need to add this proof node explicitly to cdp because it + // does not have a step for premiseChildConclusion. Rather it is only + // present in cdp as a descendant of premisePf (which is in cdp), so if + // premisePf is to be lost, then so will premiseChildPf. By adding + // premiseChildPf explicitly, it can be retrieved to justify + // premiseChildConclusion when requested. + cdp->addProof(premiseChildPf); + // equate it to what we expect, use equiv elim and resolution to + // obtain a proof the expected + Node equiv = premiseChildConclusion.eqNode(premise); + bool success = addAletheStep(AletheRule::ALL_SIMPLIFY, + equiv, + nm->mkNode(Kind::SEXPR, d_cl, equiv), + {}, + {}, + *cdp); + Node equivElim = nm->mkNode( + Kind::SEXPR, + {d_cl, equiv.notNode(), premiseChildConclusion.notNode(), premise}); + success &= addAletheStep( + AletheRule::EQUIV_POS2, equivElim, equivElim, {}, {}, *cdp); + Node newPremise = nm->mkNode(Kind::SEXPR, d_cl, premise); + Trace("alethe-proof") << "Reverted handling as a clause for converting " + << premiseChildConclusion << " into " << premise + << std::endl; + return success + && addAletheStep(AletheRule::RESOLUTION, + newPremise, + newPremise, + {equivElim, equiv, premiseChildConclusion}, + d_resPivots + ? std::vector{equiv, + d_false, + premiseChildConclusion, + d_false} + : std::vector(), + *cdp); + } + // Derive (cl (or t1' ... tn')) from (cl t1' ... tn') (i.e., the premise) with a subproof + // + // ----------------------- ... --------------------- OR_NEG + // premise (cl premise, (not t1')) ... (cl premise, (not tn')) + // ---------------------------- RESOLUTION + // (cl premise ... premise) + // ---------------------------- CONTRACTION + // (cl premise) + std::vector resPremises{premise}; + std::vector resArgs; + std::vector contractionPremiseChildren{d_cl}; + bool success = true; + for (const Node& n : premise) + { + Node nNeg = n.notNode(); + resPremises.push_back(nm->mkNode(Kind::SEXPR, d_cl, premise, nNeg)); + success &= addAletheStep(AletheRule::OR_NEG, + resPremises.back(), + resPremises.back(), + {}, + {}, + *cdp); + resArgs.push_back(nNeg); + resArgs.push_back(d_true); + contractionPremiseChildren.push_back(premise); + } + Node contractionPremise = nm->mkNode(Kind::SEXPR, contractionPremiseChildren); + success &= addAletheStep(AletheRule::RESOLUTION, + contractionPremise, + contractionPremise, + resPremises, + d_resPivots ? resArgs : std::vector(), + *cdp); Node newPremise = nm->mkNode(Kind::SEXPR, d_cl, premise); - addAletheStep( - AletheRule::RESOLUTION, - newPremise, - newPremise, - {equivElim, equiv, premiseChildConclusion}, - d_resPivots - ? std::vector{equiv, d_false, premiseChildConclusion, d_false} - : std::vector(), - *cdp); - Trace("alethe-proof") << "Reverted handling as a clause for converting " - << premiseChildConclusion << " into " << premise - << std::endl; - return true; + return success + && addAletheStep(AletheRule::CONTRACTION, + newPremise, + newPremise, + {contractionPremise}, + {}, + *cdp); } // Adds an OR rule to the premises of a step if the premise is not a clause and @@ -2120,6 +2190,7 @@ bool AletheProofPostprocessCallback::updatePost( AletheRule rule = getAletheRule(args[0]); Trace("alethe-proof") << "...Alethe post-update " << rule << " / " << res << " / args: " << args << std::endl; + bool success = true; switch (rule) { // In the case of a resolution rule the rule might originally have been a @@ -2175,7 +2246,7 @@ bool AletheProofPostprocessCallback::updatePost( childConclusion[1].end()); } Node newConclusion = nm->mkNode(Kind::SEXPR, subterms); - addAletheStep(AletheRule::OR, + success &= addAletheStep(AletheRule::OR, newConclusion, newConclusion, {children[0]}, @@ -2214,6 +2285,7 @@ bool AletheProofPostprocessCallback::updatePost( // the arguments will have been converted to witness form already, so // we also check whether after conversion the child is still not the // same (in the case where we'd need to have them different) + Assert(!d_anc.convert(children[i]).isNull()); if (args[polIdx] == d_false && args[pivIdx] == d_anc.convert(children[i])) { @@ -2242,7 +2314,7 @@ bool AletheProofPostprocessCallback::updatePost( childConclusion[1].end()); } Node conclusion = nm->mkNode(Kind::SEXPR, lits); - addAletheStep(AletheRule::OR, + success &= addAletheStep(AletheRule::OR, conclusion, conclusion, {children[i]}, @@ -2276,7 +2348,7 @@ bool AletheProofPostprocessCallback::updatePost( d_resPivots ? args : std::vector{args.begin(), args.begin() + 3}); - return true; + return success; } Trace("alethe-proof") << "... no update\n"; return false; @@ -2331,14 +2403,14 @@ bool AletheProofPostprocessCallback::updatePost( childConclusion[1].end()); } Node newChild = nm->mkNode(Kind::SEXPR, subterms); - addAletheStep( + success &= addAletheStep( AletheRule::OR, newChild, newChild, {children[0]}, {}, *cdp); Trace("alethe-proof") << "Added OR step in finalizer to child " << childConclusion << " / " << newChild << std::endl; // update res step cdp->addStep(res, ProofRule::ALETHE_RULE, {newChild}, args); - return true; + return success; } Trace("alethe-proof") << "... no update\n"; return false; @@ -2380,6 +2452,7 @@ bool AletheProofPostprocessCallback::finalStep(Node res, const std::vector& args, CDProof* cdp) { + bool success = true; NodeManager* nm = NodeManager::currentNM(); std::shared_ptr childPf = cdp->getProofFor(children[0]); @@ -2394,8 +2467,8 @@ bool AletheProofPostprocessCallback::finalStep(Node res, nm->mkNode(Kind::SEXPR, d_cl, d_false.notNode()); // (cl (not false)) Node newChild = nm->mkNode(Kind::SEXPR, d_cl); // (cl) - addAletheStep(AletheRule::FALSE, notFalse, notFalse, {}, {}, *cdp); - addAletheStep( + success &= addAletheStep(AletheRule::FALSE, notFalse, notFalse, {}, {}, *cdp); + success &= addAletheStep( AletheRule::RESOLUTION, newChild, newChild, @@ -2407,15 +2480,27 @@ bool AletheProofPostprocessCallback::finalStep(Node res, // Sanitize original assumptions and create a double scope to hold them, where // the first scope is empty. This is needed because of the expected form a - // proof node to be printed + // proof node to be printed. Note that this std::vector sanitizedArgs; - std::transform(args.begin(), - args.end(), - std::back_inserter(sanitizedArgs), - [this](Node a) { return d_anc.convert(a, false); }); + for (const Node& a : args) + { + Node conv = d_anc.maybeConvert(a); + if (conv.isNull()) + { + *d_reasonForConversionFailure = d_anc.d_error; + success = false; + break; + } + // avoid repeated assumptions + if (std::find(sanitizedArgs.begin(), sanitizedArgs.end(), conv) == sanitizedArgs.end()) + { + d_anc.d_convToOriginalAssumption[conv] = a; + sanitizedArgs.push_back(conv); + } + } Node placeHolder = nm->mkNode(Kind::SEXPR, res); cdp->addStep(placeHolder, ProofRule::SCOPE, children, sanitizedArgs); - return cdp->addStep(res, ProofRule::SCOPE, {placeHolder}, {}); + return success && cdp->addStep(res, ProofRule::SCOPE, {placeHolder}, {}); } bool AletheProofPostprocessCallback::addAletheStep( @@ -2429,10 +2514,22 @@ bool AletheProofPostprocessCallback::addAletheStep( std::vector newArgs{NodeManager::currentNM()->mkConstInt( Rational(static_cast(rule)))}; newArgs.push_back(res); - newArgs.push_back(d_anc.convert(conclusion)); + Node conv = d_anc.maybeConvert(conclusion); + if (conv.isNull()) + { + *d_reasonForConversionFailure = d_anc.d_error; + return false; + } + newArgs.push_back(conv); for (const Node& arg : args) { - newArgs.push_back(d_anc.convert(arg)); + conv = d_anc.maybeConvert(arg); + if (conv.isNull()) + { + *d_reasonForConversionFailure = d_anc.d_error; + return false; + } + newArgs.push_back(conv); } Trace("alethe-proof") << "... add alethe step " << res << " / " << conclusion << " " << rule << " " << children << " / " << newArgs @@ -2456,13 +2553,14 @@ bool AletheProofPostprocessCallback::addAletheStepFromOr( AletheProofPostprocess::AletheProofPostprocess(Env& env, AletheNodeConverter& anc, bool resPivots) - : EnvObj(env), d_cb(env, anc, resPivots) + : EnvObj(env), d_cb(env, anc, resPivots, &d_reasonForConversionFailure) { } AletheProofPostprocess::~AletheProofPostprocess() {} -void AletheProofPostprocess::process(std::shared_ptr pf) +bool AletheProofPostprocess::process(std::shared_ptr pf, + std::string& reasonForConversionFailure) { // first two nodes are scopes for definitions and other assumptions. We // process only the internal proof node. And we merge these two scopes @@ -2475,6 +2573,12 @@ void AletheProofPostprocess::process(std::shared_ptr pf) ProofNodeUpdater updater(d_env, d_cb, false, false); updater.process(internalProof); + if (!d_reasonForConversionFailure.empty()) + { + reasonForConversionFailure = d_reasonForConversionFailure; + return false; + } + // In the Alethe proof format the final step has to be (cl). However, after // the translation it might be (cl false). In that case additional steps are // required. @@ -2500,6 +2604,7 @@ void AletheProofPostprocess::process(std::shared_ptr pf) d_env.getProofNodeManager()->updateNode(pf.get(), npn.get()); Trace("pf-process-debug") << "...update node finished." << std::endl; } + return true; } } // namespace proof diff --git a/src/proof/alethe/alethe_post_processor.h b/src/proof/alethe/alethe_post_processor.h index 3e45845ace3..66c582c3959 100644 --- a/src/proof/alethe/alethe_post_processor.h +++ b/src/proof/alethe/alethe_post_processor.h @@ -34,7 +34,8 @@ class AletheProofPostprocessCallback : protected EnvObj, public: AletheProofPostprocessCallback(Env& env, AletheNodeConverter& anc, - bool resPivots); + bool resPivots, + std::string* reasonForConversionFailure); ~AletheProofPostprocessCallback() {} /** Should proof pn be updated? Only if its top-level proof rule is not an * Alethe proof rule. @@ -151,6 +152,8 @@ class AletheProofPostprocessCallback : protected EnvObj, /** Nodes corresponding to the Boolean values. */ Node d_true; Node d_false; + + std::string* d_reasonForConversionFailure; }; /** @@ -162,12 +165,24 @@ class AletheProofPostprocess : protected EnvObj public: AletheProofPostprocess(Env& env, AletheNodeConverter& anc, bool resPivots); ~AletheProofPostprocess(); - /** post-process */ - void process(std::shared_ptr pf); + /** post-process + * + * Converts pf to the Alethe proof calculus, if possible, in which case it + * returns true. Otherwise, returns false. The conversion may fail if the + * proof contains unsupported elements in the Alethe proof calculus. Examples + * of such elements are datatypes, uncategorized Skolems etc. + * + * The argument reasonForConversionFailure stores the reason for failure, if + * any. + */ + bool process(std::shared_ptr pf, + std::string& reasonForConversionFailure); private: /** The post process callback */ AletheProofPostprocessCallback d_cb; + + std::string d_reasonForConversionFailure; }; } // namespace proof diff --git a/src/proof/alethe/alethe_printer.cpp b/src/proof/alethe/alethe_printer.cpp index b350b22baa5..9b3bffa151d 100644 --- a/src/proof/alethe/alethe_printer.cpp +++ b/src/proof/alethe/alethe_printer.cpp @@ -21,6 +21,7 @@ #include "options/printer_options.h" #include "proof/alethe/alethe_proof_rule.h" +#include "util/smt2_quote_string.h" namespace cvc5::internal { @@ -138,11 +139,18 @@ void AletheProofPrinter::print( // Print assumptions and add them to the list but do not print anchor. for (size_t i = 0, size = args.size(); i < size; i++) { - auto it = assertionNames.find(args[i]); + // seach name with original assumption rather than its conversion + Assert(d_anc.d_convToOriginalAssumption.find(args[i]) + != d_anc.d_convToOriginalAssumption.end()); + Node original = d_anc.d_convToOriginalAssumption[args[i]]; + auto it = assertionNames.find(original); if (it != assertionNames.end()) { - out << "(assume " << it->second << " "; - assumptions[args[i]] = it->second; + // Since names can be strings that were originally quoted, we must see if + // the quotes need to be added back. + std::string quotedName = quoteSymbol(it->second); + out << "(assume " << quotedName << " "; + assumptions[args[i]] = quotedName; } else { // assumptions are always being declared @@ -175,6 +183,7 @@ std::string AletheProofPrinter::printInternal( if (pfn->getRule() == ProofRule::ASSUME) { Node res = d_anc.convert(pfn->getResult()); + Assert(!res.isNull()); Trace("alethe-printer") << "... reached assumption " << res << std::endl; auto it = assumptions.find(res); Assert(it != assumptions.end()) << "Assumption has not been printed yet! " diff --git a/src/proof/alethe/alethe_proof_rule.cpp b/src/proof/alethe/alethe_proof_rule.cpp index 24cbf70dacf..3f6bc801f8a 100644 --- a/src/proof/alethe/alethe_proof_rule.cpp +++ b/src/proof/alethe/alethe_proof_rule.cpp @@ -144,7 +144,8 @@ const char* aletheRuleToString(AletheRule id) return "bv_bitblast_step_bvequal"; case AletheRule::BV_BITBLAST_STEP_CONCAT: return "bv_bitblast_step_concat"; case AletheRule::BV_BITBLAST_STEP_CONST: return "bv_bitblast_step_const"; - case AletheRule::BV_BITBLAST_STEP_SIGN_EXTEND: return "bv_bitblast_step_sign_extend"; + case AletheRule::BV_BITBLAST_STEP_SIGN_EXTEND: + return "bv_bitblast_step_sign_extend"; //================================================= Hole case AletheRule::HOLE: return "hole"; //================================================= Undefined rule diff --git a/src/proof/proof_checker.cpp b/src/proof/proof_checker.cpp index e55a19272c4..6f42a20de22 100644 --- a/src/proof/proof_checker.cpp +++ b/src/proof/proof_checker.cpp @@ -141,6 +141,11 @@ Node ProofChecker::checkDebug(ProofRule id, return res; } +void ProofChecker::setProofCheckMode(options::ProofCheckMode pcMode) +{ + d_pcMode = pcMode; +} + Node ProofChecker::checkInternal(ProofRule id, const std::vector& cchildren, const std::vector& args, diff --git a/src/proof/proof_checker.h b/src/proof/proof_checker.h index 04fd4230d2c..1124d81df38 100644 --- a/src/proof/proof_checker.h +++ b/src/proof/proof_checker.h @@ -125,6 +125,9 @@ class ProofChecker */ bool isPedanticFailure(ProofRule id, std::ostream* out) const; + /** Assigns argument pcMode to d_pcMode. */ + void setProofCheckMode(options::ProofCheckMode pcMode); + private: /** statistics class */ ProofCheckerStatistics d_stats; diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index f13e8bf3ad7..1143b65b277 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -17,6 +17,7 @@ #include "options/base_options.h" #include "options/main_options.h" +#include "options/proof_options.h" #include "options/smt_options.h" #include "proof/alethe/alethe_node_converter.h" #include "proof/alethe/alethe_post_processor.h" @@ -269,22 +270,39 @@ void PfManager::printProof(std::ostream& out, else if (mode == options::ProofFormatMode::ALETHE_ALF) { // convert using Alethe post-processor + std::string reasonForConversionFailure; proof::AletheNodeConverter anc; proof::AletheProofPostprocess vpfpp( d_env, anc, options().proof.proofAletheResPivots); - vpfpp.process(fp); - // print using ALF printer - proof::AlfPrinter alfp(d_env, anc); - alfp.print(out, fp); + if (vpfpp.process(fp, reasonForConversionFailure)) + { + // print using ALF printer + proof::AlfPrinter alfp(d_env, anc); + alfp.print(out, fp); + } + else + { + out << "(error \"" << reasonForConversionFailure << "\")"; + } } else if (mode == options::ProofFormatMode::ALETHE) { + options::ProofCheckMode oldMode =options().proof.proofCheck; + d_pnm->getChecker()->setProofCheckMode(options::ProofCheckMode::NONE); + std::string reasonForConversionFailure; proof::AletheNodeConverter anc; proof::AletheProofPostprocess vpfpp( d_env, anc, options().proof.proofAletheResPivots); - vpfpp.process(fp); - proof::AletheProofPrinter vpp(d_env, anc); - vpp.print(out, fp, assertionNames); + if (vpfpp.process(fp, reasonForConversionFailure)) + { + proof::AletheProofPrinter vpp(d_env, anc); + vpp.print(out, fp, assertionNames); + } + else + { + out << "(error " << reasonForConversionFailure << ")"; + } + d_pnm->getChecker()->setProofCheckMode(oldMode); } else if (mode == options::ProofFormatMode::LFSC) { From 7466dce03bac4aa6a74b60298ef3cb907dec37a5 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 29 Feb 2024 16:24:05 -0600 Subject: [PATCH 5/5] Weaken rewrite db failure --- src/rewriter/rewrite_db_proof_cons.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/rewriter/rewrite_db_proof_cons.cpp b/src/rewriter/rewrite_db_proof_cons.cpp index 445e09d15f9..75976dfb49c 100644 --- a/src/rewriter/rewrite_db_proof_cons.cpp +++ b/src/rewriter/rewrite_db_proof_cons.cpp @@ -74,8 +74,8 @@ bool RewriteDbProofCons::prove(CDProof* cdp, Trace("rpc") << "...success (basic)" << std::endl; return true; } - // if there are quantifiers, fail immediately - if (expr::hasBoundVar(a) || expr::hasBoundVar(b)) + // if a is a quantified formula, fail immediately + if (a.isClosure()) { Trace("rpc") << "...fail (out of scope)" << std::endl; return false;