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

Line Exec Source
1
/*********************                                                        */
2
/*! \file split_zero_check.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Gereon Kremer, Andrew Reynolds, Tim King
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 Check for split zero lemma
13
 **/
14
15
#ifndef CVC4__THEORY__ARITH__NL__EXT__SPLIT_ZERO_CHECK_H
16
#define CVC4__THEORY__ARITH__NL__EXT__SPLIT_ZERO_CHECK_H
17
18
#include "expr/node.h"
19
#include "context/cdhashset.h"
20
21
namespace CVC4 {
22
namespace theory {
23
namespace arith {
24
namespace nl {
25
26
struct ExtState;
27
28
4388
class SplitZeroCheck
29
{
30
 public:
31
  SplitZeroCheck(ExtState* data);
32
33
  /** check split zero
34
   *
35
   * Returns a set of theory lemmas of the form
36
   *   t = 0 V t != 0
37
   * where t is a term that exists in the current context.
38
   */
39
  void check();
40
41
 private:
42
  using NodeSet = context::CDHashSet<Node, NodeHashFunction>;
43
44
  /** Basic data that is shared with other checks */
45
  ExtState* d_data;
46
  /** cache of terms t for which we have added the lemma ( t = 0 V t != 0 ). */
47
  NodeSet d_zero_split;
48
};
49
50
}  // namespace nl
51
}  // namespace arith
52
}  // namespace theory
53
}  // namespace CVC4
54
55
#endif