Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/sygus/sygus_module.h	Lines:	2	5	40.0 %
Date:	2021-05-22	Branches:	0	0	0.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Mathias Preiner, Andres Noetzli
 *
 * 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.
 * ****************************************************************************
 *
 * sygus_module
 */

#include "cvc5_private.h"

#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_MODULE_H
#define CVC5__THEORY__QUANTIFIERS__SYGUS_MODULE_H

#include <vector>

#include "expr/node.h"

namespace cvc5 {
namespace theory {
namespace quantifiers {

class SynthConjecture;
class TermDbSygus;
class QuantifiersInferenceManager;

/** SygusModule
 *
 * This is the base class of sygus modules, owned by SynthConjecture. The
 * purpose of this class is to, when applicable, suggest candidate solutions for
 * SynthConjecture to test.
 *
 * In more detail, an instance of the conjecture class (SynthConjecture) creates
 * the negated deep embedding form of the synthesis conjecture. In the
 * following, assume this is:
 *   forall d. exists x. P( d, x )
 * where d are of sygus datatype type. The "base instantiation" of this
 * conjecture (see SynthConjecture::d_base_inst) is the formula:
 *   exists y. P( k, y )
 * where k are the "candidate" variables for the conjecture.
 *
 * Modules implement an initialize function, which determines whether the module
 * will take responsibility for the given conjecture.
 */
class SygusModule
{
 public:
  SygusModule(QuantifiersInferenceManager& qim,
              TermDbSygus* tds,
              SynthConjecture* p);
  virtual ~SygusModule() {}
  /** initialize
   *
   * This function initializes the module for solving the given conjecture. This
   * typically involves registering enumerators (for constructing terms) via
   * calls to TermDbSygus::registerEnumerator.
   *
   * This function returns true if this module will take responsibility for
   * constructing candidates for the given conjecture.
   *
   * conj is the synthesis conjecture (prior to deep-embedding).
   *
   * n is the "base instantiation" of the deep-embedding version of the
   * synthesis conjecture under candidates (see SynthConjecture::d_base_inst).
   *
   * This function may add lemmas to the argument lemmas, which should be
   * sent out on the output channel of quantifiers by the caller.
   */
  virtual bool initialize(Node conj,
                          Node n,
                          const std::vector<Node>& candidates,
                          std::vector<Node>& lemmas) = 0;
  /** get term list
   *
   * This gets the list of terms that will appear as arguments to a subsequent
   * call to constructCandidates.
   */
  virtual void getTermList(const std::vector<Node>& candidates,
                           std::vector<Node>& terms) = 0;
  /** allow partial model
   *
   * This method returns true if this module does not require that all
   * terms returned by getTermList have "proper" model values when calling
   * constructCandidates. A term may have a model value that is not proper
   * if is excluded by symmetry breaking, e.g. x+0 is not proper. All model
   * values that are not proper are replaced by "null" when calling
   * constructCandidates.
   */
  virtual bool allowPartialModel() { return false; }
  /** construct candidate
   *
   * This function takes as input:
   *   terms : (a subset of) the terms returned by a call to getTermList,
   *   term_values : the current model values of terms,
   *   candidates : the list of candidates.
   *
   * In particular, notice that terms do not include inactive enumerators,
   * thus if inactive enumerators were added to getTermList, then the terms
   * list passed to this call will be a (strict) subset of that list.
   *
   * If this function returns true, it adds to candidate_values a list of terms
   * of the same length and type as candidates that are candidate solutions
   * to the synthesis conjecture in question. This candidate { v } will then be
   * tested by testing the (un)satisfiablity of P( v, cex ) for fresh cex by the
   * caller.
   *
   * This function may also add lemmas to lems, which are sent out as lemmas
   * on the output channel of quantifiers by the caller. For an example of
   * such lemmas, see SygusPbe::constructCandidates.
   *
   * This function may return false if it does not have a candidate it wants
   * to test on this iteration. In this case, lems should be non-empty.
   */
  virtual bool constructCandidates(const std::vector<Node>& terms,
                                   const std::vector<Node>& term_values,
                                   const std::vector<Node>& candidates,
                                   std::vector<Node>& candidate_values,
                                   std::vector<Node>& lems) = 0;
  /** register refinement lemma
   *
   * Assume this module, on a previous call to constructCandidates, added the
   * value { v } to candidate_values for candidates = { k }. This function is
   * called if the base instantiation of the synthesis conjecture has a model
   * under this substitution. In particular, in the above example, this function
   * is called when the refinement lemma P( v, cex ) has a model M. In calls to
   * this function, the argument vars is cex and lem is P( k, cex^M ).
   *
   * This function may also add lemmas to lems, which are sent out as lemmas
   * on the output channel of quantifiers by the caller. For an example of
   * such lemmas, see Cegis::registerRefinementLemma.
   */
  virtual void registerRefinementLemma(const std::vector<Node>& vars,
                                       Node lem,
                                       std::vector<Node>& lems)
  {
  }
  /**
   * Are we trying to repair constants in candidate solutions?
   * If we return true for usingRepairConst is true, then this module has
   * attmepted to repair any solutions returned by constructCandidates.
   */
  virtual bool usingRepairConst() { return false; }

 protected:
  /** Reference to the quantifiers inference manager */
  QuantifiersInferenceManager& d_qim;
  /** sygus term database of d_qe */
  TermDbSygus* d_tds;
  /** reference to the parent conjecture */
  SynthConjecture* d_parent;
};

}  // namespace quantifiers
}  // namespace theory
}  // namespace cvc5

