Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/cegqi/inst_strategy_cegqi.h	Lines:	3	3	100.0 %
Date:	2021-08-17	Branches:	2	4	50.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Mathias Preiner, Tim King
 *
 * 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.
 * ****************************************************************************
 *
 * Counterexample-guided quantifier instantiation.
 */

#include "cvc5_private.h"

#ifndef CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_CEGQI_H
#define CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_CEGQI_H

#include "theory/decision_manager.h"
#include "theory/quantifiers/bv_inverter.h"
#include "theory/quantifiers/cegqi/ceg_instantiator.h"
#include "theory/quantifiers/cegqi/nested_qe.h"
#include "theory/quantifiers/cegqi/vts_term_cache.h"
#include "theory/quantifiers/instantiate.h"
#include "theory/quantifiers/quant_module.h"
#include "util/statistics_stats.h"

namespace cvc5 {
namespace theory {
namespace quantifiers {

class InstStrategyCegqi;

/**
 * An instantiation rewriter based on the counterexample-guided instantiation
 * quantifiers module below.
 */
class InstRewriterCegqi : public InstantiationRewriter
{
 public:
  InstRewriterCegqi(InstStrategyCegqi* p);
  ~InstRewriterCegqi() {}
  /**
   * Rewrite the instantiation via d_parent, based on virtual term substitution
   * and nested quantifier elimination. Returns a TrustNode of kind REWRITE,
   * corresponding to the rewrite and its proof generator.
   */
  TrustNode rewriteInstantiation(Node q,
                                 std::vector<Node>& terms,
                                 Node inst,
                                 bool doVts) override;

 private:
  /** pointer to the parent of this class */
  InstStrategyCegqi* d_parent;
};

/**
 * Counterexample-guided quantifier instantiation module.
 *
 * This class manages counterexample-guided instantiation strategies for all
 * asserted quantified formulas.
 */
class InstStrategyCegqi : public QuantifiersModule
{
  typedef context::CDHashSet<Node> NodeSet;
  typedef context::CDHashMap<Node, int> NodeIntMap;

 public:
  InstStrategyCegqi(QuantifiersState& qs,
                    QuantifiersInferenceManager& qim,
                    QuantifiersRegistry& qr,
                    TermRegistry& tr);
  ~InstStrategyCegqi();

  /** whether to do counterexample-guided instantiation for quantifier q */
  bool doCbqi(Node q);
  /** needs check at effort */
  bool needsCheck(Theory::Effort e) override;
  /** needs model at effort */
  QEffort needsModel(Theory::Effort e) override;
  /** reset round */
  void reset_round(Theory::Effort e) override;
  /** check */
  void check(Theory::Effort e, QEffort quant_e) override;
  /** check complete */
  bool checkComplete(IncompleteId& incId) override;
  /** check complete for quantified formula */
  bool checkCompleteFor(Node q) override;
  /** check ownership */
  void checkOwnership(Node q) override;
  /** identify */
  std::string identify() const override { return std::string("Cegqi"); }
  /** get instantiator for quantifier */
  CegInstantiator* getInstantiator(Node q);
  /** get the virtual term substitution term cache utility */
  VtsTermCache* getVtsTermCache() const;
  /** get the BV inverter utility */
  BvInverter* getBvInverter() const;
  /** pre-register quantifier */
  void preRegisterQuantifier(Node q) override;

  /**
   * Rewrite the instantiation inst of quantified formula q for terms; return
   * the result.
   *
   * We rewrite inst based on virtual term substitution and nested quantifier
   * elimination. For details, see "Solving Quantified Linear Arithmetic via
   * Counterexample-Guided Instantiation" FMSD 2017, Reynolds et al.
   *
   * Returns a TrustNode of kind REWRITE, corresponding to the rewrite and its
   * proof generator.
   */
  TrustNode rewriteInstantiation(Node q,
                                 std::vector<Node>& terms,
                                 Node inst,
                                 bool doVts);
  /** get the instantiation rewriter object */
  InstantiationRewriter* getInstRewriter() const;

  //------------------- interface for CegqiOutputInstStrategy
  /** Instantiate the current quantified formula forall x. Q with x -> subs. */
  bool doAddInstantiation(std::vector<Node>& subs);
  //------------------- end interface for CegqiOutputInstStrategy

