diff options
author | mudathirmahgoub <mudathirmahgoub@gmail.com> | 2020-09-22 16:59:41 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-09-22 16:59:41 -0500 |
commit | e4a29a6033ecc7ba5ec266f37e8f151f09ead020 (patch) | |
tree | 26dff55bd5121dc311185dcd3071a6e8751f9f5e /src/theory | |
parent | 524c879720779abc3bc529459da8734f2eb3e3ad (diff) |
Add skeleton for theory of bags (multisets) (#5100)
This PR adds initial headers and mostly empty source files for the theory of bags (multisets).
It acts as a basis for future commits.
It includes straightforward implementation for typing rules an enumerator for bags.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/bags/inference_manager.cpp | 35 | ||||
-rw-r--r-- | src/theory/bags/inference_manager.h | 57 | ||||
-rw-r--r-- | src/theory/bags/kinds | 79 | ||||
-rw-r--r-- | src/theory/bags/normal_form.cpp | 27 | ||||
-rw-r--r-- | src/theory/bags/normal_form.h | 44 | ||||
-rw-r--r-- | src/theory/bags/solver_state.cpp | 35 | ||||
-rw-r--r-- | src/theory/bags/solver_state.h | 44 | ||||
-rw-r--r-- | src/theory/bags/term_registry.cpp | 45 | ||||
-rw-r--r-- | src/theory/bags/term_registry.h | 63 | ||||
-rw-r--r-- | src/theory/bags/theory_bags.cpp | 139 | ||||
-rw-r--r-- | src/theory/bags/theory_bags.h | 110 | ||||
-rw-r--r-- | src/theory/bags/theory_bags_rewriter.cpp | 37 | ||||
-rw-r--r-- | src/theory/bags/theory_bags_rewriter.h | 38 | ||||
-rw-r--r-- | src/theory/bags/theory_bags_type_enumerator.cpp | 85 | ||||
-rw-r--r-- | src/theory/bags/theory_bags_type_enumerator.h | 91 | ||||
-rw-r--r-- | src/theory/bags/theory_bags_type_rules.h | 255 | ||||
-rw-r--r-- | src/theory/logic_info.cpp | 5 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 1 | ||||
-rw-r--r-- | src/theory/theory_id.cpp | 2 | ||||
-rw-r--r-- | src/theory/theory_id.h | 1 |
20 files changed, 1193 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 */ diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index 4bbbdc322..73cd920d2 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -338,6 +338,11 @@ std::string LogicInfo::getLogicString() const { ss << "FS"; ++seen; } + if (d_theories[THEORY_BAGS]) + { + ss << "FB"; + ++seen; + } if(seen != d_sharingTheories) { Unhandled() << "can't extract a logic string from LogicInfo; at least one " diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 2d32b34d4..a425441fd 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -82,6 +82,7 @@ namespace theory { CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_DATATYPES) \ CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_SEP) \ CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_SETS) \ + CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_BAGS) \ CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_STRINGS) \ CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_QUANTIFIERS) diff --git a/src/theory/theory_id.cpp b/src/theory/theory_id.cpp index 5c11c340a..31b864e7f 100644 --- a/src/theory/theory_id.cpp +++ b/src/theory/theory_id.cpp @@ -43,6 +43,7 @@ std::ostream& operator<<(std::ostream& out, TheoryId theoryId) case THEORY_SAT_SOLVER: out << "THEORY_SAT_SOLVER"; break; case THEORY_SEP: out << "THEORY_SEP"; break; case THEORY_SETS: out << "THEORY_SETS"; break; + case THEORY_BAGS: out << "THEORY_BAGS"; break; case THEORY_STRINGS: out << "THEORY_STRINGS"; break; case THEORY_QUANTIFIERS: out << "THEORY_QUANTIFIERS"; break; @@ -65,6 +66,7 @@ std::string getStatsPrefix(TheoryId theoryId) case THEORY_DATATYPES: return "theory::datatypes"; break; case THEORY_SEP: return "theory::sep"; break; case THEORY_SETS: return "theory::sets"; break; + case THEORY_BAGS: return "theory::bags"; break; case THEORY_STRINGS: return "theory::strings"; break; case THEORY_QUANTIFIERS: return "theory::quantifiers"; break; diff --git a/src/theory/theory_id.h b/src/theory/theory_id.h index 60e005cf7..e0dfaa507 100644 --- a/src/theory/theory_id.h +++ b/src/theory/theory_id.h @@ -42,6 +42,7 @@ enum TheoryId THEORY_DATATYPES, THEORY_SEP, THEORY_SETS, + THEORY_BAGS, THEORY_STRINGS, THEORY_QUANTIFIERS, |