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

Line Exec Source
1
/*********************                                                        */
2
/*! \file non_clausal_simp.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Aina Niemetz, Gereon Kremer
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 Non-clausal simplification preprocessing pass.
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__PREPROCESSING__PASSES__NON_CLAUSAL_SIMP_H
18
#define CVC4__PREPROCESSING__PASSES__NON_CLAUSAL_SIMP_H
19
20
#include "context/cdlist.h"
21
#include "expr/node.h"
22
#include "preprocessing/preprocessing_pass.h"
23
#include "theory/trust_node.h"
24
25
namespace CVC4 {
26
27
class LazyCDProof;
28
class ProofNodeManager;
29
30
namespace smt {
31
class PreprocessProofGenerator;
32
}
33
namespace theory {
34
class TrustSubstitutionMap;
35
}
36
37
namespace preprocessing {
38
namespace passes {
39
40
17988
class NonClausalSimp : public PreprocessingPass
41
{
42
 public:
43
  NonClausalSimp(PreprocessingPassContext* preprocContext);
44
45
 protected:
46
  PreprocessingPassResult applyInternal(
47
      AssertionPipeline* assertionsToPreprocess) override;
48
49
 private:
50
  struct Statistics
51
  {
52
    IntStat d_numConstantProps;
53
    Statistics();
54
    ~Statistics();
55
  };
56
57
  Statistics d_statistics;
58
  /**
59
   * Transform learned literal lit. We apply substitutions in subs once and then
60
   * apply constant propagations cp to fixed point. Return the rewritten
61
   * form of lit.
62
   *
63
   * If proofs are enabled, then we require that the learned literal preprocess
64
   * proof generator (d_llpg) has a proof of lit when this method is called,
65
   * and ensure that the return literal also has a proof in d_llpg.
66
   */
67
  Node processLearnedLit(Node lit,
68
                         theory::TrustSubstitutionMap* subs,
69
                         theory::TrustSubstitutionMap* cp);
70
  /**
71
   * Process rewritten learned literal. This is called when we have a
72
   * learned literal lit that is rewritten to litr based on the proof generator
73
   * contained in trn (if it exists). The trust node trn should be of kind
74
   * REWRITE and proving (= lit litr).
75
   *
76
   * This tracks the proof in the learned literal preprocess proof generator
77
   * d_llpg below and returns the rewritten learned literal.
78
   */
79
  Node processRewrittenLearnedLit(theory::TrustNode trn);
80
  /** Is proof enabled? */
81
  bool isProofEnabled() const;
82
  /** The proof node manager */
83
  ProofNodeManager* d_pnm;
84
  /** the learned literal preprocess proof generator */
85
  std::unique_ptr<smt::PreprocessProofGenerator> d_llpg;
86
  /**
87
   * An lazy proof for learned literals that are reasserted into the assertions
88
   * pipeline by this class.
89
   */
90
  std::unique_ptr<LazyCDProof> d_llra;
91
  /**
92
   * A context-dependent list of trust substitution maps, which are required
93
   * for storing proofs.
94
   */
95
  context::CDList<std::shared_ptr<theory::TrustSubstitutionMap> > d_tsubsList;
96
};
97
98
}  // namespace passes
99
}  // namespace preprocessing
100
}  // namespace CVC4
101
102
#endif