Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/quant_module.h	Lines:	9	11	81.8 %
Date:	2021-09-18	Branches:	0	0	0.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds
 *
 * 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.
 * ****************************************************************************
 *
 * quantifier module
 */

#include "cvc5_private.h"

#ifndef CVC5__THEORY__QUANT_MODULE_H
#define CVC5__THEORY__QUANT_MODULE_H

#include <iostream>
#include <map>
#include <vector>

#include "smt/env_obj.h"
#include "theory/quantifiers/quantifiers_inference_manager.h"
#include "theory/quantifiers/quantifiers_registry.h"
#include "theory/quantifiers/quantifiers_state.h"
#include "theory/quantifiers/term_registry.h"
#include "theory/theory.h"
#include "theory/uf/equality_engine.h"

namespace cvc5 {
namespace theory {
namespace quantifiers {
class TermDb;
}  // namespace quantifiers

/** QuantifiersModule class
 *
 * This is the virtual class for defining subsolvers of the quantifiers theory.
 * It has a similar interface to a Theory object.
 */
class QuantifiersModule : protected EnvObj
{
 public:
  /** effort levels for quantifiers modules check */
  enum QEffort
  {
    // conflict effort, for conflict-based instantiation
    QEFFORT_CONFLICT,
    // standard effort, for heuristic instantiation
    QEFFORT_STANDARD,
    // model effort, for model-based instantiation
    QEFFORT_MODEL,
    // last call effort, for last resort techniques
    QEFFORT_LAST_CALL,
    // none
    QEFFORT_NONE,
  };

 public:
  QuantifiersModule(Env& env,
                    quantifiers::QuantifiersState& qs,
                    quantifiers::QuantifiersInferenceManager& qim,
                    quantifiers::QuantifiersRegistry& qr,
                    quantifiers::TermRegistry& tr);
  virtual ~QuantifiersModule() {}
  /** Presolve.
   *
   * Called at the beginning of check-sat call.
   */
  virtual void presolve() {}
  /** Needs check.
   *
   * Returns true if this module wishes a call to be made
   * to check(e) during QuantifiersEngine::check(e).
   */
  virtual bool needsCheck(Theory::Effort e)
  {
    return e >= Theory::EFFORT_LAST_CALL;
  }
  /** Needs model.
   *
   * Whether this module needs a model built during a
   * call to QuantifiersEngine::check(e)
   * It returns one of QEFFORT_* from the enumeration above.
   * which specifies the quantifiers effort in which it requires the model to
   * be built.
   */
  virtual QEffort needsModel(Theory::Effort e);
  /** Reset.
   *
   * Called at the beginning of QuantifiersEngine::check(e).
   */
  virtual void reset_round(Theory::Effort e) {}
  /** Check.
   *
   *   Called during QuantifiersEngine::check(e) depending
   *   if needsCheck(e) returns true.
   */
  virtual void check(Theory::Effort e, QEffort quant_e) = 0;
  /** Check complete?
   *
   * Returns false if the module's reasoning was globally incomplete
   * (e.g. "sat" must be replaced with "incomplete").
   *
   * This is called just before the quantifiers engine will return
   * with no lemmas added during a LAST_CALL effort check.
   *
   * If this method returns false, it should update incId to the reason for
   * why the module was incomplete.
   */
  virtual bool checkComplete(IncompleteId& incId) { return true; }
  /** Check was complete for quantified formula q
   *
   * If for each quantified formula q, some module returns true for
   * checkCompleteFor( q ),
   * and no lemmas are added by the quantifiers theory, then we may answer
   * "sat", unless
   * we are incomplete for other reasons.
   */
  virtual bool checkCompleteFor(Node q) { return false; }
  /** Check ownership
   *
   * Called once for new quantified formulas that are registered by the
   * quantifiers theory. The primary purpose of this function is to establish
   * if this module is the owner of quantified formula q.
   */
  virtual void checkOwnership(Node q) {}
  /** Register quantifier
   *
   * Called once for new quantified formulas q that are pre-registered by the
   * quantifiers theory, after internal ownership of quantified formulas is
   * finalized. This does context-independent initialization of this module
   * for quantified formula q.
   */
  virtual void registerQuantifier(Node q) {}
  /** Pre-register quantifier
   *
   * Called once for new quantified formulas that are
   * pre-registered by the quantifiers theory, after
   * internal ownership of quantified formulas is finalized.
   */
  virtual void preRegisterQuantifier(Node q) {}
  /** Assert node.
   *
   * Called when a quantified formula q is asserted to the quantifiers theory
   */
  virtual void assertNode(Node q) {}
  /** Identify this module (for debugging, dynamic configuration, etc..) */
  virtual std::string identify() const = 0;
  //----------------------------general queries
  /** get currently used the equality engine */
  eq::EqualityEngine* getEqualityEngine() const;
  /** are n1 and n2 equal in the current used equality engine? */
  bool areEqual(TNode n1, TNode n2) const;
  /** are n1 and n2 disequal in the current used equality engine? */
  bool areDisequal(TNode n1, TNode n2) const;
  /** get the representative of n in the current used equality engine */
  TNode getRepresentative(TNode n) const;
  /** get currently used term database */
  quantifiers::TermDb* getTermDatabase() const;
  /** get the quantifiers state */
  quantifiers::QuantifiersState& getState();
  /** get the quantifiers inference manager */
  quantifiers::QuantifiersInferenceManager& getInferenceManager();
  /** get the quantifiers registry */
  quantifiers::QuantifiersRegistry& getQuantifiersRegistry();
  //----------------------------end general queries
 protected:
  /** Reference to the state of the quantifiers engine */
  quantifiers::QuantifiersState& d_qstate;
  /** Reference to the quantifiers inference manager */
  quantifiers::QuantifiersInferenceManager& d_qim;
  /** Reference to the quantifiers registry */
  quantifiers::QuantifiersRegistry& d_qreg;
  /** Reference to the term registry */
  quantifiers::TermRegistry& d_treg;
}; /* class QuantifiersModule */

}  // namespace theory
}  // namespace cvc5

