GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bags/solver_state.h Lines: 1 1 100.0 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file solver_state.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Mudathir Mohamed
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief Bags state object
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__BAGS__THEORY_SOLVER_STATE_H
18
#define CVC4__THEORY__BAGS__THEORY_SOLVER_STATE_H
19
20
#include <map>
21
22
#include "theory/theory_state.h"
23
24
namespace CVC4 {
25
namespace theory {
26
namespace bags {
27
28
8994
class SolverState : public TheoryState
29
{
30
 public:
31
  SolverState(context::Context* c, context::UserContext* u, Valuation val);
32
33
  /**
34
   * This function adds the bag representative n to the set d_bags if it is not
35
   * already there. This function is called during postCheck to collect bag
36
   * terms in the equality engine. See the documentation of
37
   * @link SolverState::collectBagsAndCountTerms
38
   */
39
  void registerBag(TNode n);
40
41
  /**
42
   * @param n has the form (bag.count e A)
43
   * @pre bag A needs is already registered using registerBag(A)
44
   * @return a unique skolem for (bag.count e A)
45
   */
46
  void registerCountTerm(TNode n);
47
  /** get all bag terms that are representatives in the equality engine.
48
   * This function is valid after the current solver is initialized during
49
   * postCheck. See SolverState::initialize and BagSolver::postCheck
50
   */
51
  const std::set<Node>& getBags();
52
  /**
53
   * @pre B is a registered bag
54
   * @return all elements associated with bag B so far
55
   * Note that associated elements are not necessarily elements in B
56
   * Example:
57
   * (assert (= 0 (bag.count x B)))
58
   * element x is associated with bag B, albeit x is definitely not in B.
59
   */
60
  const std::set<Node>& getElements(Node B);
61
  /** initialize bag and count terms */
62
  void initialize();
63
  /** return disequal bag terms */
64
  const std::set<Node>& getDisequalBagTerms();
65
66
 private:
67
  /** clear all bags data structures */
68
  void reset();
69
  /**
70
   * collect bags' representatives and all count terms.
71
   * This function is called during postCheck
72
   */
73
  void collectBagsAndCountTerms();
74
  /**
75
   * collect disequal bag terms. This function is called during postCheck.
76
   */
77
  void collectDisequalBagTerms();
78
  /** constants */
79
  Node d_true;
80
  Node d_false;
81
  /** node manager for this solver state */
82
  NodeManager* d_nm;
83
  /** collection of bag representatives */
84
  std::set<Node> d_bags;
85
  /** bag -> associated elements */
86
  std::map<Node, std::set<Node>> d_bagElements;
87
  /** Disequal bag terms */
88
  std::set<Node> d_deq;
89
}; /* class SolverState */
90
91
}  // namespace bags
92
}  // namespace theory
93
}  // namespace CVC4
94
95
#endif /* CVC4__THEORY__BAGS__THEORY_SOLVER_STATE_H */