Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/sygus/sygus_interpol.h	Lines:	1	1	100.0 %
Date:	2021-09-10	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/env_obj.h"

namespace cvc5 {

class Env;
class SmtEngine;

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 : protected EnvObj
{
 public:
  SygusInterpol(Env& env);

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