GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/ematching/inst_strategy_e_matching.h Lines: 3 3 100.0 %
Date: 2021-03-23 Branches: 10 14 71.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file inst_strategy_e_matching.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Morgan Deters, 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 E matching instantiation strategies
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__INST_STRATEGY_E_MATCHING_H
18
#define CVC4__INST_STRATEGY_E_MATCHING_H
19
20
#include "theory/quantifiers/ematching/inst_strategy.h"
21
#include "theory/quantifiers/ematching/trigger.h"
22
#include "theory/quantifiers/quant_relevance.h"
23
24
namespace CVC4 {
25
namespace theory {
26
namespace quantifiers {
27
28
/**
29
 * This class is responsible for instantiating quantifiers based on
30
 * automatically generated triggers. It selects pattern terms, generates
31
 * and manages triggers, and uses a strategy for processing them.
32
 */
33
class InstStrategyAutoGenTriggers : public InstStrategy
34
{
35
 public:
36
  enum
37
  {
38
    RELEVANCE_NONE,
39
    RELEVANCE_DEFAULT,
40
  };
41
42
 private:
43
  /** trigger generation strategy */
44
  options::TriggerSelMode d_tr_strategy;
45
  /** regeneration */
46
  bool d_regenerate;
47
  int d_regenerate_frequency;
48
  /** (single,multi) triggers for each quantifier */
49
  std::map<Node, std::map<inst::Trigger*, bool> > d_auto_gen_trigger[2];
50
  std::map<Node, int> d_counter;
51
  /** single, multi triggers for each quantifier */
52
  std::map<Node, std::vector<Node> > d_patTerms[2];
53
  std::map<Node, std::map<Node, bool> > d_patReqPol;
54
  /** information about triggers */
55
  std::map<Node, bool> d_is_single_trigger;
56
  std::map<Node, bool> d_single_trigger_gen;
57
  std::map<Node, bool> d_made_multi_trigger;
58
  // processed trigger this round
59
  std::map<Node, std::map<inst::Trigger*, bool> > d_processed_trigger;
60
  // instantiation no patterns
61
  std::map<Node, std::vector<Node> > d_user_no_gen;
62
  // number of trigger variables per quantifier
63
  std::map<Node, unsigned> d_num_trigger_vars;
64
  std::map<Node, Node> d_vc_partition[2];
65
  std::map<Node, Node> d_pat_to_mpat;
66
67
 private:
68
  /** process functions */
69
  void processResetInstantiationRound(Theory::Effort effort) override;
70
  /** Process */
71
  InstStrategyStatus process(Node q, Theory::Effort effort, int e) override;
72
  /**
73
   * Generate triggers for quantified formula q.
74
   */
75
  void generateTriggers(Node q);
76
  /**
77
   * Generate pattern terms for quantified formula q.
78
   */
79
  bool generatePatternTerms(Node q);
80
  void addPatternToPool(Node q, Node pat, unsigned num_fv, Node mpat);
81
  void addTrigger(inst::Trigger* tr, Node f);
82
  /** has user patterns */
83
  bool hasUserPatterns(Node q);
84
  /** has user patterns */
85
  std::map<Node, bool> d_hasUserPatterns;
86
87
 public:
88
  InstStrategyAutoGenTriggers(QuantifiersEngine* qe,
89
                              QuantifiersState& qs,
90
                              QuantifiersInferenceManager& qim,
91
                              QuantifiersRegistry& qr,
92
                              QuantRelevance* qrlv);
93
11644
  ~InstStrategyAutoGenTriggers() {}
94
95
  /** get auto-generated trigger */
96
  inst::Trigger* getAutoGenTrigger(Node q);
97
  /** identify */
98
80632
  std::string identify() const override
99
  {
100
80632
    return std::string("AutoGenTriggers");
101
  }
102
  /** add pattern */
103
  void addUserNoPattern(Node q, Node pat);
104
105
 private:
106
  /**
107
   * Pointer to the module that computes relevance of quantifiers, which is
108
   * owned by the instantiation engine that owns this class.
109
   */
110
  QuantRelevance* d_quant_rel;
111
}; /* class InstStrategyAutoGenTriggers */
112
}
113
}/* CVC4::theory namespace */
114
}/* CVC4 namespace */
115
116
#endif