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

Line Exec Source
1
/*********************                                                        */
2
/*! \file quantifiers_state.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds
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 Utility for quantifiers state
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATE_H
18
#define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATE_H
19
20
#include "theory/theory.h"
21
#include "theory/theory_state.h"
22
23
namespace CVC4 {
24
namespace theory {
25
namespace quantifiers {
26
27
/**
28
 * The quantifiers state.
29
 */
30
class QuantifiersState : public TheoryState
31
{
32
 public:
33
  QuantifiersState(context::Context* c,
34
                   context::UserContext* u,
35
                   Valuation val,
36
                   const LogicInfo& logicInfo);
37
8992
  ~QuantifiersState() {}
38
  /**
39
   * Increment the instantiation counters, called once at the beginning of when
40
   * we perform a check with quantifiers engine for the given effort.
41
   */
42
  void incrementInstRoundCounters(Theory::Effort e);
43
  /**
44
   * Get whether we need to check at effort e based on the inst-when mode. This
45
   * option determines the policy of quantifier instantiation and theory
46
   * combination, e.g. does it run before, after, or interleaved with theory
47
   * combination. This is based on the state of the counters maintained by this
48
   * class.
49
   */
50
  bool getInstWhenNeedsCheck(Theory::Effort e) const;
51
  /** Get the number of instantiation rounds performed in this SAT context */
52
  uint64_t getInstRoundDepth() const;
53
  /** Get the total number of instantiation rounds performed */
54
  uint64_t getInstRounds() const;
55
  /** debug print equality engine on trace c */
56
  void debugPrintEqualityEngine(const char* c) const;
57
  /** get the logic info */
58
  const LogicInfo& getLogicInfo() const;
59
60
 private:
61
  /** The number of instantiation rounds in this SAT context */
62
  context::CDO<uint64_t> d_ierCounterc;
63
  /** The number of total instantiation rounds (full effort) */
64
  uint64_t d_ierCounter;
65
  /** The number of total instantiation rounds (last call effort) */
66
  uint64_t d_ierCounterLc;
67
  /**
68
   * A counter to remember the last value of d_ierCounterLc where we a
69
   * full effort check. This is used for interleaving theory combination
70
   * and quantifier instantiation rounds.
71
   */
72
  uint64_t d_ierCounterLastLc;
73
  /**
74
   * The number of instantiation rounds we run for each call to theory
75
   * combination.
76
   */
77
  uint64_t d_instWhenPhase;
78
  /** Information about the logic we're operating within. */
79
  const LogicInfo& d_logicInfo;
80
};
81
82
}  // namespace quantifiers
83
}  // namespace theory
84
}  // namespace CVC4
85
86
#endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATE_H */