-/********************* */
-/*! \file theory_sets.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Andrew Reynolds, Kshitij Bansal, Andres Noetzli
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 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.\endverbatim
- **
- ** \brief Sets theory.
- **
- ** Sets theory.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ * Andrew Reynolds, Kshitij Bansal, Andres Noetzli
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * Sets theory.
+ */
#include "theory/sets/theory_sets.h"
#include "theory/sets/theory_sets_private.h"
#include "theory/sets/theory_sets_rewriter.h"
#include "theory/theory_model.h"
+#include "theory/trust_substitutions.h"
-using namespace CVC4::kind;
+using namespace cvc5::kind;
-namespace CVC4 {
+namespace cvc5 {
namespace theory {
namespace sets {
-TheorySets::TheorySets(context::Context* c,
- context::UserContext* u,
- OutputChannel& out,
- Valuation valuation,
- const LogicInfo& logicInfo,
- ProofNodeManager* pnm)
- : Theory(THEORY_SETS, c, u, out, valuation, logicInfo, pnm),
- d_skCache(),
- d_state(c, u, valuation, d_skCache),
- d_im(*this, d_state, pnm),
- d_internal(new TheorySetsPrivate(*this, d_state, d_im, d_skCache)),
+TheorySets::TheorySets(Env& env, OutputChannel& out, Valuation valuation)
+ : Theory(THEORY_SETS, env, out, valuation),
+ d_skCache(env.getRewriter()),
+ d_state(env, valuation, d_skCache),
+ d_im(env, *this, d_state),
+ d_internal(
+ new TheorySetsPrivate(env, *this, d_state, d_im, d_skCache, d_pnm)),
d_notify(*d_internal.get(), d_im)
{
// use the official theory state and inference manager objects
return d_internal->getTheoryRewriter();
}
+ProofRuleChecker* TheorySets::getProofChecker() { return nullptr; }
+
bool TheorySets::needsEqualityEngine(EeSetupInfo& esi)
{
esi.d_notify = &d_notify;
esi.d_name = "theory::sets::ee";
+ esi.d_notifyNewClass = true;
+ esi.d_notifyMerge = true;
+ esi.d_notifyDisequal = true;
return true;
}
d_valuation.setUnevaluatedKind(COMPREHENSION);
// choice is used to eliminate witness
d_valuation.setUnevaluatedKind(WITNESS);
+ // Universe set is not evaluated. This is moreover important for ensuring that
+ // we do not eliminate terms whose value involves the universe set.
+ d_valuation.setUnevaluatedKind(UNIVERSE_SET);
// functions we are doing congruence over
d_equalityEngine->addFunctionKind(SINGLETON);
d_internal->preRegisterTerm(node);
}
-TrustNode TheorySets::expandDefinition(Node n)
+TrustNode TheorySets::ppRewrite(TNode n, std::vector<SkolemLemma>& lems)
{
Kind nk = n.getKind();
if (nk == UNIVERSE_SET || nk == COMPLEMENT || nk == JOIN_IMAGE
|| nk == COMPREHENSION)
{
- if (!options::setsExt())
+ if (!options().sets.setsExt)
{
std::stringstream ss;
ss << "Extended set operators are not supported in default mode, try "
if (nk == COMPREHENSION)
{
// set comprehension is an implicit quantifier, require it in the logic
- if (!getLogicInfo().isQuantified())
+ if (!logicInfo().isQuantified())
{
std::stringstream ss;
ss << "Set comprehensions require quantifiers in the background logic.";
throw LogicException(ss.str());
}
}
- return d_internal->expandDefinition(n);
+ return d_internal->ppRewrite(n, lems);
}
-Theory::PPAssertStatus TheorySets::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
+Theory::PPAssertStatus TheorySets::ppAssert(
+ TrustNode tin, TrustSubstitutionMap& outSubstitutions)
+{
+ TNode in = tin.getNode();
Debug("sets-proc") << "ppAssert : " << in << std::endl;
Theory::PPAssertStatus status = Theory::PP_ASSERT_STATUS_UNSOLVED;
// may appear when this option is enabled, and solving for such a set
// impacts the semantics of universe set, see
// regress0/sets/pre-proc-univ.smt2
- if (!in[0].getType().isSet() || !options::setsExt())
+ if (!in[0].getType().isSet() || !options().sets.setsExt)
{
- outSubstitutions.addSubstitution(in[0], in[1]);
+ outSubstitutions.addSubstitutionSolved(in[0], in[1], tin);
status = Theory::PP_ASSERT_STATUS_SOLVED;
}
}
else if (in[1].isVar() && isLegalElimination(in[1], in[0]))
{
- if (!in[0].getType().isSet() || !options::setsExt())
+ if (!in[0].getType().isSet() || !options().sets.setsExt)
{
- outSubstitutions.addSubstitution(in[1], in[0]);
+ outSubstitutions.addSubstitutionSolved(in[1], in[0], tin);
status = Theory::PP_ASSERT_STATUS_SOLVED;
}
}
d_theory.eqNotifyDisequal(t1, t2, reason);
}
-}/* CVC4::theory::sets namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+} // namespace sets
+} // namespace theory
+} // namespace cvc5
projects / cvc5.git / blobdiff