GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus/ce_guided_single_inv.h Lines: 2 2 100.0 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file ce_guided_single_inv.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Tim King, Mathias Preiner
6
 ** This file is part of the CVC4 project.
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.\endverbatim
11
 **
12
 ** \brief utility for processing single invocation synthesis conjectures
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_H
18
#define CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_H
19
20
#include "context/cdlist.h"
21
#include "expr/subs.h"
22
#include "theory/quantifiers/cegqi/inst_strategy_cegqi.h"
23
#include "theory/quantifiers/inst_match_trie.h"
24
#include "theory/quantifiers/single_inv_partition.h"
25
#include "theory/quantifiers/sygus/ce_guided_single_inv_sol.h"
26
27
namespace CVC4 {
28
namespace theory {
29
namespace quantifiers {
30
31
class SynthConjecture;
32
33
// this class infers whether a conjecture is single invocation (Reynolds et al CAV 2015), and sets up the
34
// counterexample-guided quantifier instantiation utility (d_cinst), and methods for solution
35
// reconstruction (d_sol).
36
// It also has more advanced techniques for:
37
// (1) partitioning a conjecture into single invocation / non-single invocation portions for invariant synthesis,
38
// (2) inferring whether the conjecture corresponds to a deterministic transistion system (by utility d_ti).
39
// For these techniques, we may generate a template (d_templ) which specifies a restricted
40
// solution space. We may in turn embed this template as a SyGuS grammar.
41
class CegSingleInv
42
{
43
 private:
44
  //presolve
45
  void collectPresolveEqTerms( Node n,
46
                               std::map< Node, std::vector< Node > >& teq );
47
  void getPresolveEqConjuncts( std::vector< Node >& vars,
48
                               std::vector< Node >& terms,
49
                               std::map< Node, std::vector< Node > >& teq,
50
                               Node n, std::vector< Node >& conj );
51
 private:
52
  /** pointer to the quantifiers engine */
53
  QuantifiersEngine* d_qe;
54
  // single invocation inference utility
55
  SingleInvocationPartition* d_sip;
56
  // solution reconstruction
57
  CegSingleInvSol* d_sol;
58
59
  // list of skolems for each argument of programs
60
  std::vector<Node> d_single_inv_arg_sk;
61
  // program to solution index
62
  std::map<Node, unsigned> d_prog_to_sol_index;
63
  // original conjecture
64
  Node d_orig_conjecture;
65
66
 public:
67
  //---------------------------------representation of the solution
68
  /**
69
   * The list of instantiations that suffice to show the first-order equivalent
70
   * of the negated synthesis conjecture is unsatisfiable.
71
   */
72
  std::vector<std::vector<Node> > d_inst;
73
  /**
74
   * The list of instantiation lemmas, corresponding to instantiations of the
75
   * first order conjecture for the term vectors above.
76
   */
77
  std::vector<Node> d_instConds;
78
  /** The solutions, without reconstruction to syntax */
79
  std::vector<Node> d_solutions;
80
  /** The solutions, after reconstruction to syntax */
81
  std::vector<Node> d_rcSolutions;
82
  /** is solved */
83
  bool d_isSolved;
84
  //---------------------------------end representation of the solution
85
86
 private:
87
  Node d_simp_quant;
88
  // are we single invocation?
89
  bool d_single_invocation;
90
  // single invocation portion of quantified formula
91
  Node d_single_inv;
92
93
 public:
94
  CegSingleInv(QuantifiersEngine* qe);
95
  ~CegSingleInv();
96
97
  // get simplified conjecture
98
506
  Node getSimplifiedConjecture() { return d_simp_quant; }
99
  /** initialize this class for synthesis conjecture q */
100
  void initialize( Node q );
101
  /** finish initialize
102
   *
103
   * This method sets up final decisions about whether to use single invocation
104
   * techniques.
105
   *
106
   * The argument syntaxRestricted is whether the syntax for solutions for the
107
   * initialized conjecture is restricted.
108
   */
109
  void finishInit(bool syntaxRestricted);
110
  /** solve
111
   *
112
   * If single invocation techniques are being used, it solves
113
   * the first order form of the negated synthesis conjecture using a fresh
114
   * copy of the SMT engine. This method returns true if it has successfully
115
   * found a solution to the synthesis conjecture using this method.
116
   */
117
  bool solve();
118
  /**
119
   * Get solution for the sol_index^th function to synthesize of the conjecture
120
   * this class was assigned.
121
   *
122
   * @param sol_index The index of the function to synthesize
123
   * @param stn The sygus type of the solution, which corresponds to syntactic
124
   * restrictions
125
   * @param reconstructed Set to the status of reconstructing the solution,
126
   * where 1 = success, 0 = no reconstruction specified, -1 = failed
127
   * @param rconsSygus Whether to apply sygus reconstruction techniques based
128
   * on the underlying reconstruction module. If this is false, then the
129
   * solution does not necessarily fit the grammar.
130
   * @return the solution for the sol_index^th function to synthesize of the
131
   * conjecture assigned to this class.
132
   */
133
  Node getSolution(size_t sol_index,
134
                   TypeNode stn,
135
                   int& reconstructed,
136
                   bool rconsSygus = true);
137
  //reconstruct to syntax
138
  Node reconstructToSyntax( Node s, TypeNode stn, int& reconstructed,
139
                            bool rconsSygus = true );
140
  // is single invocation
141
59714
  bool isSingleInvocation() const { return !d_single_inv.isNull(); }
142
  /** preregister conjecture */
143
  void preregisterConjecture( Node q );
144
145
 private:
146
  /** solve trivial
147
   *
148
   * If this method returns true, it sets d_isSolved to true and adds
149
   * t1 ... tn to d_inst if it can be shown that (forall x1 ... xn. P) is
150
   * unsatisfiable for instantiation {x1 -> t1 ... xn -> tn}.
151
   */
152
  bool solveTrivial(Node q);
153
  /**
154
   * Get solution from the instantiations stored in this class (d_inst) for
155
   * the index^th function to synthesize. The vector d_inst should be
156
   * initialized before calling this method.
157
   */
158
  Node getSolutionFromInst(size_t index);
159
  /**
160
   * Set solution, which sets the d_solutions / d_rcSolutions fields based on
161
   * calls to the above method getSolutionFromInst.
162
   */
163
  void setSolution();
164
  /** The conjecture */
165
  Node d_quant;
166
  //-------------- decomposed conjecture
167
  /** All functions */
168
  std::vector<Node> d_funs;
169
  /** Unsolved functions */
170
  std::vector<Node> d_unsolvedf;
171
  /** Mapping of solved functions */
172
  Subs d_solvedf;
173
  //-------------- end decomposed conjecture
174
};
175
176
}/* namespace CVC4::theory::quantifiers */
177
}/* namespace CVC4::theory */
178
}/* namespace CVC4 */
179
180
#endif