 protected:
  /** The instantiation rewriter object */
  std::unique_ptr<InstRewriterCegqi> d_irew;
  /** set quantified formula inactive
   *
   * This flag is set to true during a full effort check if at least one
   * quantified formula is set "inactive", that is, its negation is
   * unsatisfiable in the current context.
   */
  bool d_cbqi_set_quant_inactive;
  /** incomplete check
   *
   * This is set to true during a full effort check if this strategy could
   * not find an instantiation for at least one asserted quantified formula.
   */
  bool d_incomplete_check;
  /** whether we have added cbqi lemma */
  NodeSet d_added_cbqi_lemma;
  /** parent guards */
  std::map< Node, std::vector< Node > > d_parent_quant;
  std::map< Node, std::vector< Node > > d_children_quant;
  std::map< Node, bool > d_active_quant;
  /** Whether cegqi handles each quantified formula. */
  std::map<Node, CegHandledStatus> d_do_cbqi;
  /**
   * The instantiator for each quantified formula q registered to this class.
   * This object is responsible for finding instantiatons for q.
   */
  std::map<Node, std::unique_ptr<CegInstantiator>> d_cinst;
  /** virtual term substitution term cache for arithmetic instantiation */
  std::unique_ptr<VtsTermCache> d_vtsCache;
  /** inversion utility for BV instantiation */
  std::unique_ptr<BvInverter> d_bv_invert;
  /**
   * The decision strategy for each quantified formula q registered to this
   * class.
   */
  std::map<Node, std::unique_ptr<DecisionStrategy>> d_dstrat;
  /** the current quantified formula we are processing */
  Node d_curr_quant;
  //---------------------- for vts delta minimization
  /**
   * Whether we will use vts delta minimization. If this flag is true, we
   * add lemmas on demand of the form delta < c^1, delta < c^2, ... where c
   * is a small (< 1) constant. This heuristic is used in strategies where
   * vts delta cannot be fully eliminated from assertions (for example, when
   * using nested quantifiers and a non-innermost instantiation strategy).
   * The same strategy applies for vts infinity, which we add lemmas of the
   * form inf > (1/c)^1, inf > (1/c)^2, ....
   */
  bool d_check_vts_lemma_lc;
  /** a multiplier used to make d_small_const even smaller over time */
  const Node d_small_const_multiplier;
  /** a small constant, used as a coefficient above */
  Node d_small_const;
  //---------------------- end for vts delta minimization
  /** register ce lemma */
  bool registerCbqiLemma( Node q );
  /** register counterexample lemma
   *
   * This is called when we have constructed lem, the negation of the body of
   * quantified formula q, skolemized with the instantiation constants of q.
   * This function is used for setting up the proper information in the
   * instantiator for q.
   */
  void registerCounterexampleLemma(Node q, Node lem);
  /** has added cbqi lemma */
  bool hasAddedCbqiLemma( Node q ) { return d_added_cbqi_lemma.find( q )!=d_added_cbqi_lemma.end(); }
  /**
   * Return true if q can be processed with nested quantifier elimination.
   * This may add a lemma on the output channel of quantifiers engine if so.
   *
   * @param q The quantified formula to process
   * @param isPreregister Whether this method is being called at preregister.
   */
  bool processNestedQe(Node q, bool isPreregister);
  /** process functions */
  void process(Node q, Theory::Effort effort, int e);
  /**
   * Get counterexample literal. This is the fresh Boolean variable whose
   * semantics is "there exists a set of values for which the body of
   * quantified formula q does not hold". These literals are cached by this
   * class.
   */
  Node getCounterexampleLiteral(Node q);
  /** map from universal quantifiers to their counterexample literals */
  std::map<Node, Node> d_ce_lit;
  /** The nested quantifier elimination utility */
  std::unique_ptr<NestedQe> d_nestedQe;
};

}
}
}  // namespace cvc5

