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

Line Exec Source
1
/*********************                                                        */
2
/*! \file quantifier_macros.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Yoni Zohar, Andrew Reynolds, Mathias Preiner
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 Pre-process step for detecting quantifier macro definitions
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H
18
#define CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H
19
20
#include <map>
21
#include <vector>
22
#include "expr/node.h"
23
#include "preprocessing/preprocessing_pass.h"
24
25
namespace CVC4 {
26
namespace preprocessing {
27
namespace passes {
28
29
class QuantifierMacros : public PreprocessingPass
30
{
31
 public:
32
  QuantifierMacros(PreprocessingPassContext* preprocContext);
33
17988
  ~QuantifierMacros() {}
34
 protected:
35
  PreprocessingPassResult applyInternal(
36
      AssertionPipeline* assertionsToPreprocess) override;
37
38
 private:
39
  bool processAssertion(Node n);
40
  bool isBoundVarApplyUf(Node n);
41
  bool process(Node n, bool pol, std::vector<Node>& args, Node f);
42
  bool containsBadOp(Node n,
43
                     Node op,
44
                     std::vector<Node>& opc,
45
                     std::map<Node, bool>& visited);
46
  bool isMacroLiteral(Node n, bool pol);
47
  bool isGroundUfTerm(Node f, Node n);
48
  void getMacroCandidates(Node n,
49
                          std::vector<Node>& candidates,
50
                          std::map<Node, bool>& visited);
51
  Node solveInEquality(Node n, Node lit);
52
  bool getFreeVariables(Node n,
53
                        std::vector<Node>& v_quant,
54
                        std::vector<Node>& vars,
55
                        bool retOnly,
56
                        std::map<Node, bool>& visited);
57
  bool getSubstitution(std::vector<Node>& v_quant,
58
                       std::map<Node, Node>& solved,
59
                       std::vector<Node>& vars,
60
                       std::vector<Node>& subs,
61
                       bool reqComplete);
62
  void addMacro(Node op, Node n, std::vector<Node>& opc);
63
  void debugMacroDefinition(Node oo, Node n);
64
  /**
65
   * This applies macro elimination to the given pipeline, which discovers
66
   * whether there are any quantified formulas corresponding to macros.
67
   *
68
   * @param ap The pipeline to apply macros to.
69
   * @param doRewrite Whether we also wish to rewrite the assertions based on
70
   * the discovered macro definitions.
71
   * @return Whether new definitions were inferred and we rewrote the assertions
72
   * based on them.
73
   */
74
  bool simplify(AssertionPipeline* ap, bool doRewrite = false);
75
  Node simplify(Node n);
76
  void finalizeDefinitions();
77
  void clearMaps();
78
79
  // map from operators to macro basis terms
80
  std::map<Node, std::vector<Node> > d_macro_basis;
81
  // map from operators to macro definition
82
  std::map<Node, Node> d_macro_defs;
83
  std::map<Node, Node> d_macro_defs_new;
84
  // operators to macro ops that contain them
85
  std::map<Node, std::vector<Node> > d_macro_def_contains;
86
  // simplify caches
87
  std::map<Node, Node> d_simplify_cache;
88
  std::map<Node, bool> d_quant_macros;
89
  bool d_ground_macros;
90
};
91
92
}  // passes
93
}  // preprocessing
94
}  // CVC4
95
96
#endif /*CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H */