GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/ematching/im_generator.h Lines: 2 6 33.3 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file inst_match_generator.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner, Tim King
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 inst match generator base class
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__QUANTIFIERS__IM_GENERATOR_H
18
#define CVC4__THEORY__QUANTIFIERS__IM_GENERATOR_H
19
20
#include <map>
21
#include "expr/node.h"
22
#include "theory/inference_id.h"
23
#include "theory/quantifiers/inst_match.h"
24
25
namespace CVC4 {
26
namespace theory {
27
28
class QuantifiersEngine;
29
30
namespace quantifiers {
31
class QuantifiersState;
32
}  // namespace quantifiers
33
34
namespace inst {
35
36
class Trigger;
37
38
/** IMGenerator class
39
*
40
* Virtual base class for generating InstMatch objects, which correspond to
41
* quantifier instantiations. The main use of this class is as a backend utility
42
* to Trigger (see theory/quantifiers/ematching/trigger.h).
43
*
44
* Some functions below take as argument a pointer to the current quantifiers
45
* engine, which is used for making various queries about what terms and
46
* equalities exist in the current context.
47
*
48
* Some functions below take a pointer to a parent Trigger object, which is used
49
* to post-process and finalize the instantiations through
50
* sendInstantiation(...), where the parent trigger will make calls to
51
* qe->getInstantiate()->addInstantiation(...). The latter function is the entry
52
* point in which instantiate lemmas are enqueued to be sent on the output
53
* channel.
54
*/
55
class IMGenerator {
56
public:
57
 IMGenerator(Trigger* tparent);
58
41581
 virtual ~IMGenerator() {}
59
 /** Reset instantiation round.
60
  *
61
  * Called once at beginning of an instantiation round.
62
  */
63
 virtual void resetInstantiationRound() {}
64
 /** Reset.
65
  *
66
  * eqc is the equivalence class to search in (any if eqc=null).
67
  * Returns true if this generator can produce instantiations, and false
68
  * otherwise. An example of when it returns false is if it can be determined
69
  * that no appropriate matchable terms occur based on eqc.
70
  */
71
80694
 virtual bool reset(Node eqc) { return true; }
72
 /** Get the next match.
73
  *
74
  * Must call reset( eqc ) before this function. This constructs an
75
  * instantiation, which it populates in data structure m,
76
  * based on the current context using the implemented matching algorithm.
77
  *
78
  * q is the quantified formula we are adding instantiations for
79
  * m is the InstMatch object we are generating
80
  *
81
  * Returns a value >0 if an instantiation was successfully generated
82
  */
83
 virtual int getNextMatch(Node q, InstMatch& m) { return 0; }
84
 /** add instantiations
85
  *
86
  * This adds all available instantiations for q based on the current context
87
  * using the implemented matching algorithm. It typically is implemented as a
88
  * fixed point of getNextMatch above.
89
  *
90
  * It returns the number of instantiations added using calls to
91
  * Instantiate::addInstantiation(...).
92
  */
93
 virtual uint64_t addInstantiations(Node q) { return 0; }
94
 /** get active score
95
  *
96
  * A heuristic value indicating how active this generator is.
97
  */
98
 virtual int getActiveScore() { return 0; }
99
100
protected:
101
 /** send instantiation
102
  *
103
  * This method sends instantiation, specified by m, to the parent trigger
104
  * object, which will in turn make a call to
105
  * Instantiate::addInstantiation(...). This method returns true if a
106
  * call to Instantiate::addInstantiation(...) was successfully made,
107
  * indicating that an instantiation was enqueued in the quantifier engine's
108
  * lemma cache.
109
  */
110
 bool sendInstantiation(InstMatch& m, InferenceId id);
111
 /** The parent trigger that owns this */
112
 Trigger* d_tparent;
113
 /** The state of the quantifiers engine */
114
 quantifiers::QuantifiersState& d_qstate;
115
 // !!!!!!!!! temporarily available (project #15)
116
 QuantifiersEngine* getQuantifiersEngine();
117
};/* class IMGenerator */
118
119
}
120
}
121
}
122
123
#endif