summaryrefslogtreecommitdiff
path: root/src/theory/bags
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/bags')
-rw-r--r--src/theory/bags/inference_manager.cpp35
-rw-r--r--src/theory/bags/inference_manager.h57
-rw-r--r--src/theory/bags/kinds79
-rw-r--r--src/theory/bags/normal_form.cpp27
-rw-r--r--src/theory/bags/normal_form.h44
-rw-r--r--src/theory/bags/solver_state.cpp35
-rw-r--r--src/theory/bags/solver_state.h44
-rw-r--r--src/theory/bags/term_registry.cpp45
-rw-r--r--src/theory/bags/term_registry.h63
-rw-r--r--src/theory/bags/theory_bags.cpp139
-rw-r--r--src/theory/bags/theory_bags.h110
-rw-r--r--src/theory/bags/theory_bags_rewriter.cpp37
-rw-r--r--src/theory/bags/theory_bags_rewriter.h38
-rw-r--r--src/theory/bags/theory_bags_type_enumerator.cpp85
-rw-r--r--src/theory/bags/theory_bags_type_enumerator.h91
-rw-r--r--src/theory/bags/theory_bags_type_rules.h255
16 files changed, 1184 insertions, 0 deletions
diff --git a/src/theory/bags/inference_manager.cpp b/src/theory/bags/inference_manager.cpp
new file mode 100644
index 000000000..4d18ad926
--- /dev/null
+++ b/src/theory/bags/inference_manager.cpp
@@ -0,0 +1,35 @@
+/********************* */
+/*! \file inference_manager.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Mudathir Mohamed
+ ** 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 Implementation of the inference manager for the theory of bags
+ **/
+
+#include "theory/bags/inference_manager.h"
+
+using namespace std;
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace bags {
+
+InferenceManager::InferenceManager(Theory& t,
+ SolverState& s,
+ ProofNodeManager* pnm)
+ : InferenceManagerBuffered(t, s, pnm), d_state(s)
+{
+ d_true = NodeManager::currentNM()->mkConst(true);
+ d_false = NodeManager::currentNM()->mkConst(false);
+}
+
+} // namespace bags
+} // namespace theory
+} // namespace CVC4
diff --git a/src/theory/bags/inference_manager.h b/src/theory/bags/inference_manager.h
new file mode 100644
index 000000000..4b4edbaef
--- /dev/null
+++ b/src/theory/bags/inference_manager.h
@@ -0,0 +1,57 @@
+/********************* */
+/*! \file inference_manager.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Mudathir Mohamed
+ ** 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 The inference manager for the theory of bags.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__BAGS__INFERENCE_MANAGER_H
+#define CVC4__THEORY__BAGS__INFERENCE_MANAGER_H
+
+#include "theory/bags/solver_state.h"
+#include "theory/inference_manager_buffered.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bags {
+
+/** Inference manager
+ *
+ * This class manages inferences produced by the theory of bags. It manages
+ * whether inferences are processed as external lemmas on the output channel
+ * of theory of bags or internally as literals asserted to the equality engine
+ * of theory of bags. The latter literals are referred to as "facts".
+ */
+class InferenceManager : public InferenceManagerBuffered
+{
+ typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+
+ public:
+ InferenceManager(Theory& t, SolverState& s, ProofNodeManager* pnm);
+
+ private:
+ /** constants */
+ Node d_true;
+ Node d_false;
+ /**
+ * Reference to the state object for the theory of bags. We store the
+ * (derived) state here, since it has additional methods required in this
+ * class.
+ */
+ SolverState& d_state;
+};
+
+} // namespace bags
+} // namespace theory
+} // namespace CVC4
+
+#endif /* CVC4__THEORY__BAGS__INFERENCE_MANAGER_H */
diff --git a/src/theory/bags/kinds b/src/theory/bags/kinds
new file mode 100644
index 000000000..8093448a0
--- /dev/null
+++ b/src/theory/bags/kinds
@@ -0,0 +1,79 @@
+# kinds -*- sh -*-
+#
+# For documentation on this file format, please refer to
+# src/theory/builtin/kinds.
+#
+
+theory THEORY_BAGS \
+ ::CVC4::theory::bags::TheoryBags \
+ "theory/bags/theory_bags.h"
+typechecker "theory/bags/theory_bags_type_rules.h"
+rewriter ::CVC4::theory::bags::TheoryBagsRewriter \
+ "theory/bags/theory_bags_rewriter.h"
+
+properties parametric
+properties check propagate presolve
+
+# constants
+constant EMPTYBAG \
+ ::CVC4::EmptyBag \
+ ::CVC4::EmptyBagHashFunction \
+ "expr/emptybag.h" \
+ "the empty bag constant; payload is an instance of the CVC4::EmptyBag class"
+
+# the type
+operator BAG_TYPE 1 "bag type, takes as parameter the type of the elements"
+cardinality BAG_TYPE \
+ "::CVC4::theory::bags::BagsProperties::computeCardinality(%TYPE%)" \
+ "theory/bags/theory_bags_type_rules.h"
+well-founded BAG_TYPE \
+ "::CVC4::theory::bags::BagsProperties::isWellFounded(%TYPE%)" \
+ "::CVC4::theory::bags::BagsProperties::mkGroundTerm(%TYPE%)" \
+ "theory/bags/theory_bags_type_rules.h"
+enumerator BAG_TYPE \
+ "::CVC4::theory::bags::BagEnumerator" \
+ "theory/bags/theory_bags_type_enumerator.h"
+
+# operators
+operator UNION_MAX 2 "union for bags (max)"
+operator UNION_DISJOINT 2 "disjoint union for bags (sum)"
+operator INTERSECTION_MIN 2 "bag intersection (min)"
+
+# {("a", 2), ("b", 3)} \ {("a", 1)} = {("a", 1), ("b", 3)}
+operator DIFFERENCE_SUBTRACT 2 "bag difference1 (subtracts multiplicities)"
+
+# {("a", 2), ("b", 3)} \\ {("a", 1)} = {("b", 3)}
+operator DIFFERENCE_REMOVE 2 "bag difference remove (removes shared elements)"
+
+operator BAG_IS_INCLUDED 2 "inclusion predicate for bags (less than or equal multiplicities)"
+operator BAG_COUNT 2 "multiplicity of an element in a bag"
+operator MK_BAG 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_CARD 1 "bag cardinality operator"
+
+# 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.
+# If the bag is empty, then (choose A) is an arbitrary value.
+# If the bag has cardinality > 1, then (choose A) will deterministically return an element in A.
+operator BAG_CHOOSE 1 "return an element in the bag given as a parameter"
+
+typerule UNION_MAX ::CVC4::theory::bags::BinaryOperatorTypeRule
+typerule UNION_DISJOINT ::CVC4::theory::bags::BinaryOperatorTypeRule
+typerule INTERSECTION_MIN ::CVC4::theory::bags::BinaryOperatorTypeRule
+typerule DIFFERENCE_SUBTRACT ::CVC4::theory::bags::BinaryOperatorTypeRule
+typerule DIFFERENCE_REMOVE ::CVC4::theory::bags::BinaryOperatorTypeRule
+typerule BAG_IS_INCLUDED ::CVC4::theory::bags::IsIncludedTypeRule
+typerule BAG_COUNT ::CVC4::theory::bags::CountTypeRule
+typerule MK_BAG ::CVC4::theory::bags::MkBagTypeRule
+typerule EMPTYBAG ::CVC4::theory::bags::EmptyBagTypeRule
+typerule BAG_CARD ::CVC4::theory::bags::CardTypeRule
+typerule BAG_CHOOSE ::CVC4::theory::bags::ChooseTypeRule
+typerule BAG_IS_SINGLETON ::CVC4::theory::bags::IsSingletonTypeRule
+
+construle UNION_DISJOINT ::CVC4::theory::bags::BinaryOperatorTypeRule
+construle MK_BAG ::CVC4::theory::bags::MkBagTypeRule
+
+endtheory \ No newline at end of file
diff --git a/src/theory/bags/normal_form.cpp b/src/theory/bags/normal_form.cpp
new file mode 100644
index 000000000..d9248615b
--- /dev/null
+++ b/src/theory/bags/normal_form.cpp
@@ -0,0 +1,27 @@
+/************************* */
+/*! \file normal_form.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Mudathir Mohamed
+ ** 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
+ **/
+
+#include "normal_form.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bags {
+
+bool NormalForm::checkNormalConstant(TNode n)
+{
+ // TODO(projects#223): complete this function
+ return false;
+}
+
+} // namespace bags
+} // namespace theory
+} // namespace CVC4 \ No newline at end of file
diff --git a/src/theory/bags/normal_form.h b/src/theory/bags/normal_form.h
new file mode 100644
index 000000000..73fd8dba8
--- /dev/null
+++ b/src/theory/bags/normal_form.h
@@ -0,0 +1,44 @@
+/********************* */
+/*! \file normal_form.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Mudathir Mohamed
+ ** 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 Normal form for bag constants.
+ **/
+
+#include "cvc4_private.h"
+#include <expr/node.h>
+
+#ifndef CVC4__THEORY__BAGS__NORMAL_FORM_H
+#define CVC4__THEORY__BAGS__NORMAL_FORM_H
+
+namespace CVC4 {
+namespace theory {
+namespace bags {
+
+class NormalForm
+{
+ public:
+ /**
+ * Returns true if n is considered a to be a (canonical) constant bag value.
+ * A canonical bag value is one whose AST is:
+ * (disjoint-union (mk-bag e1 n1) ...
+ * (disjoint-union (mk-bag e_{n-1} n_{n-1}) (mk-bag e_n n_n))))
+ * where c1 ... cn are constants and the node identifier of these constants
+ * are such that:
+ * c1 > ... > cn.
+ * Also handles the corner cases of empty bag and singleton bag.
+ */
+ static bool checkNormalConstant(TNode n);
+};
+} // namespace bags
+} // namespace theory
+} // namespace CVC4
+
+#endif /* CVC4__THEORY__BAGS__NORMAL_FORM_H */
diff --git a/src/theory/bags/solver_state.cpp b/src/theory/bags/solver_state.cpp
new file mode 100644
index 000000000..77204ae76
--- /dev/null
+++ b/src/theory/bags/solver_state.cpp
@@ -0,0 +1,35 @@
+/********************* */
+/*! \file solver_state.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Mudathir Mohamed
+ ** 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 Implementation of bags state object
+ **/
+
+#include "theory/bags/solver_state.h"
+
+using namespace std;
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace bags {
+
+SolverState::SolverState(context::Context* c,
+ context::UserContext* u,
+ Valuation val)
+ : TheoryState(c, u, val)
+{
+ d_true = NodeManager::currentNM()->mkConst(true);
+ d_false = NodeManager::currentNM()->mkConst(false);
+}
+
+} // namespace bags
+} // namespace theory
+} // namespace CVC4
diff --git a/src/theory/bags/solver_state.h b/src/theory/bags/solver_state.h
new file mode 100644
index 000000000..f5b67cb78
--- /dev/null
+++ b/src/theory/bags/solver_state.h
@@ -0,0 +1,44 @@
+/********************* */
+/*! \file solver_state.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Mudathir Mohamed
+ ** 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 Bags state object
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__BAGS__THEORY_SOLVER_STATE_H
+#define CVC4__THEORY__BAGS__THEORY_SOLVER_STATE_H
+
+#include <map>
+#include <vector>
+
+#include "theory/theory_state.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bags {
+
+class SolverState : public TheoryState
+{
+ public:
+ SolverState(context::Context* c, context::UserContext* u, Valuation val);
+
+ private:
+ /** constants */
+ Node d_true;
+ Node d_false;
+}; /* class SolverState */
+
+} // namespace bags
+} // namespace theory
+} // namespace CVC4
+
+#endif /* CVC4__THEORY__BAGS__THEORY_SOLVER_STATE_H */
diff --git a/src/theory/bags/term_registry.cpp b/src/theory/bags/term_registry.cpp
new file mode 100644
index 000000000..60beef29f
--- /dev/null
+++ b/src/theory/bags/term_registry.cpp
@@ -0,0 +1,45 @@
+/********************* */
+/*! \file term_registry.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Mudathir Mohamed
+ ** 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 Implementation of bags term registry object
+ **/
+
+#include "theory/bags/term_registry.h"
+
+using namespace std;
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace bags {
+
+TermRegistry::TermRegistry(SolverState& state, InferenceManager& im)
+ : d_im(im),
+ d_proxy(state.getUserContext()),
+ d_proxy_to_term(state.getUserContext())
+{
+}
+
+Node TermRegistry::getEmptyBag(TypeNode tn)
+{
+ std::map<TypeNode, Node>::iterator it = d_emptybag.find(tn);
+ if (it != d_emptybag.end())
+ {
+ return it->second;
+ }
+ Node n = NodeManager::currentNM()->mkConst(EmptySet(tn));
+ d_emptybag[tn] = n;
+ return n;
+}
+
+} // namespace bags
+} // namespace theory
+} // namespace CVC4
diff --git a/src/theory/bags/term_registry.h b/src/theory/bags/term_registry.h
new file mode 100644
index 000000000..d284126ee
--- /dev/null
+++ b/src/theory/bags/term_registry.h
@@ -0,0 +1,63 @@
+/********************* */
+/*! \file term_registry.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Mudathir Mohamed
+ ** 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 Bags state object
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__BAGS__TERM_REGISTRY_H
+#define CVC4__THEORY__BAGS__TERM_REGISTRY_H
+
+#include <map>
+#include <vector>
+
+#include "context/cdhashmap.h"
+#include "theory/bags/inference_manager.h"
+#include "theory/bags/solver_state.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bags {
+
+/**
+ * Term registry, the purpose of this class is to maintain a database of
+ * commonly used terms, and mappings from bags to their "proxy variables".
+ */
+class TermRegistry
+{
+ typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap;
+
+ public:
+ TermRegistry(SolverState& state, InferenceManager& im);
+
+ /**
+ * Returns the existing empty bag for type tn
+ * or creates a new one and returns it.
+ **/
+ Node getEmptyBag(TypeNode tn);
+
+ private:
+ /** The inference manager */
+ InferenceManager& d_im;
+ /** Map from bag terms to their proxy variables */
+ NodeMap d_proxy;
+ /** Backwards map of above */
+ NodeMap d_proxy_to_term;
+ /** Map from types to empty bag of that type */
+ std::map<TypeNode, Node> d_emptybag;
+}; /* class Term */
+
+} // namespace bags
+} // namespace theory
+} // namespace CVC4
+
+#endif /* CVC4__THEORY__BAGS__TERM_REGISTRY_H */
diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp
new file mode 100644
index 000000000..5ddd17302
--- /dev/null
+++ b/src/theory/bags/theory_bags.cpp
@@ -0,0 +1,139 @@
+/********************* */
+/*! \file theory_bags.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Mudathir Mohamed
+ ** 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 Bags theory.
+ **/
+
+#include "theory/bags/theory_bags.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace bags {
+
+TheoryBags::TheoryBags(context::Context* c,
+ context::UserContext* u,
+ OutputChannel& out,
+ Valuation valuation,
+ const LogicInfo& logicInfo,
+ ProofNodeManager* pnm)
+ : Theory(THEORY_BAGS, c, u, out, valuation, logicInfo, pnm),
+ d_state(c, u, valuation),
+ d_im(*this, d_state, pnm),
+ d_rewriter(),
+ d_notify(*this, d_im)
+{
+ // use the official theory state and inference manager objects
+ d_theoryState = &d_state;
+ d_inferManager = &d_im;
+}
+
+TheoryBags::~TheoryBags() {}
+
+TheoryRewriter* TheoryBags::getTheoryRewriter() { return &d_rewriter; }
+
+bool TheoryBags::needsEqualityEngine(EeSetupInfo& esi)
+{
+ esi.d_notify = &d_notify;
+ esi.d_name = "theory::bags::ee";
+ return true;
+}
+
+void TheoryBags::finishInit()
+{
+ Assert(d_equalityEngine != nullptr);
+
+ // choice is used to eliminate witness
+ d_valuation.setUnevaluatedKind(WITNESS);
+
+ // functions we are doing congruence over
+ d_equalityEngine->addFunctionKind(UNION_MAX);
+ d_equalityEngine->addFunctionKind(UNION_DISJOINT);
+ d_equalityEngine->addFunctionKind(INTERSECTION_MIN);
+ d_equalityEngine->addFunctionKind(DIFFERENCE_SUBTRACT);
+ d_equalityEngine->addFunctionKind(DIFFERENCE_REMOVE);
+ d_equalityEngine->addFunctionKind(BAG_COUNT);
+ d_equalityEngine->addFunctionKind(MK_BAG);
+ d_equalityEngine->addFunctionKind(BAG_CARD);
+}
+
+void TheoryBags::postCheck(Effort level) {}
+
+void TheoryBags::notifyFact(TNode atom,
+ bool polarity,
+ TNode fact,
+ bool isInternal)
+{
+}
+
+bool TheoryBags::collectModelValues(TheoryModel* m,
+ const std::set<Node>& termBag)
+{
+ return true;
+}
+
+TrustNode TheoryBags::explain(TNode node) { return d_im.explainLit(node); }
+
+Node TheoryBags::getModelValue(TNode node) { return Node::null(); }
+
+void TheoryBags::preRegisterTerm(TNode node) {}
+
+TrustNode TheoryBags::expandDefinition(Node n)
+{
+ // TODO(projects#224): add choose and is_singleton here
+ return TrustNode::null();
+}
+
+void TheoryBags::presolve() {}
+
+/**************************** eq::NotifyClass *****************************/
+
+void TheoryBags::eqNotifyNewClass(TNode t)
+{
+ Assert(false) << "Not implemented yet" << std::endl;
+}
+
+void TheoryBags::eqNotifyMerge(TNode t1, TNode t2)
+{
+ Assert(false) << "Not implemented yet" << std::endl;
+}
+
+void TheoryBags::eqNotifyDisequal(TNode t1, TNode t2, TNode reason)
+{
+ Assert(false) << "Not implemented yet" << std::endl;
+}
+
+void TheoryBags::NotifyClass::eqNotifyNewClass(TNode t)
+{
+ Debug("bags-eq") << "[bags-eq] eqNotifyNewClass:"
+ << " t = " << t << std::endl;
+ d_theory.eqNotifyNewClass(t);
+}
+
+void TheoryBags::NotifyClass::eqNotifyMerge(TNode t1, TNode t2)
+{
+ Debug("bags-eq") << "[bags-eq] eqNotifyMerge:"
+ << " t1 = " << t1 << " t2 = " << t2 << std::endl;
+ d_theory.eqNotifyMerge(t1, t2);
+}
+
+void TheoryBags::NotifyClass::eqNotifyDisequal(TNode t1, TNode t2, TNode reason)
+{
+ Debug("bags-eq") << "[bags-eq] eqNotifyDisequal:"
+ << " t1 = " << t1 << " t2 = " << t2 << " reason = " << reason
+ << std::endl;
+ d_theory.eqNotifyDisequal(t1, t2, reason);
+}
+
+} // namespace bags
+} // namespace theory
+} // namespace CVC4
diff --git a/src/theory/bags/theory_bags.h b/src/theory/bags/theory_bags.h
new file mode 100644
index 000000000..44f7ae1b0
--- /dev/null
+++ b/src/theory/bags/theory_bags.h
@@ -0,0 +1,110 @@
+/********************* */
+/*! \file theory_bags.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Mudathir Mohamed
+ ** 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 Bags theory.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__BAGS__THEORY_BAGS_H
+#define CVC4__THEORY__BAGS__THEORY_BAGS_H
+
+#include <memory>
+
+#include "theory/bags/inference_manager.h"
+#include "theory/bags/solver_state.h"
+#include "theory/bags/theory_bags_rewriter.h"
+#include "theory/theory.h"
+#include "theory/theory_eq_notify.h"
+#include "theory/uf/equality_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bags {
+
+class TheoryBags : public Theory
+{
+ public:
+ /** Constructs a new instance of TheoryBags w.r.t. the provided contexts. */
+ TheoryBags(context::Context* c,
+ context::UserContext* u,
+ OutputChannel& out,
+ Valuation valuation,
+ const LogicInfo& logicInfo,
+ ProofNodeManager* pnm);
+ ~TheoryBags() override;
+
+ //--------------------------------- initialization
+ /** get the official theory rewriter of this theory */
+ TheoryRewriter* getTheoryRewriter() override;
+ /**
+ * Returns true if we need an equality engine. If so, we initialize the
+ * information regarding how it should be setup. For details, see the
+ * documentation in Theory::needsEqualityEngine.
+ */
+ bool needsEqualityEngine(EeSetupInfo& esi) override;
+ /** finish initialization */
+ void finishInit() override;
+ //--------------------------------- end initialization
+
+ //--------------------------------- standard check
+ /** Post-check, called after the fact queue of the theory is processed. */
+ void postCheck(Effort level) override;
+ /** Notify fact */
+ void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) override;
+ //--------------------------------- end standard check
+ /** Collect model values in m based on the relevant terms given by termSet */
+ bool collectModelValues(TheoryModel* m,
+ const std::set<Node>& termSet) override;
+ TrustNode explain(TNode) override;
+ Node getModelValue(TNode) override;
+ std::string identify() const override { return "THEORY_BAGS"; }
+ void preRegisterTerm(TNode node) override;
+ TrustNode expandDefinition(Node n) override;
+ void presolve() override;
+
+ private:
+ /** Functions to handle callbacks from equality engine */
+ class NotifyClass : public TheoryEqNotifyClass
+ {
+ public:
+ NotifyClass(TheoryBags& theory, TheoryInferenceManager& inferenceManager)
+
+ : TheoryEqNotifyClass(inferenceManager), d_theory(theory)
+ {
+ }
+ void eqNotifyNewClass(TNode t) override;
+ void eqNotifyMerge(TNode t1, TNode t2) override;
+ void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override;
+
+ private:
+ TheoryBags& d_theory;
+ };
+
+ /** The state of the bags solver at full effort */
+ SolverState d_state;
+ /** The inference manager */
+ InferenceManager d_im;
+ /** Instance of the above class */
+ NotifyClass d_notify;
+ /** The theory rewriter for this theory. */
+ TheoryBagsRewriter d_rewriter;
+
+ void eqNotifyNewClass(TNode t);
+ void eqNotifyMerge(TNode t1, TNode t2);
+ void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
+}; /* class TheoryBags */
+
+} // namespace bags
+} // namespace theory
+} // namespace CVC4
+
+#endif /* CVC4__THEORY__BAGS__THEORY_BAGS_H */
diff --git a/src/theory/bags/theory_bags_rewriter.cpp b/src/theory/bags/theory_bags_rewriter.cpp
new file mode 100644
index 000000000..aaf0ab98c
--- /dev/null
+++ b/src/theory/bags/theory_bags_rewriter.cpp
@@ -0,0 +1,37 @@
+/********************* */
+/*! \file theory_bags_rewriter.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Mudathir Mohamed
+ ** 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 Bags theory rewriter.
+ **/
+
+#include "theory/bags/theory_bags_rewriter.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace bags {
+
+RewriteResponse TheoryBagsRewriter::postRewrite(TNode node)
+{
+ // TODO(projects#225): complete the code here
+ return RewriteResponse(REWRITE_DONE, node);
+}
+
+RewriteResponse TheoryBagsRewriter::preRewrite(TNode node)
+{
+ // TODO(projects#225): complete the code here
+ return RewriteResponse(REWRITE_DONE, node);
+}
+
+} // namespace bags
+} // namespace theory
+} // namespace CVC4
diff --git a/src/theory/bags/theory_bags_rewriter.h b/src/theory/bags/theory_bags_rewriter.h
new file mode 100644
index 000000000..7be88636a
--- /dev/null
+++ b/src/theory/bags/theory_bags_rewriter.h
@@ -0,0 +1,38 @@
+/********************* */
+/*! \file theory_bags_rewriter.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Mudathir Mohamed
+ ** 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 Bags theory rewriter.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__BAGS__THEORY_BAGS_REWRITER_H
+#define CVC4__THEORY__BAGS__THEORY_BAGS_REWRITER_H
+
+#include "theory/rewriter.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bags {
+
+class TheoryBagsRewriter : public TheoryRewriter
+{
+ public:
+ RewriteResponse postRewrite(TNode node) override;
+
+ RewriteResponse preRewrite(TNode node) override;
+}; /* class TheoryBagsRewriter */
+
+} // namespace bags
+} // namespace theory
+} // namespace CVC4
+
+#endif /* CVC4__THEORY__BAGS__THEORY_BAGS_REWRITER_H */
diff --git a/src/theory/bags/theory_bags_type_enumerator.cpp b/src/theory/bags/theory_bags_type_enumerator.cpp
new file mode 100644
index 000000000..7975bb379
--- /dev/null
+++ b/src/theory/bags/theory_bags_type_enumerator.cpp
@@ -0,0 +1,85 @@
+/********************* */
+/*! \file theory_bags_type_enumerator.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Mudathir Mohamed
+ ** 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 bag enumerator implementation
+ **/
+
+#include "theory/bags/theory_bags_type_enumerator.h"
+
+#include "expr/emptybag.h"
+#include "theory/rewriter.h"
+#include "theory_bags_type_enumerator.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bags {
+
+BagEnumerator::BagEnumerator(TypeNode type, TypeEnumeratorProperties* tep)
+ : TypeEnumeratorBase<BagEnumerator>(type),
+ d_nodeManager(NodeManager::currentNM()),
+ d_elementTypeEnumerator(type.getBagElementType(), tep)
+{
+ d_currentBag = d_nodeManager->mkConst(EmptyBag(type));
+ d_element = *d_elementTypeEnumerator;
+}
+
+BagEnumerator::BagEnumerator(const BagEnumerator& enumerator)
+ : TypeEnumeratorBase<BagEnumerator>(enumerator.getType()),
+ d_nodeManager(enumerator.d_nodeManager),
+ d_elementTypeEnumerator(enumerator.d_elementTypeEnumerator),
+ d_currentBag(enumerator.d_currentBag),
+ d_element(enumerator.d_element)
+{
+}
+
+BagEnumerator::~BagEnumerator() {}
+
+Node BagEnumerator::operator*()
+{
+ Trace("bag-type-enum") << "BagEnumerator::operator* d_currentBag = "
+ << d_currentBag << std::endl;
+
+ return d_currentBag;
+}
+
+BagEnumerator& BagEnumerator::operator++()
+{
+ // increase the multiplicity by one
+ Node one = d_nodeManager->mkConst(Rational(1));
+ Node singleton = d_nodeManager->mkNode(kind::MK_BAG, d_element, one);
+ if (d_currentBag.getKind() == kind::EMPTYBAG)
+ {
+ d_currentBag = singleton;
+ }
+ else
+ {
+ d_currentBag =
+ d_nodeManager->mkNode(kind::UNION_DISJOINT, singleton, d_currentBag);
+ }
+
+ d_currentBag = Rewriter::rewrite(d_currentBag);
+
+ Assert(d_currentBag.isConst());
+
+ Trace("bag-type-enum") << "BagEnumerator::operator++ d_currentBag = "
+ << d_currentBag << std::endl;
+ return *this;
+}
+
+bool BagEnumerator::isFinished()
+{
+ // bags sequence is infinite and it never ends
+ return false;
+}
+
+} // namespace bags
+} // namespace theory
+} // namespace CVC4 \ No newline at end of file
diff --git a/src/theory/bags/theory_bags_type_enumerator.h b/src/theory/bags/theory_bags_type_enumerator.h
new file mode 100644
index 000000000..26639afd8
--- /dev/null
+++ b/src/theory/bags/theory_bags_type_enumerator.h
@@ -0,0 +1,91 @@
+/********************* */
+/*! \file theory_bags_type_enumerator.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Mudathir Mohamed
+ ** 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 type enumerator for bags
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__BAGS__TYPE_ENUMERATOR_H
+#define CVC4__THEORY__BAGS__TYPE_ENUMERATOR_H
+
+#include "expr/type_node.h"
+#include "theory/type_enumerator.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bags {
+
+class BagEnumerator : public TypeEnumeratorBase<BagEnumerator>
+{
+ public:
+ BagEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr);
+ BagEnumerator(const BagEnumerator& enumerator);
+ ~BagEnumerator();
+
+ Node operator*() override;
+
+ /**
+ * This operator iterates over the infinite bags constructed from the element
+ * type . Ideally iterating over bags of {1, 2, 3, ...} will return the
+ * following infinite sequence of bags, where n in the pair (m, n) means the
+ * multiplicity of the element m in the bag
+ * {}, sum = 0, #elements = 0, cardinality = 0
+ *
+ * {(1,1)}, sum = 2, #elements = 1, cardinality = 1
+ *
+ * {(2,1)}, sum = 3, #elements = 2, cardinality = 1
+ * {(1,2)}, sum = 3, #elements = 2, cardinality = 2
+ *
+ * {(3, 1)}, sum = 4, #elements = 3, cardinality = 1
+ * {(2, 2)}, sum = 4, #elements = 3, cardinality = 2
+ * {(1, 3)}, sum = 4, #elements = 3, cardinality = 3
+ *
+ * {(4, 1)}, sum = 5, #elements = 4, cardinality = 1
+ * {(3, 2)}, sum = 5, #elements = 4, cardinality = 2
+ * {(1, 1),(2, 1)}, sum = 5, #elements = 4, cardinality = 2
+ * {(2, 3)}, sum = 5, #elements = 4, cardinality = 3
+ * {(1, 4)}, sum = 5, #elements = 4, cardinality = 4
+ *
+ * {(5, 1)}, sum = 6, #elements = 5, cardinality = 1
+ * {(4, 2)}, sum = 6, #elements = 5, cardinality = 2
+ * {(1, 1), (3,1)}, sum = 6, #elements = 5, cardinality = 2
+ * {(3, 3)}, sum = 6, #elements = 5, cardinality = 3
+ * {(1, 1), (2,2)}, sum = 6, #elements = 5, cardinality = 3
+ * {(1, 2), (2,1)}, sum = 6, #elements = 5, cardinality = 3
+ * {(2, 4)}, sum = 6, #elements = 5, cardinality = 4
+ * {(1, 5)}, sum = 6, #elements = 5, cardinality = 5
+ *
+ * This seems too expensive to implement.
+ * For now we are implementing an obvious solution
+ * {(1,1)}, {(1,2)}, {(1,3)}, ... which works for both fininte and infinite
+ * types
+ */
+ BagEnumerator& operator++() override;
+
+ bool isFinished() override;
+
+ private:
+ /** a pointer to the node manager */
+ NodeManager* d_nodeManager;
+ /** an enumerator for the set of pairs of element type x integer type */
+ TypeEnumerator d_elementTypeEnumerator;
+ /** the current set returned by the set enumerator */
+ Node d_currentBag;
+ /** the first value returned by the element type enumerator*/
+ Node d_element;
+}; /* class BagEnumerator */
+
+} // namespace bags
+} // namespace theory
+} // namespace CVC4
+
+#endif /* CVC4__THEORY__BAGS__TYPE_ENUMERATOR_H */ \ No newline at end of file
diff --git a/src/theory/bags/theory_bags_type_rules.h b/src/theory/bags/theory_bags_type_rules.h
new file mode 100644
index 000000000..fc5a19348
--- /dev/null
+++ b/src/theory/bags/theory_bags_type_rules.h
@@ -0,0 +1,255 @@
+/********************* */
+/*! \file theory_bags_type_rules.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Mudathir Mohamed
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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 Bags theory type rules.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__BAGS__THEORY_BAGS_TYPE_RULES_H
+#define CVC4__THEORY__BAGS__THEORY_BAGS_TYPE_RULES_H
+
+#include "theory/bags/normal_form.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bags {
+
+struct BinaryOperatorTypeRule
+{
+ static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ {
+ Assert(n.getKind() == kind::UNION_MAX || n.getKind() == kind::UNION_DISJOINT
+ || n.getKind() == kind::INTERSECTION_MIN
+ || n.getKind() == kind::DIFFERENCE_SUBTRACT
+ || n.getKind() == kind::DIFFERENCE_REMOVE);
+ TypeNode bagType = n[0].getType(check);
+ if (check)
+ {
+ if (!bagType.isBag())
+ {
+ throw TypeCheckingExceptionPrivate(
+ n, "operator expects a bag, first argument is not");
+ }
+ TypeNode secondBagType = n[1].getType(check);
+ if (secondBagType != bagType)
+ {
+ if (n.getKind() == kind::INTERSECTION_MIN)
+ {
+ bagType = TypeNode::mostCommonTypeNode(secondBagType, bagType);
+ }
+ else
+ {
+ bagType = TypeNode::leastCommonTypeNode(secondBagType, bagType);
+ }
+ if (bagType.isNull())
+ {
+ throw TypeCheckingExceptionPrivate(
+ n, "operator expects two bags of comparable types");
+ }
+ }
+ }
+ return bagType;
+ }
+
+ static bool computeIsConst(NodeManager* nodeManager, TNode n)
+ {
+ // only UNION_DISJOINT has a const rule in kinds.
+ // Other binary operators do not have const rules in kinds
+ Assert(n.getKind() == kind::UNION_DISJOINT);
+ return NormalForm::checkNormalConstant(n);
+ }
+}; /* struct BinaryOperatorTypeRule */
+
+struct IsIncludedTypeRule
+{
+ static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ {
+ Assert(n.getKind() == kind::BAG_IS_INCLUDED);
+ TypeNode bagType = n[0].getType(check);
+ if (check)
+ {
+ if (!bagType.isBag())
+ {
+ throw TypeCheckingExceptionPrivate(
+ n, "BAG_IS_INCLUDED operating on non-bag");
+ }
+ TypeNode secondBagType = n[1].getType(check);
+ if (secondBagType != bagType)
+ {
+ if (!bagType.isComparableTo(secondBagType))
+ {
+ throw TypeCheckingExceptionPrivate(
+ n, "BAG_IS_INCLUDED operating on bags of different types");
+ }
+ }
+ }
+ return nodeManager->booleanType();
+ }
+}; /* struct IsIncludedTypeRule */
+
+struct CountTypeRule
+{
+ static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ {
+ Assert(n.getKind() == kind::BAG_COUNT);
+ TypeNode bagType = n[1].getType(check);
+ if (check)
+ {
+ if (!bagType.isBag())
+ {
+ throw TypeCheckingExceptionPrivate(
+ n, "checking for membership in a non-bag");
+ }
+ TypeNode elementType = n[0].getType(check);
+ // TODO(projects#226): comments from sets
+ //
+ // T : (Bag Int)
+ // B : (Bag Real)
+ // (= (as T (Bag Real)) B)
+ // (= (bag-count 0.5 B) 1)
+ // ...where (bag-count 0.5 T) is inferred
+
+ if (!elementType.isComparableTo(bagType.getBagElementType()))
+ {
+ std::stringstream ss;
+ ss << "member operating on bags of different types:\n"
+ << "child type: " << elementType << "\n"
+ << "not subtype: " << bagType.getBagElementType() << "\n"
+ << "in term : " << n;
+ throw TypeCheckingExceptionPrivate(n, ss.str());
+ }
+ }
+ return nodeManager->integerType();
+ }
+}; /* struct CountTypeRule */
+
+struct MkBagTypeRule
+{
+ static TypeNode computeType(NodeManager* nm, TNode n, bool check)
+ {
+ Assert(n.getKind() == kind::MK_BAG);
+ if (check)
+ {
+ if (n.getNumChildren() != 2)
+ {
+ std::stringstream ss;
+ ss << "operands in term " << n << " are " << n.getNumChildren()
+ << ", but MK_BAG expects 2 operands.";
+ throw TypeCheckingExceptionPrivate(n, ss.str());
+ }
+ TypeNode type1 = n[1].getType(check);
+ if (!type1.isInteger())
+ {
+ std::stringstream ss;
+ ss << "MK_BAG expects an integer for " << n[1] << ". Found" << type1;
+ throw TypeCheckingExceptionPrivate(n, ss.str());
+ }
+ }
+
+ return nm->mkBagType(n[0].getType(check));
+ }
+
+ static bool computeIsConst(NodeManager* nodeManager, TNode n)
+ {
+ Assert(n.getKind() == kind::MK_BAG);
+ // for a bag to be a constant, both the element and its multiplicity should
+ // be constants, and the multiplicity should be > 0.
+ return n[0].isConst() && n[1].isConst()
+ && n[1].getConst<Rational>().sgn() == 1;
+ }
+}; /* struct MkBagTypeRule */
+
+struct IsSingletonTypeRule
+{
+ static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ {
+ 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();
+ }
+}; /* struct IsMkBagTypeRule */
+
+struct EmptyBagTypeRule
+{
+ static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ {
+ Assert(n.getKind() == kind::EMPTYBAG);
+ EmptyBag emptyBag = n.getConst<EmptyBag>();
+ return emptyBag.getType();
+ }
+}; /* struct EmptyBagTypeRule */
+
+struct CardTypeRule
+{
+ static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ {
+ Assert(n.getKind() == kind::BAG_CARD);
+ TypeNode bagType = n[0].getType(check);
+ if (check)
+ {
+ if (!bagType.isBag())
+ {
+ throw TypeCheckingExceptionPrivate(
+ n, "cardinality operates on a bag, non-bag object found");
+ }
+ }
+ return nodeManager->integerType();
+ }
+}; /* struct CardTypeRule */
+
+struct ChooseTypeRule
+{
+ static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ {
+ Assert(n.getKind() == kind::BAG_CHOOSE);
+ TypeNode bagType = n[0].getType(check);
+ if (check)
+ {
+ if (!bagType.isBag())
+ {
+ throw TypeCheckingExceptionPrivate(
+ n, "CHOOSE operator expects a bag, a non-bag is found");
+ }
+ }
+ return bagType.getBagElementType();
+ }
+}; /* struct ChooseTypeRule */
+
+struct BagsProperties
+{
+ static Cardinality computeCardinality(TypeNode type)
+ {
+ return Cardinality::UNKNOWN_CARD;
+ }
+
+ static bool isWellFounded(TypeNode type) { return type[0].isWellFounded(); }
+
+ static Node mkGroundTerm(TypeNode type)
+ {
+ Assert(type.isBag());
+ return NodeManager::currentNM()->mkConst(EmptyBag(type));
+ }
+}; /* struct BagsProperties */
+
+} // namespace bags
+} // namespace theory
+} // namespace CVC4
+
+#endif /* CVC4__THEORY__BAGS__THEORY_BAGS_TYPE_RULES_H */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback