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

Line Exec Source
1
/*********************                                                        */
2
/*! \file arith_preprocess.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 Arithmetic preprocess
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__ARITH__ARITH_PREPROCESS_H
18
#define CVC4__THEORY__ARITH__ARITH_PREPROCESS_H
19
20
#include "context/cdhashmap.h"
21
#include "theory/arith/operator_elim.h"
22
#include "theory/logic_info.h"
23
24
namespace CVC4 {
25
namespace theory {
26
27
class SkolemLemma;
28
29
namespace arith {
30
31
class ArithState;
32
class InferenceManager;
33
34
/**
35
 * This module can be used for (on demand) elimination of extended arithmetic
36
 * operators like div, mod, to_int, is_int, sqrt, and so on. It uses the
37
 * operator elimination utility for determining how to reduce formulas. It
38
 * extends that utility with the ability to generate lemmas on demand via
39
 * the provided inference manager.
40
 */
41
class ArithPreprocess
42
{
43
 public:
44
  ArithPreprocess(ArithState& state,
45
                  InferenceManager& im,
46
                  ProofNodeManager* pnm,
47
                  const LogicInfo& info);
48
8992
  ~ArithPreprocess() {}
49
  /**
50
   * Call eliminate operators on formula n, return the resulting trust node,
51
   * which is of TrustNodeKind REWRITE and whose node is the result of
52
   * eliminating extended operators from n.
53
   *
54
   * @param n The node to eliminate operators from
55
   * @param partialOnly Whether we are eliminating partial operators only.
56
   * @return the trust node proving (= n nr) where nr is the return of
57
   * eliminating operators in n, or the null trust node if n was unchanged.
58
   */
59
  TrustNode eliminate(TNode n,
60
                      std::vector<SkolemLemma>& lems,
61
                      bool partialOnly = false);
62
  /**
63
   * Reduce assertion. This sends a lemma via the inference manager if atom
64
   * contains any extended operators. When applicable, the lemma is of the form:
65
   *   atom == d_opElim.eliminate(atom)
66
   * This method returns true if a lemma of the above form was added to
67
   * the inference manager. Note this returns true even if this lemma was added
68
   * on a previous call.
69
   */
70
  bool reduceAssertion(TNode atom);
71
  /**
72
   * Is the atom reduced? Returns true if a call to method reduceAssertion was
73
   * made for the given atom and returned a lemma. In this case, the atom
74
   * can be ignored.
75
   */
76
  bool isReduced(TNode atom) const;
77
78
 private:
79
  /** Reference to the inference manager */
80
  InferenceManager& d_im;
81
  /** The operator elimination utility */
82
  OperatorElim d_opElim;
83
  /** The set of assertions that were reduced */
84
  context::CDHashMap<Node, bool, NodeHashFunction> d_reduced;
85
};
86
87
}  // namespace arith
88
}  // namespace theory
89
}  // namespace CVC4
90
91
#endif