Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/ematching/im_generator.h	Lines:	2	6	33.3 %
Date:	2021-08-16	Branches:	0	0	0.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Clark Barrett
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Inst match generator base class.
 */

#include "cvc5_private.h"

#ifndef CVC5__THEORY__QUANTIFIERS__IM_GENERATOR_H
#define CVC5__THEORY__QUANTIFIERS__IM_GENERATOR_H

#include <map>
#include "expr/node.h"
#include "theory/inference_id.h"
#include "theory/quantifiers/inst_match.h"

namespace cvc5 {
namespace theory {
namespace quantifiers {

class QuantifiersState;
class TermRegistry;

namespace inst {

class Trigger;

/** IMGenerator class
 *
 * Virtual base class for generating InstMatch objects, which correspond to
 * quantifier instantiations. The main use of this class is as a backend utility
 * to Trigger (see theory/quantifiers/ematching/trigger.h).
 *
 * Some functions below take as argument a pointer to the current quantifiers
 * engine, which is used for making various queries about what terms and
 * equalities exist in the current context.
 *
 * Some functions below take a pointer to a parent Trigger object, which is used
 * to post-process and finalize the instantiations through
 * sendInstantiation(...), where the parent trigger will make calls to
 * Instantiate::addInstantiation(...). The latter function is the entry
 * point in which instantiate lemmas are enqueued to be sent on the output
 * channel.
 */
class IMGenerator {
public:
 IMGenerator(Trigger* tparent);
 virtual ~IMGenerator() {}
 /** Reset instantiation round.
  *
  * Called once at beginning of an instantiation round.
  */
 virtual void resetInstantiationRound() {}
 /** Reset.
  *
  * eqc is the equivalence class to search in (any if eqc=null).
  * Returns true if this generator can produce instantiations, and false
  * otherwise. An example of when it returns false is if it can be determined
  * that no appropriate matchable terms occur based on eqc.
  */
 virtual bool reset(Node eqc) { return true; }
 /** Get the next match.
  *
  * Must call reset( eqc ) before this function. This constructs an
  * instantiation, which it populates in data structure m,
  * based on the current context using the implemented matching algorithm.
  *
  * q is the quantified formula we are adding instantiations for
  * m is the InstMatch object we are generating
  *
  * Returns a value >0 if an instantiation was successfully generated
  */
 virtual int getNextMatch(Node q, InstMatch& m) { return 0; }
 /** add instantiations
  *
  * This adds all available instantiations for q based on the current context
  * using the implemented matching algorithm. It typically is implemented as a
  * fixed point of getNextMatch above.
  *
  * It returns the number of instantiations added using calls to
  * Instantiate::addInstantiation(...).
  */
 virtual uint64_t addInstantiations(Node q) { return 0; }
 /** get active score
  *
  * A heuristic value indicating how active this generator is.
  */
 virtual int getActiveScore() { return 0; }

protected:
 /** send instantiation
  *
  * This method sends instantiation, specified by m, to the parent trigger
  * object, which will in turn make a call to
  * Instantiate::addInstantiation(...). This method returns true if a
  * call to Instantiate::addInstantiation(...) was successfully made,
  * indicating that an instantiation was enqueued in the quantifier engine's
  * lemma cache.
  */
 bool sendInstantiation(InstMatch& m, InferenceId id);
 /** The parent trigger that owns this */
 Trigger* d_tparent;
 /** Reference to the state of the quantifiers engine */
 QuantifiersState& d_qstate;
 /** Reference to the term registry */
 TermRegistry& d_treg;
};/* class IMGenerator */

}  // namespace inst
}
}
}  // namespace cvc5

#endif


Generated by: GCOVR (Version 3.2)

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