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
|
/********************* */
/*! \file ce_guided_single_inv.h
** \verbatim
** Original author: Andrew Reynolds
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 project.
** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
** \brief utility for processing single invocation synthesis conjectures
**/
#include "cvc4_private.h"
#ifndef __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_H
#define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_H
#include "context/cdhashmap.h"
#include "context/cdchunk_list.h"
#include "theory/quantifiers_engine.h"
#include "theory/quantifiers/ce_guided_single_inv_sol.h"
#include "theory/quantifiers/inst_strategy_cbqi.h"
namespace CVC4 {
namespace theory {
namespace quantifiers {
class CegConjecture;
class CegConjectureSingleInv;
class CegqiOutputSingleInv : public CegqiOutput
{
public:
CegqiOutputSingleInv( CegConjectureSingleInv * out ) : d_out( out ){}
~CegqiOutputSingleInv() {}
CegConjectureSingleInv * d_out;
bool addInstantiation( std::vector< Node >& subs );
bool isEligibleForInstantiation( Node n );
bool addLemma( Node lem );
};
class CegConjectureSingleInv
{
friend class CegqiOutputSingleInv;
private:
QuantifiersEngine * d_qe;
CegConjecture * d_parent;
CegConjectureSingleInvSol * d_sol;
//the instantiator
CegInstantiator * d_cinst;
//for recognizing when conjecture is single invocation
bool analyzeSygusConjunct( Node n, Node p, std::map< Node, std::vector< Node > >& children,
std::map< Node, std::map< Node, std::vector< Node > > >& prog_invoke,
std::vector< Node >& progs, std::map< Node, std::map< Node, bool > >& contains, bool pol );
bool analyzeSygusTerm( Node n, std::map< Node, std::vector< Node > >& prog_invoke, std::map< Node, bool >& contains );
bool processSingleInvLiteral( Node lit, bool pol, std::map< Node, std::vector< Node > >& case_vals );
bool doVariableElimination( Node v, std::vector< Node >& conjuncts );
bool getVariableEliminationTerm( bool pol, bool active, Node v, Node n, TNode& s, int& status );
//for recognizing templates for invariant synthesis
int extractInvariantPolarity( Node n, Node inv, std::vector< Node >& curr_disj, bool pol );
Node substituteInvariantTemplates( Node n, std::map< Node, Node >& prog_templ, std::map< Node, std::vector< Node > >& prog_templ_vars );
//presolve
void collectPresolveEqTerms( Node n, std::map< Node, std::vector< Node > >& teq );
void getPresolveEqConjuncts( std::vector< Node >& vars, std::vector< Node >& terms, std::map< Node, std::vector< Node > >& teq, Node n, std::vector< Node >& conj );
//constructing solution
Node constructSolution( std::vector< unsigned >& indices, unsigned i, unsigned index );
private:
//map from programs to variables in single invocation property
std::map< Node, Node > d_single_inv_map;
std::map< Node, Node > d_single_inv_map_to_prog;
//map from programs to evaluator term representing the above variable
std::map< Node, Node > d_single_inv_app_map;
//list of skolems for each argument of programs
std::vector< Node > d_single_inv_arg_sk;
//list of skolems for each program
std::vector< Node > d_single_inv_sk;
std::map< Node, int > d_single_inv_sk_index;
//list of skolems for each program
std::vector< Node > d_single_inv_var;
//lemmas produced
inst::InstMatchTrie d_inst_match_trie;
inst::CDInstMatchTrie * d_c_inst_match_trie;
// solution
std::vector< Node > d_varList;
Node d_orig_solution;
Node d_solution;
Node d_sygus_solution;
bool d_has_ites;
public:
//lemmas produced
std::vector< Node > d_lemmas_produced;
std::vector< std::vector< Node > > d_inst;
private:
std::vector< Node > d_curr_lemmas;
//add instantiation
bool addInstantiation( std::vector< Node >& subs );
//is eligible for instantiation
bool isEligibleForInstantiation( Node n );
// add lemma
bool addLemma( Node lem );
public:
CegConjectureSingleInv( QuantifiersEngine * qe, CegConjecture * p );
// original conjecture
Node d_quant;
// single invocation version of quant
Node d_single_inv;
// transition relation version per program
std::map< Node, Node > d_trans_pre;
std::map< Node, Node > d_trans_post;
std::map< Node, std::vector< Node > > d_prog_templ_vars;
public:
//get the single invocation lemma(s)
void getSingleInvLemma( Node guard, std::vector< Node >& lems );
//initialize
void initialize( Node q );
//check
void check( std::vector< Node >& lems );
//get solution
Node getSolution( unsigned sol_index, TypeNode stn, int& reconstructed );
//reconstruct to syntax
Node reconstructToSyntax( Node s, TypeNode stn, int& reconstructed );
// has ites
bool hasITEs() { return d_has_ites; }
// is single invocation
bool isSingleInvocation() { return !d_single_inv.isNull(); }
//needs check
bool needsCheck();
};
}
}
}
#endif
|