#endif


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Mathias Preiner, Tim King
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		* Counterexample-guided quantifier instantiation.
14		*/
15
16		#include "cvc5_private.h"
17
18		#ifndef CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_CEGQI_H
19		#define CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_CEGQI_H
20
21		#include "theory/decision_manager.h"
22		#include "theory/quantifiers/bv_inverter.h"
23		#include "theory/quantifiers/cegqi/ceg_instantiator.h"
24		#include "theory/quantifiers/cegqi/nested_qe.h"
25		#include "theory/quantifiers/cegqi/vts_term_cache.h"
26		#include "theory/quantifiers/instantiate.h"
27		#include "theory/quantifiers/quant_module.h"
28		#include "util/statistics_stats.h"
29
30		namespace cvc5 {
31		namespace theory {
32		namespace quantifiers {
33
34		class InstStrategyCegqi;
35
36		/**
37		* An instantiation rewriter based on the counterexample-guided instantiation
38		* quantifiers module below.
39		*/
40		class InstRewriterCegqi : public InstantiationRewriter
41		{
42		public:
43		InstRewriterCegqi(InstStrategyCegqi* p);
44	13292	~InstRewriterCegqi() {}
45		/**
46		* Rewrite the instantiation via d_parent, based on virtual term substitution
47		* and nested quantifier elimination. Returns a TrustNode of kind REWRITE,
48		* corresponding to the rewrite and its proof generator.
49		*/
50		TrustNode rewriteInstantiation(Node q,
51		std::vector<Node>& terms,
52		Node inst,
53		bool doVts) override;
54
55		private:
56		/** pointer to the parent of this class */
57		InstStrategyCegqi* d_parent;
58		};
59
60		/**
61		* Counterexample-guided quantifier instantiation module.
62		*
63		* This class manages counterexample-guided instantiation strategies for all
64		* asserted quantified formulas.
65		*/
66		class InstStrategyCegqi : public QuantifiersModule
67		{
68		typedef context::CDHashSet<Node> NodeSet;
69		typedef context::CDHashMap<Node, int> NodeIntMap;
70
71		public:
72		InstStrategyCegqi(QuantifiersState& qs,
73		QuantifiersInferenceManager& qim,
74		QuantifiersRegistry& qr,
75		TermRegistry& tr);
76		~InstStrategyCegqi();
77
78		/** whether to do counterexample-guided instantiation for quantifier q */
79		bool doCbqi(Node q);
80		/** needs check at effort */
81		bool needsCheck(Theory::Effort e) override;
82		/** needs model at effort */
83		QEffort needsModel(Theory::Effort e) override;
84		/** reset round */
85		void reset_round(Theory::Effort e) override;
86		/** check */
87		void check(Theory::Effort e, QEffort quant_e) override;
88		/** check complete */
89		bool checkComplete(IncompleteId& incId) override;
90		/** check complete for quantified formula */
91		bool checkCompleteFor(Node q) override;
92		/** check ownership */
93		void checkOwnership(Node q) override;
94		/** identify */
95	131649	std::string identify() const override { return std::string("Cegqi"); }
96		/** get instantiator for quantifier */
97		CegInstantiator* getInstantiator(Node q);
98		/** get the virtual term substitution term cache utility */
99		VtsTermCache* getVtsTermCache() const;
100		/** get the BV inverter utility */
101		BvInverter* getBvInverter() const;
102		/** pre-register quantifier */
103		void preRegisterQuantifier(Node q) override;
104
105		/**
106		* Rewrite the instantiation inst of quantified formula q for terms; return
107		* the result.
108		*
109		* We rewrite inst based on virtual term substitution and nested quantifier
110		* elimination. For details, see "Solving Quantified Linear Arithmetic via
111		* Counterexample-Guided Instantiation" FMSD 2017, Reynolds et al.
112		*
113		* Returns a TrustNode of kind REWRITE, corresponding to the rewrite and its
114		* proof generator.
115		*/
116		TrustNode rewriteInstantiation(Node q,
117		std::vector<Node>& terms,
118		Node inst,
119		bool doVts);
120		/** get the instantiation rewriter object */
121		InstantiationRewriter* getInstRewriter() const;
122
123		//------------------- interface for CegqiOutputInstStrategy
124		/** Instantiate the current quantified formula forall x. Q with x -> subs. */
125		bool doAddInstantiation(std::vector<Node>& subs);
126		//------------------- end interface for CegqiOutputInstStrategy
127
128		protected:
129		/** The instantiation rewriter object */
130		std::unique_ptr<InstRewriterCegqi> d_irew;
131		/** set quantified formula inactive
132		*
133		* This flag is set to true during a full effort check if at least one
134		* quantified formula is set "inactive", that is, its negation is
135		* unsatisfiable in the current context.
136		*/
137		bool d_cbqi_set_quant_inactive;
138		/** incomplete check
139		*
140		* This is set to true during a full effort check if this strategy could
141		* not find an instantiation for at least one asserted quantified formula.
142		*/
143		bool d_incomplete_check;
144		/** whether we have added cbqi lemma */
145		NodeSet d_added_cbqi_lemma;
146		/** parent guards */
147		std::map< Node, std::vector< Node > > d_parent_quant;
148		std::map< Node, std::vector< Node > > d_children_quant;
149		std::map< Node, bool > d_active_quant;
150		/** Whether cegqi handles each quantified formula. */
151		std::map<Node, CegHandledStatus> d_do_cbqi;
152		/**
153		* The instantiator for each quantified formula q registered to this class.
154		* This object is responsible for finding instantiatons for q.
155		*/
156		std::map<Node, std::unique_ptr<CegInstantiator>> d_cinst;
157		/** virtual term substitution term cache for arithmetic instantiation */
158		std::unique_ptr<VtsTermCache> d_vtsCache;
159		/** inversion utility for BV instantiation */
160		std::unique_ptr<BvInverter> d_bv_invert;
161		/**
162		* The decision strategy for each quantified formula q registered to this
163		* class.
164		*/
165		std::map<Node, std::unique_ptr<DecisionStrategy>> d_dstrat;
166		/** the current quantified formula we are processing */
167		Node d_curr_quant;
168		//---------------------- for vts delta minimization
169		/**
170		* Whether we will use vts delta minimization. If this flag is true, we
171		* add lemmas on demand of the form delta < c^1, delta < c^2, ... where c
172		* is a small (< 1) constant. This heuristic is used in strategies where
173		* vts delta cannot be fully eliminated from assertions (for example, when
174		* using nested quantifiers and a non-innermost instantiation strategy).
175		* The same strategy applies for vts infinity, which we add lemmas of the
176		* form inf > (1/c)^1, inf > (1/c)^2, ....
177		*/
178		bool d_check_vts_lemma_lc;
179		/** a multiplier used to make d_small_const even smaller over time */
180		const Node d_small_const_multiplier;
181		/** a small constant, used as a coefficient above */
182		Node d_small_const;
183		//---------------------- end for vts delta minimization
184		/** register ce lemma */
185		bool registerCbqiLemma( Node q );
186		/** register counterexample lemma
187		*
188		* This is called when we have constructed lem, the negation of the body of
189		* quantified formula q, skolemized with the instantiation constants of q.
190		* This function is used for setting up the proper information in the
191		* instantiator for q.
192		*/
193		void registerCounterexampleLemma(Node q, Node lem);
194		/** has added cbqi lemma */
195	1774	bool hasAddedCbqiLemma( Node q ) { return d_added_cbqi_lemma.find( q )!=d_added_cbqi_lemma.end(); }
196		/**
197		* Return true if q can be processed with nested quantifier elimination.
198		* This may add a lemma on the output channel of quantifiers engine if so.
199		*
200		* @param q The quantified formula to process
201		* @param isPreregister Whether this method is being called at preregister.
202		*/
203		bool processNestedQe(Node q, bool isPreregister);
204		/** process functions */
205		void process(Node q, Theory::Effort effort, int e);
206		/**
207		* Get counterexample literal. This is the fresh Boolean variable whose
208		* semantics is "there exists a set of values for which the body of
209		* quantified formula q does not hold". These literals are cached by this
210		* class.
211		*/
212		Node getCounterexampleLiteral(Node q);
213		/** map from universal quantifiers to their counterexample literals */
214		std::map<Node, Node> d_ce_lit;
215		/** The nested quantifier elimination utility */
216		std::unique_ptr<NestedQe> d_nestedQe;
217		};
218
219		}
220		}
221		} // namespace cvc5
222
223		#endif