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