diff --git a/NEWS.md b/NEWS.md index 3ea6df3df88..c73e6e19c82 100644 --- a/NEWS.md +++ b/NEWS.md @@ -1,19 +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 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/CMakeLists.txt b/src/CMakeLists.txt index 51e48d51955..c0394826f4c 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -252,6 +252,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/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 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 67943814a94..517fc7b0e69 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -976,6 +976,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/bags/bag_solver.cpp b/src/theory/bags/bag_solver.cpp index fa0d991dddb..02c06d97b21 100644 --- a/src/theory/bags/bag_solver.cpp +++ b/src/theory/bags/bag_solver.cpp @@ -75,7 +75,7 @@ void BagSolver::checkBasicOperations() case Kind::BAG_INTER_MIN: checkIntersectionMin(n); break; case Kind::BAG_DIFFERENCE_SUBTRACT: checkDifferenceSubtract(n); break; case Kind::BAG_DIFFERENCE_REMOVE: checkDifferenceRemove(n); break; - case Kind::BAG_DUPLICATE_REMOVAL: checkDuplicateRemoval(n); break; + case Kind::BAG_SETOF: checkSetof(n); break; case Kind::BAG_FILTER: checkFilter(n); break; case Kind::TABLE_PRODUCT: checkProduct(n); break; case Kind::TABLE_JOIN: checkJoin(n); break; @@ -258,9 +258,9 @@ void BagSolver::checkDifferenceRemove(const Node& n) } } -void BagSolver::checkDuplicateRemoval(Node n) +void BagSolver::checkSetof(Node n) { - Assert(n.getKind() == Kind::BAG_DUPLICATE_REMOVAL); + Assert(n.getKind() == Kind::BAG_SETOF); set 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 1225ac70b4f..1770327a712 100644 --- a/src/theory/bags/theory_bags_type_rules.cpp +++ b/src/theory/bags/theory_bags_type_rules.cpp @@ -193,16 +193,16 @@ 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].getTypeOrNull(); if (check) { @@ -211,7 +211,7 @@ TypeNode DuplicateRemovalTypeRule::computeType(NodeManager* nodeManager, if (errOut) { (*errOut) - << "Applying BAG_DUPLICATE_REMOVAL on a non-bag argument in term " + << "Applying BAG_SETOF on a non-bag argument in term " << n; } return TypeNode::null(); @@ -266,32 +266,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].getTypeOrNull(); - if (check) - { - if (!bagType.isBag()) - { - if (errOut) - { - (*errOut) - << "BAG_IS_SINGLETON operator expects a bag, a non-bag is found"; - } - return TypeNode::null(); - } - } - return nodeManager->booleanType(); -} - TypeNode EmptyBagTypeRule::preComputeType(NodeManager* nm, TNode n) { return TypeNode::null(); @@ -356,60 +330,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].getTypeOrNull(); - if (check) - { - if (!setType.isSet()) - { - if (errOut) - { - (*errOut) << "bag.from_set operator expects a set, a non-set is found"; - } - return TypeNode::null(); - } - } - 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].getTypeOrNull(); - if (check) - { - if (!bagType.isBag()) - { - if (errOut) - { - (*errOut) << "bag.to_set operator expects a bag, a non-bag is found"; - } - return TypeNode::null(); - } - } - 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/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 c3c15e262da..3cbaa779092 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 @@ -2145,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/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) 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);