blob: be35025bdb2e66e4d06badfafcbfafbe03bef1af (
plain)
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
|
/********************* */
/*! \file template_infer.h
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 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.\endverbatim
**
** \brief utility for inferring templates for invariant problems
**/
#include "cvc4_private.h"
#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS__TEMPLATE_INFER_H
#define CVC4__THEORY__QUANTIFIERS__SYGUS__TEMPLATE_INFER_H
#include <map>
#include "expr/node.h"
#include "theory/quantifiers/sygus/transition_inference.h"
namespace CVC5 {
namespace theory {
namespace quantifiers {
/**
* This class infers templates for an invariant-to-synthesize based on the
* template mode. It uses the transition inference to choose a template.
*/
class SygusTemplateInfer
{
public:
SygusTemplateInfer() {}
~SygusTemplateInfer() {}
/**
* Initialize this class for synthesis conjecture q. If applicable, the
* templates for functions-to-synthesize for q are accessible by the
* calls below afterwards.
*/
void initialize(Node q);
/**
* Get template for program prog. This returns a term of the form t[x] where
* x is the template argument (see below)
*/
Node getTemplate(Node prog) const;
/**
* Get the template argument for program prog. This is a variable which
* indicates the position of the function/predicate to synthesize.
*/
Node getTemplateArg(Node prog) const;
private:
/** The quantified formula we initialized with */
Node d_quant;
/** transition relation pre and post version per function to synthesize */
std::map<Node, Node> d_trans_pre;
std::map<Node, Node> d_trans_post;
/** the template for each function to synthesize */
std::map<Node, Node> d_templ;
/**
* The template argument for each function to synthesize (occurs in exactly
* one position of its template)
*/
std::map<Node, Node> d_templ_arg;
/** transition inference module */
TransitionInference d_ti;
};
} // namespace quantifiers
} // namespace theory
} // namespace CVC5
#endif
|
