Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/sygus/sygus_interpol.h	Lines:	1	1	100.0 %
Date:	2021-08-16	Branches:	0	0	0.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Ying Sheng, Abdalrhman Mohamed
 *
 * 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 interpolation utility, which transforms an input of axioms and
 * conjecture into an interpolation problem, and solve it.
 */

#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_INTERPOL_H
#define CVC5__THEORY__QUANTIFIERS__SYGUS_INTERPOL_H

#include <string>
#include <vector>

#include "expr/node.h"
#include "expr/type_node.h"
#include "smt/smt_engine.h"

namespace cvc5 {
namespace theory {
namespace quantifiers {
/**
 * This is an utility for the SMT-LIB command (get-interpol <term>).
 * The utility turns a set of quantifier-free assertions into a sygus
 * conjecture that encodes an interpolation problem, and then solve the
 * interpolation problem by synthesizing it. In detail, if our input formula is
 * F( x ) for free symbol x, and is partitioned into axioms Fa and conjecture Fc
 * then the sygus conjecture we construct is:
 *
 * (Fa( x ) => A( x )) ^ (A( x ) => Fc( x ))
 *
 * where A( x ) is a predicate over the free symbols of our input that are
 * shared between Fa and Fc. In other words, A( x ) must be implied by our
 * axioms Fa( x ) and implies Fc( x ). Then, to solve the interpolation problem,
 * we just need to synthesis A( x ).
 *
 * This class uses a fresh copy of the SMT engine which is used for solving the
 * interpolation problem. In particular, consider the input: (assert A)
 *   (get-interpol s B)
 * In the copy of the SMT engine where these commands are issued, we maintain
 * A in the assertion stack. In solving the interpolation problem, we will
 * need to call a SMT engine solver with a different assertion stack, which is
 * a sygus conjecture build from A and B. Then to solve the interpolation
 * problem, instead of modifying the assertion stack to remove A and add the
 * sygus conjecture (exists I. ...), we invoke a fresh copy of the SMT engine
 * and leave the original assertion stack unchanged. This copy of the SMT
 * engine will have the assertion stack with the sygus conjecture. This copy
 * of the SMT engine can be further queried for information regarding further
 * solutions.
 */
class SygusInterpol
{
 public:
  SygusInterpol();

  /**
   * Returns the sygus conjecture in interpol corresponding to the interpolation
   * problem for input problem (F above) given by axioms (Fa above), and conj
   * (Fc above). And solve the interpolation by sygus. Note that axioms is
   * expected to be a subset of assertions in SMT-LIB.
   *
   * @param name the name for the interpol-to-synthesize.
   * @param axioms the assertions (Fa above)
   * @param conj the conjecture (Fc above)
   * @param itpGType (if non-null) a sygus datatype type that encodes the
   * grammar that should be used for solutions of the interpolation conjecture.
   * @interpol the solution to the sygus conjecture.
   */
  bool solveInterpolation(const std::string& name,
                          const std::vector<Node>& axioms,
                          const Node& conj,
                          const TypeNode& itpGType,
                          Node& interpol);

 private:
  /**
   * Collects symbols from axioms (axioms) and conjecture (conj), which are
   * stored in d_syms, and computes the shared symbols between axioms and
   * conjecture, stored in d_symSetShared.
   *
   * @param axioms the assertions (Fa above)
   * @param conj the conjecture (Fc above)
   */
  void collectSymbols(const std::vector<Node>& axioms, const Node& conj);

  /**
   * Creates free variables and shared free variables from d_syms and
   * d_symSetShared, which are stored in d_vars and d_varsShared. And also
   * creates the corresponding set of variables for the formal argument list,
   * which is stored in d_vlvs and d_vlvsShared. Extracts the types of shared
   * variables, which are stored in d_varTypesShared. Creates the formal
   * argument list of the interpol-to-synthese, stored in d_ibvlShared.
   *
   * When using default grammar, the needsShared is true. When using
   * user-defined gramar, the needsShared is false.
   *
   * @param needsShared If it is true, the argument list of the
   * interpol-to-synthesis will be restricted to be over shared variables. If it
   * is false, the argument list will be over all the variables.
   */
  void createVariables(bool needsShared);

