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

Line Exec Source
1
/*********************                                                        */
2
/*! \file factoring_check.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Gereon Kremer, 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 Check for factoring lemma
13
 **/
14
15
#ifndef CVC4__THEORY__ARITH__NL__EXT__FACTORING_CHECK_H
16
#define CVC4__THEORY__ARITH__NL__EXT__FACTORING_CHECK_H
17
18
#include <vector>
19
20
#include "expr/node.h"
21
22
namespace CVC4 {
23
24
class CDProof;
25
26
namespace theory {
27
namespace arith {
28
namespace nl {
29
30
struct ExtState;
31
32
4388
class FactoringCheck
33
{
34
 public:
35
  FactoringCheck(ExtState* data);
36
37
  /** check factoring
38
   *
39
   * Returns a set of valid theory lemmas, based on a
40
   * lemma schema that states a relationship between monomials
41
   * with common factors that occur in the same constraint.
42
   *
43
   * Examples:
44
   *
45
   * x*z+y*z > t => ( k = x + y ^ k*z > t )
46
   *   ...where k is fresh and x*z + y*z > t is a
47
   *      constraint that occurs in the current context.
48
   */
49
  void check(const std::vector<Node>& asserts,
50
             const std::vector<Node>& false_asserts);
51
52
 private:
53
  /** Basic data that is shared with other checks */
54
  ExtState* d_data;
55
56
  /** maps nodes to their factor skolems */
57
  std::map<Node, Node> d_factor_skolem;
58
59
  Node d_zero;
60
  Node d_one;
61
62
  /**
63
   * Introduces a new purification skolem k for n and adds k=n as lemma.
64
   * If proof is not nullptr, it proves this lemma via MACRO_SR_PRED_INTRO.
65
   */
66
  Node getFactorSkolem(Node n, CDProof* proof);
67
};
68
69
}  // namespace nl
70
}  // namespace arith
71
}  // namespace theory
72
}  // namespace CVC4
73
74
#endif