diff options
Diffstat (limited to 'src/theory/bags/bag_solver.h')
-rw-r--r-- | src/theory/bags/bag_solver.h | 70 |
1 files changed, 70 insertions, 0 deletions
diff --git a/src/theory/bags/bag_solver.h b/src/theory/bags/bag_solver.h new file mode 100644 index 000000000..48583d134 --- /dev/null +++ b/src/theory/bags/bag_solver.h @@ -0,0 +1,70 @@ +/********************* */ +/*! \file bag_solver.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 solver for the theory of bags. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__BAG__SOLVER_H +#define CVC4__THEORY__BAG__SOLVER_H + +#include "context/cdhashset.h" +#include "context/cdlist.h" +#include "theory/bags/infer_info.h" +#include "theory/bags/inference_manager.h" +#include "theory/bags/normal_form.h" +#include "theory/bags/solver_state.h" +#include "theory/bags/term_registry.h" + +namespace CVC4 { +namespace theory { +namespace bags { + +/** The solver for the theory of bags + * + */ +class BagSolver +{ + public: + BagSolver(SolverState& s, InferenceManager& im, TermRegistry& tr); + ~BagSolver(); + + void postCheck(); + + private: + /** apply inference rules for MK_BAG operator */ + void checkMkBag(const Node& n); + /** apply inference rules for union disjoint */ + void checkUnionDisjoint(const Node& n); + /** apply inference rules for union max */ + void checkUnionMax(const Node& n); + /** apply inference rules for difference subtract */ + void checkDifferenceSubtract(const Node& n); + + /** The solver state object */ + SolverState& d_state; + /** Reference to the inference manager for the theory of bags */ + InferenceManager& d_im; + /** Reference to the term registry of theory of bags */ + TermRegistry& d_termReg; + /** Commonly used constants */ + Node d_true; + Node d_false; + Node d_zero; + Node d_one; +}; /* class BagSolver */ + +} // namespace bags +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__BAG__SOLVER_H */ |