1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
|
/********************* */
/*! \file ce_guided_single_inv_sol.h
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds, Paul Meng
** This file is part of the CVC4 project.
** Copyright (c) 2009-2017 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.\endverbatim
**
** \brief utility for reconstructing solutions for single invocation synthesis conjectures
**/
#include "cvc4_private.h"
#ifndef __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_SOL_H
#define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_SOL_H
#include "context/cdhashmap.h"
#include "theory/quantifiers_engine.h"
namespace CVC4 {
namespace theory {
namespace quantifiers {
class CegConjectureSingleInv;
/** CegConjectureSingleInvSol
*
* This function implements Figure 5 of "Counterexample-Guided Quantifier
* Instantiation for Synthesis in SMT", Reynolds et al CAV 2015.
*
*/
class CegConjectureSingleInvSol
{
friend class CegConjectureSingleInv;
private:
QuantifiersEngine * d_qe;
std::vector< Node > d_varList;
std::map< Node, int > d_dterm_size;
std::map< Node, int > d_dterm_ite_size;
//solution simplification
private:
bool debugSolution( Node sol );
void debugTermSize( Node sol, int& t_size, int& num_ite );
Node pullITEs( Node n );
bool pullITECondition( Node root, Node n, std::vector< Node >& conj, Node& t, Node& rem, int depth );
Node flattenITEs( Node n, bool rec = true );
bool getAssign( bool pol, Node n, std::map< Node, bool >& assign, std::vector< Node >& new_assign,
std::vector< Node >& vars, std::vector< Node >& new_vars, std::vector< Node >& new_subs );
bool getAssignEquality( Node eq, std::vector< Node >& vars, std::vector< Node >& new_vars, std::vector< Node >& new_subs );
Node simplifySolutionNode( Node sol, TypeNode stn, std::map< Node, bool >& assign,
std::vector< Node >& vars, std::vector< Node >& subs, int status );
public:
CegConjectureSingleInvSol(QuantifiersEngine* qe);
/** simplify solution
*
* Returns the simplified version of node sol whose syntax is restricted by
* the grammar corresponding to sygus datatype stn.
*/
Node simplifySolution( Node sol, TypeNode stn );
/** reconstruct solution
*
* Returns (if possible) a node that is equivalent to sol those syntax
* matches the grammar corresponding to sygus datatype stn.
* The value reconstructed is set to 1 if we successfully return a node,
* otherwise it is set to -1.
*/
Node reconstructSolution(Node sol, TypeNode stn, int& reconstructed);
/** preregister conjecture
*
* q : the synthesis conjecture this class is for.
* This is used as a heuristic to find terms in the original conjecture which
* may be helpful for using during reconstruction.
*/
void preregisterConjecture(Node q);
private:
int d_id_count;
int d_root_id;
std::map< int, Node > d_id_node;
std::map< int, TypeNode > d_id_type;
std::map< TypeNode, std::map< Node, int > > d_rcons_to_id;
std::map< TypeNode, std::map< Node, int > > d_rcons_to_status;
std::map< int, std::map< Node, std::vector< int > > > d_reconstruct_op;
std::map< int, Node > d_reconstruct;
std::map< int, std::vector< int > > d_parents;
std::map< int, std::vector< int > > d_eqc;
std::map< int, int > d_rep;
//equivalent terms
std::map< Node, Node > d_eqt_rep;
std::map< Node, std::vector< Node > > d_eqt_eqc;
//cache when reconstructing solutions
std::vector< int > d_tmp_fail;
// get reconstructed solution
Node getReconstructedSolution( int id, bool mod_eq = true );
// allocate node with type
int allocate( Node n, TypeNode stn );
// term t with sygus type st, returns inducted templated form of t
int collectReconstructNodes( Node t, TypeNode stn, int& status );
bool collectReconstructNodes( int pid, std::vector< Node >& ts, const DatatypeConstructor& dtc, std::vector< int >& ids, int& status );
bool getPathToRoot( int id );
void setReconstructed( int id, Node n );
//get equivalent terms to n with top symbol k
void getEquivalentTerms( Kind k, Node n, std::vector< Node >& equiv );
//register equivalent terms
void registerEquivalentTerms( Node n );
/** builtin to sygus const
*
* Returns a sygus term of type tn that encodes the builtin constant c.
* If the sygus datatype tn allows any constant, this may return a variable
* with the attribute SygusPrintProxyAttribute that associates it with c.
*
* rcons_depth limits the number of recursive calls when doing accelerated
* constant reconstruction (currently limited to 1000). Notice this is hacky:
* depending upon order of calls, constant rcons may succeed, e.g. 1001, 999
* vs. 999, 1001.
*/
Node builtinToSygusConst(Node c, TypeNode tn, int rcons_depth = 0);
/** cache for the above function */
std::map<TypeNode, std::map<Node, Node> > d_builtin_const_to_sygus;
/** sorted list of constants, per type */
std::map<TypeNode, std::vector<Node> > d_const_list;
/** number of positive constants, per type */
std::map<TypeNode, unsigned> d_const_list_pos;
/** list of constructor indices whose operators are identity functions */
std::map<TypeNode, std::vector<int> > d_id_funcs;
/** initialize the above information for sygus type tn */
void registerType(TypeNode tn);
/** get generic base
*
* This returns the builtin term that is the analog of an application of the
* c^th constructor of dt to fresh variables.
*/
Node getGenericBase(TypeNode tn, const Datatype& dt, int c);
/** cache for the above function */
std::map<TypeNode, std::map<int, Node> > d_generic_base;
/** get match
*
* This function attempts to find a substitution for which p = n. If
* successful, this function returns a substitution in the form of s/new_s,
* where:
* s : substitution, where the domain are indices of terms in the sygus
* term database, and
* new_s : the members that were added to s on this call.
* Otherwise, this function returns false and s and new_s are unmodified.
*/
bool getMatch(Node p,
Node n,
std::map<int, Node>& s,
std::vector<int>& new_s);
/** get match
*
* This function attempts to find a builtin term that is analog to a value
* of the sygus datatype st that is equivalent to n. If this function returns
* true, then it has found such a term. Then we set:
* index_found : updated to the constructor index of the sygus term whose
* analog to equivalent to n.
* args : builtin terms corresponding to the match, in order.
* Otherwise, this function returns false and index_found and args are
* unmodified.
* For example, for grammar:
* A -> 0 | 1 | x | +( A, A )
* Given input ( 5 + (x+1) ) and A we would return true, where:
* index_found is set to 3 and args is set to { 5, x+1 }.
*
* index_exc : (if applicable) exclude a constructor index of st
* index_start : start index of constructors of st to try
*/
bool getMatch(Node n,
TypeNode st,
int& index_found,
std::vector<Node>& args,
int index_exc = -1,
int index_start = 0);
};
}
}
}
#endif
|