  /**
   * Get include_cons for mkSygusDefaultType.
   * mkSygusDefaultType() is a function to make default grammar. It has an
   * arguemnt include_cons, which will restrict what operators we want in the
   * grammar. The return value depends on options::produceInterpols(). In
   * ASSUMPTIONS option, it will return the operators from axioms. In CONJECTURE
   * option, it will return the operators from conj. In SHARED option, it will
   * return the oprators shared by axioms and conj. In ALL option, it will
   * return the operators from either axioms or conj.
   *
   * @param axioms input argument
   * @param conj input argument
   * @param result the return value
   */
  void getIncludeCons(const std::vector<Node>& axioms,
                      const Node& conj,
                      std::map<TypeNode, std::unordered_set<Node>>& result);

  /**
   * Set up the grammar for the interpol-to-synthesis.
   *
   * The user-defined grammar will be encoded by itpGType. The options for
   * grammar is given by options::produceInterpols(). In DEFAULT option, it will
   * set up the grammar from itpGType. And if itpGType is null, it will set up
   * the default grammar, which is built according to a policy handled by
   * getIncludeCons().
   *
   * @param itpGType (if non-null) a sygus datatype type that encodes the
   * grammar that should be used for solutions of the interpolation conjecture.
   * @param axioms the assertions (Fa above)
   * @param conj the conjecture (Fc above)
   */
  TypeNode setSynthGrammar(const TypeNode& itpGType,
                           const std::vector<Node>& axioms,
                           const Node& conj);

  /**
   * Make the interpolation predicate.
   *
   * @param name the name of the interpol-to-synthesis.
   */
  Node mkPredicate(const std::string& name);

  /**
   * Make the sygus conjecture to be synthesis.
   * The conjecture body is Fa( x ) => A( x ) ^ A( x ) => Fc( x ) as described
   * above.
   *
   * @param itp the interpolation predicate.
   * @param axioms the assertions (Fa above)
   * @param conj the conjecture (Fc above)
   */
  void mkSygusConjecture(Node itp,
                         const std::vector<Node>& axioms,
                         const Node& conj);

  /**
   * Get the synthesis solution, stored in interpol.
   *
   * @param interpol the solution to the sygus conjecture.
   * @param itp the interpolation predicate.
   */
  bool findInterpol(SmtEngine* subsolver, Node& interpol, Node itp);

  /**
   * symbols from axioms and conjecture.
   */
  std::vector<Node> d_syms;
  /**
   * unordered set for shared symbols between axioms and conjecture.
   */
  std::unordered_set<Node> d_symSetShared;
  /**
   * free variables created from d_syms.
   */
  std::vector<Node> d_vars;
  /**
   * variables created from d_syms for formal argument list.
   */
  std::vector<Node> d_vlvs;
  /**
   * free variables created from d_symSetShared.
   */
  std::vector<Node> d_varsShared;
  /**
   * variables created from d_symShared for formal argument list.
   */
  std::vector<Node> d_vlvsShared;
  /**
   * types of shared variables between axioms and conjecture.
   */
  std::vector<TypeNode> d_varTypesShared;
  /**
   * formal argument list of the interpol-to-synthesis.
   */
  Node d_ibvlShared;