#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_MODULE_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Mathias Preiner, Andres Noetzli
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		* sygus_module
14		*/
15
16		#include "cvc5_private.h"
17
18		#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_MODULE_H
19		#define CVC5__THEORY__QUANTIFIERS__SYGUS_MODULE_H
20
21		#include <vector>
22
23		#include "expr/node.h"
24
25		namespace cvc5 {
26		namespace theory {
27		namespace quantifiers {
28
29		class SynthConjecture;
30		class TermDbSygus;
31		class QuantifiersInferenceManager;
32
33		/** SygusModule
34		*
35		* This is the base class of sygus modules, owned by SynthConjecture. The
36		* purpose of this class is to, when applicable, suggest candidate solutions for
37		* SynthConjecture to test.
38		*
39		* In more detail, an instance of the conjecture class (SynthConjecture) creates
40		* the negated deep embedding form of the synthesis conjecture. In the
41		* following, assume this is:
42		* forall d. exists x. P( d, x )
43		* where d are of sygus datatype type. The "base instantiation" of this
44		* conjecture (see SynthConjecture::d_base_inst) is the formula:
45		* exists y. P( k, y )
46		* where k are the "candidate" variables for the conjecture.
47		*
48		* Modules implement an initialize function, which determines whether the module
49		* will take responsibility for the given conjecture.
50		*/
51		class SygusModule
52		{
53		public:
54		SygusModule(QuantifiersInferenceManager& qim,
55		TermDbSygus* tds,
56		SynthConjecture* p);
57	6116	virtual ~SygusModule() {}
58		/** initialize
59		*
60		* This function initializes the module for solving the given conjecture. This
61		* typically involves registering enumerators (for constructing terms) via
62		* calls to TermDbSygus::registerEnumerator.
63		*
64		* This function returns true if this module will take responsibility for
65		* constructing candidates for the given conjecture.
66		*
67		* conj is the synthesis conjecture (prior to deep-embedding).
68		*
69		* n is the "base instantiation" of the deep-embedding version of the
70		* synthesis conjecture under candidates (see SynthConjecture::d_base_inst).
71		*
72		* This function may add lemmas to the argument lemmas, which should be
73		* sent out on the output channel of quantifiers by the caller.
74		*/
75		virtual bool initialize(Node conj,
76		Node n,
77		const std::vector<Node>& candidates,
78		std::vector<Node>& lemmas) = 0;
79		/** get term list
80		*
81		* This gets the list of terms that will appear as arguments to a subsequent
82		* call to constructCandidates.
83		*/
84		virtual void getTermList(const std::vector<Node>& candidates,
85		std::vector<Node>& terms) = 0;
86		/** allow partial model
87		*
88		* This method returns true if this module does not require that all
89		* terms returned by getTermList have "proper" model values when calling
90		* constructCandidates. A term may have a model value that is not proper
91		* if is excluded by symmetry breaking, e.g. x+0 is not proper. All model
92		* values that are not proper are replaced by "null" when calling
93		* constructCandidates.
94		*/
95	35048	virtual bool allowPartialModel() { return false; }
96		/** construct candidate
97		*
98		* This function takes as input:
99		* terms : (a subset of) the terms returned by a call to getTermList,
100		* term_values : the current model values of terms,
101		* candidates : the list of candidates.
102		*
103		* In particular, notice that terms do not include inactive enumerators,
104		* thus if inactive enumerators were added to getTermList, then the terms
105		* list passed to this call will be a (strict) subset of that list.
106		*
107		* If this function returns true, it adds to candidate_values a list of terms
108		* of the same length and type as candidates that are candidate solutions
109		* to the synthesis conjecture in question. This candidate { v } will then be
110		* tested by testing the (un)satisfiablity of P( v, cex ) for fresh cex by the
111		* caller.
112		*
113		* This function may also add lemmas to lems, which are sent out as lemmas
114		* on the output channel of quantifiers by the caller. For an example of
115		* such lemmas, see SygusPbe::constructCandidates.
116		*
117		* This function may return false if it does not have a candidate it wants
118		* to test on this iteration. In this case, lems should be non-empty.
119		*/
120		virtual bool constructCandidates(const std::vector<Node>& terms,
121		const std::vector<Node>& term_values,
122		const std::vector<Node>& candidates,
123		std::vector<Node>& candidate_values,
124		std::vector<Node>& lems) = 0;
125		/** register refinement lemma
126		*
127		* Assume this module, on a previous call to constructCandidates, added the
128		* value { v } to candidate_values for candidates = { k }. This function is
129		* called if the base instantiation of the synthesis conjecture has a model
130		* under this substitution. In particular, in the above example, this function
131		* is called when the refinement lemma P( v, cex ) has a model M. In calls to
132		* this function, the argument vars is cex and lem is P( k, cex^M ).
133		*
134		* This function may also add lemmas to lems, which are sent out as lemmas
135		* on the output channel of quantifiers by the caller. For an example of
136		* such lemmas, see Cegis::registerRefinementLemma.
137		*/
138		virtual void registerRefinementLemma(const std::vector<Node>& vars,
139		Node lem,
140		std::vector<Node>& lems)
141		{
142		}
143		/**
144		* Are we trying to repair constants in candidate solutions?
145		* If we return true for usingRepairConst is true, then this module has
146		* attmepted to repair any solutions returned by constructCandidates.
147		*/
148		virtual bool usingRepairConst() { return false; }
149
150		protected:
151		/** Reference to the quantifiers inference manager */
152		QuantifiersInferenceManager& d_qim;
153		/** sygus term database of d_qe */
154		TermDbSygus* d_tds;
155		/** reference to the parent conjecture */
156		SynthConjecture* d_parent;
157		};
158
159		} // namespace quantifiers
160		} // namespace theory
161		} // namespace cvc5
162
163		#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_MODULE_H */