#endif /* CVC5__THEORY__QUANT_UTIL_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds
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		* quantifier module
14		*/
15
16		#include "cvc5_private.h"
17
18		#ifndef CVC5__THEORY__QUANT_MODULE_H
19		#define CVC5__THEORY__QUANT_MODULE_H
20
21		#include <iostream>
22		#include <map>
23		#include <vector>
24
25		#include "smt/env_obj.h"
26		#include "theory/quantifiers/quantifiers_inference_manager.h"
27		#include "theory/quantifiers/quantifiers_registry.h"
28		#include "theory/quantifiers/quantifiers_state.h"
29		#include "theory/quantifiers/term_registry.h"
30		#include "theory/theory.h"
31		#include "theory/uf/equality_engine.h"
32
33		namespace cvc5 {
34		namespace theory {
35		namespace quantifiers {
36		class TermDb;
37		} // namespace quantifiers
38
39		/** QuantifiersModule class
40		*
41		* This is the virtual class for defining subsolvers of the quantifiers theory.
42		* It has a similar interface to a Theory object.
43		*/
44		class QuantifiersModule : protected EnvObj
45		{
46		public:
47		/** effort levels for quantifiers modules check */
48		enum QEffort
49		{
50		// conflict effort, for conflict-based instantiation
51		QEFFORT_CONFLICT,
52		// standard effort, for heuristic instantiation
53		QEFFORT_STANDARD,
54		// model effort, for model-based instantiation
55		QEFFORT_MODEL,
56		// last call effort, for last resort techniques
57		QEFFORT_LAST_CALL,
58		// none
59		QEFFORT_NONE,
60		};
61
62		public:
63		QuantifiersModule(Env& env,
64		quantifiers::QuantifiersState& qs,
65		quantifiers::QuantifiersInferenceManager& qim,
66		quantifiers::QuantifiersRegistry& qr,
67		quantifiers::TermRegistry& tr);
68	34679	virtual ~QuantifiersModule() {}
69		/** Presolve.
70		*
71		* Called at the beginning of check-sat call.
72		*/
73	22750	virtual void presolve() {}
74		/** Needs check.
75		*
76		* Returns true if this module wishes a call to be made
77		* to check(e) during QuantifiersEngine::check(e).
78		*/
79		virtual bool needsCheck(Theory::Effort e)
80		{
81		return e >= Theory::EFFORT_LAST_CALL;
82		}
83		/** Needs model.
84		*
85		* Whether this module needs a model built during a
86		* call to QuantifiersEngine::check(e)
87		* It returns one of QEFFORT_* from the enumeration above.
88		* which specifies the quantifiers effort in which it requires the model to
89		* be built.
90		*/
91		virtual QEffort needsModel(Theory::Effort e);
92		/** Reset.
93		*
94		* Called at the beginning of QuantifiersEngine::check(e).
95		*/
96	32256	virtual void reset_round(Theory::Effort e) {}
97		/** Check.
98		*
99		* Called during QuantifiersEngine::check(e) depending
100		* if needsCheck(e) returns true.
101		*/
102		virtual void check(Theory::Effort e, QEffort quant_e) = 0;
103		/** Check complete?
104		*
105		* Returns false if the module's reasoning was globally incomplete
106		* (e.g. "sat" must be replaced with "incomplete").
107		*
108		* This is called just before the quantifiers engine will return
109		* with no lemmas added during a LAST_CALL effort check.
110		*
111		* If this method returns false, it should update incId to the reason for
112		* why the module was incomplete.
113		*/
114	10182	virtual bool checkComplete(IncompleteId& incId) { return true; }
115		/** Check was complete for quantified formula q
116		*
117		* If for each quantified formula q, some module returns true for
118		* checkCompleteFor( q ),
119		* and no lemmas are added by the quantifiers theory, then we may answer
120		* "sat", unless
121		* we are incomplete for other reasons.
122		*/
123	4150	virtual bool checkCompleteFor(Node q) { return false; }
124		/** Check ownership
125		*
126		* Called once for new quantified formulas that are registered by the
127		* quantifiers theory. The primary purpose of this function is to establish
128		* if this module is the owner of quantified formula q.
129		*/
130	55770	virtual void checkOwnership(Node q) {}
131		/** Register quantifier
132		*
133		* Called once for new quantified formulas q that are pre-registered by the
134		* quantifiers theory, after internal ownership of quantified formulas is
135		* finalized. This does context-independent initialization of this module
136		* for quantified formula q.
137		*/
138	39491	virtual void registerQuantifier(Node q) {}
139		/** Pre-register quantifier
140		*
141		* Called once for new quantified formulas that are
142		* pre-registered by the quantifiers theory, after
143		* internal ownership of quantified formulas is finalized.
144		*/
145	91786	virtual void preRegisterQuantifier(Node q) {}
146		/** Assert node.
147		*
148		* Called when a quantified formula q is asserted to the quantifiers theory
149		*/
150	326010	virtual void assertNode(Node q) {}
151		/** Identify this module (for debugging, dynamic configuration, etc..) */
152		virtual std::string identify() const = 0;
153		//----------------------------general queries
154		/** get currently used the equality engine */
155		eq::EqualityEngine* getEqualityEngine() const;
156		/** are n1 and n2 equal in the current used equality engine? */
157		bool areEqual(TNode n1, TNode n2) const;
158		/** are n1 and n2 disequal in the current used equality engine? */
159		bool areDisequal(TNode n1, TNode n2) const;
160		/** get the representative of n in the current used equality engine */
161		TNode getRepresentative(TNode n) const;
162		/** get currently used term database */
163		quantifiers::TermDb* getTermDatabase() const;
164		/** get the quantifiers state */
165		quantifiers::QuantifiersState& getState();
166		/** get the quantifiers inference manager */
167		quantifiers::QuantifiersInferenceManager& getInferenceManager();
168		/** get the quantifiers registry */
169		quantifiers::QuantifiersRegistry& getQuantifiersRegistry();
170		//----------------------------end general queries
171		protected:
172		/** Reference to the state of the quantifiers engine */
173		quantifiers::QuantifiersState& d_qstate;
174		/** Reference to the quantifiers inference manager */
175		quantifiers::QuantifiersInferenceManager& d_qim;
176		/** Reference to the quantifiers registry */
177		quantifiers::QuantifiersRegistry& d_qreg;
178		/** Reference to the term registry */
179		quantifiers::TermRegistry& d_treg;
180		}; /* class QuantifiersModule */
181
182		} // namespace theory
183		} // namespace cvc5
184
185		#endif /* CVC5__THEORY__QUANT_UTIL_H */