  /**
   * the sygus conjecture to synthesis for interpolation problem
   */
  Node d_sygusConj;
};

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

#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_INTERPOL_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Ying Sheng, Abdalrhman Mohamed
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 interpolation utility, which transforms an input of axioms and
14		* conjecture into an interpolation problem, and solve it.
15		*/
16
17		#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_INTERPOL_H
18		#define CVC5__THEORY__QUANTIFIERS__SYGUS_INTERPOL_H
19
20		#include <string>
21		#include <vector>
22
23		#include "expr/node.h"
24		#include "expr/type_node.h"
25		#include "smt/smt_engine.h"
26
27		namespace cvc5 {
28		namespace theory {
29		namespace quantifiers {
30		/**
31		* This is an utility for the SMT-LIB command (get-interpol <term>).
32		* The utility turns a set of quantifier-free assertions into a sygus
33		* conjecture that encodes an interpolation problem, and then solve the
34		* interpolation problem by synthesizing it. In detail, if our input formula is
35		* F( x ) for free symbol x, and is partitioned into axioms Fa and conjecture Fc
36		* then the sygus conjecture we construct is:
37		*
38		* (Fa( x ) => A( x )) ^ (A( x ) => Fc( x ))
39		*
40		* where A( x ) is a predicate over the free symbols of our input that are
41		* shared between Fa and Fc. In other words, A( x ) must be implied by our
42		* axioms Fa( x ) and implies Fc( x ). Then, to solve the interpolation problem,
43		* we just need to synthesis A( x ).
44		*
45		* This class uses a fresh copy of the SMT engine which is used for solving the
46		* interpolation problem. In particular, consider the input: (assert A)
47		* (get-interpol s B)
48		* In the copy of the SMT engine where these commands are issued, we maintain
49		* A in the assertion stack. In solving the interpolation problem, we will
50		* need to call a SMT engine solver with a different assertion stack, which is
51		* a sygus conjecture build from A and B. Then to solve the interpolation
52		* problem, instead of modifying the assertion stack to remove A and add the
53		* sygus conjecture (exists I. ...), we invoke a fresh copy of the SMT engine
54		* and leave the original assertion stack unchanged. This copy of the SMT
55		* engine will have the assertion stack with the sygus conjecture. This copy
56		* of the SMT engine can be further queried for information regarding further
57		* solutions.
58		*/
59	10	class SygusInterpol
60		{
61		public:
62		SygusInterpol();
63
64		/**
65		* Returns the sygus conjecture in interpol corresponding to the interpolation
66		* problem for input problem (F above) given by axioms (Fa above), and conj
67		* (Fc above). And solve the interpolation by sygus. Note that axioms is
68		* expected to be a subset of assertions in SMT-LIB.
69		*
70		* @param name the name for the interpol-to-synthesize.
71		* @param axioms the assertions (Fa above)
72		* @param conj the conjecture (Fc above)
73		* @param itpGType (if non-null) a sygus datatype type that encodes the
74		* grammar that should be used for solutions of the interpolation conjecture.
75		* @interpol the solution to the sygus conjecture.
76		*/
77		bool solveInterpolation(const std::string& name,
78		const std::vector<Node>& axioms,
79		const Node& conj,
80		const TypeNode& itpGType,
81		Node& interpol);
82
83		private:
84		/**
85		* Collects symbols from axioms (axioms) and conjecture (conj), which are
86		* stored in d_syms, and computes the shared symbols between axioms and
87		* conjecture, stored in d_symSetShared.
88		*
89		* @param axioms the assertions (Fa above)
90		* @param conj the conjecture (Fc above)
91		*/
92		void collectSymbols(const std::vector<Node>& axioms, const Node& conj);
93
94		/**
95		* Creates free variables and shared free variables from d_syms and
96		* d_symSetShared, which are stored in d_vars and d_varsShared. And also
97		* creates the corresponding set of variables for the formal argument list,
98		* which is stored in d_vlvs and d_vlvsShared. Extracts the types of shared
99		* variables, which are stored in d_varTypesShared. Creates the formal
100		* argument list of the interpol-to-synthese, stored in d_ibvlShared.
101		*
102		* When using default grammar, the needsShared is true. When using
103		* user-defined gramar, the needsShared is false.
104		*
105		* @param needsShared If it is true, the argument list of the
106		* interpol-to-synthesis will be restricted to be over shared variables. If it
107		* is false, the argument list will be over all the variables.
108		*/
109		void createVariables(bool needsShared);
110
111		/**
112		* Get include_cons for mkSygusDefaultType.
113		* mkSygusDefaultType() is a function to make default grammar. It has an
114		* arguemnt include_cons, which will restrict what operators we want in the
115		* grammar. The return value depends on options::produceInterpols(). In
116		* ASSUMPTIONS option, it will return the operators from axioms. In CONJECTURE
117		* option, it will return the operators from conj. In SHARED option, it will
118		* return the oprators shared by axioms and conj. In ALL option, it will
119		* return the operators from either axioms or conj.
120		*
121		* @param axioms input argument
122		* @param conj input argument
123		* @param result the return value
124		*/
125		void getIncludeCons(const std::vector<Node>& axioms,
126		const Node& conj,
127		std::map<TypeNode, std::unordered_set<Node>>& result);
128
129		/**
130		* Set up the grammar for the interpol-to-synthesis.
131		*
132		* The user-defined grammar will be encoded by itpGType. The options for
133		* grammar is given by options::produceInterpols(). In DEFAULT option, it will
134		* set up the grammar from itpGType. And if itpGType is null, it will set up
135		* the default grammar, which is built according to a policy handled by
136		* getIncludeCons().
137		*
138		* @param itpGType (if non-null) a sygus datatype type that encodes the
139		* grammar that should be used for solutions of the interpolation conjecture.
140		* @param axioms the assertions (Fa above)
141		* @param conj the conjecture (Fc above)
142		*/
143		TypeNode setSynthGrammar(const TypeNode& itpGType,
144		const std::vector<Node>& axioms,
145		const Node& conj);
146
147		/**
148		* Make the interpolation predicate.
149		*
150		* @param name the name of the interpol-to-synthesis.
151		*/
152		Node mkPredicate(const std::string& name);
153
154		/**
155		* Make the sygus conjecture to be synthesis.
156		* The conjecture body is Fa( x ) => A( x ) ^ A( x ) => Fc( x ) as described
157		* above.
158		*
159		* @param itp the interpolation predicate.
160		* @param axioms the assertions (Fa above)
161		* @param conj the conjecture (Fc above)
162		*/
163		void mkSygusConjecture(Node itp,
164		const std::vector<Node>& axioms,
165		const Node& conj);
166
167		/**
168		* Get the synthesis solution, stored in interpol.
169		*
170		* @param interpol the solution to the sygus conjecture.
171		* @param itp the interpolation predicate.
172		*/
173		bool findInterpol(SmtEngine* subsolver, Node& interpol, Node itp);
174
175		/**
176		* symbols from axioms and conjecture.
177		*/
178		std::vector<Node> d_syms;
179		/**
180		* unordered set for shared symbols between axioms and conjecture.
181		*/
182		std::unordered_set<Node> d_symSetShared;
183		/**
184		* free variables created from d_syms.
185		*/
186		std::vector<Node> d_vars;
187		/**
188		* variables created from d_syms for formal argument list.
189		*/
190		std::vector<Node> d_vlvs;
191		/**
192		* free variables created from d_symSetShared.
193		*/
194		std::vector<Node> d_varsShared;
195		/**
196		* variables created from d_symShared for formal argument list.
197		*/
198		std::vector<Node> d_vlvsShared;
199		/**
200		* types of shared variables between axioms and conjecture.
201		*/
202		std::vector<TypeNode> d_varTypesShared;
203		/**
204		* formal argument list of the interpol-to-synthesis.
205		*/
206		Node d_ibvlShared;
207
208		/**
209		* the sygus conjecture to synthesis for interpolation problem
210		*/
211		Node d_sygusConj;
212		};
213
214		} // namespace quantifiers
215		} // namespace theory
216		} // namespace cvc5
217
218		#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_INTERPOL_H */