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
|
/********************* */
/*! \file ce_guided_instantiation.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 counterexample guided instantiation class
**/
#include "cvc4_private.h"
#ifndef CE_GUIDED_INSTANTIATION_H
#define CE_GUIDED_INSTANTIATION_H
#include "context/cdhashmap.h"
#include "context/cdchunk_list.h"
#include "theory/quantifiers_engine.h"
namespace CVC4 {
namespace theory {
namespace quantifiers {
class CegInstantiation : public QuantifiersModule
{
typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
private:
/** collect disjuncts */
static void collectDisjuncts( Node n, std::vector< Node >& ex );
/** a synthesis conjecture */
class CegConjecture {
public:
CegConjecture( context::Context* c );
/** is conjecture active */
context::CDO< bool > d_active;
/** is conjecture infeasible */
context::CDO< bool > d_infeasible;
/** quantified formula */
Node d_quant;
/** guard */
Node d_guard;
/** base instantiation */
Node d_base_inst;
/** expand base inst to disjuncts */
std::vector< Node > d_base_disj;
/** guard split */
Node d_guard_split;
/** is syntax-guided */
bool d_syntax_guided;
/** list of constants for quantified formula */
std::vector< Node > d_candidates;
/** list of variables on inner quantification */
std::vector< Node > d_inner_vars;
std::vector< std::vector< Node > > d_inner_vars_disj;
/** list of terms we have instantiated candidates with */
std::map< int, std::vector< Node > > d_candidate_inst;
/** initialize guard */
void initializeGuard( QuantifiersEngine * qe );
/** measure term */
Node d_measure_term;
/** measure sum size */
int d_measure_term_size;
/** refine count */
unsigned d_refine_count;
/** assign */
void assign( QuantifiersEngine * qe, Node q );
/** is assigned */
bool isAssigned() { return !d_quant.isNull(); }
/** current extential quantifeirs whose couterexamples we must refine */
std::vector< std::vector< Node > > d_ce_sk;
private: //for single invocation
void analyzeSygusConjecture();
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 );
public:
Node d_single_inv;
//map from programs to variables in single invocation property
std::map< Node, Node > d_single_inv_map;
//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;
public: //for fairness
/** the cardinality literals */
std::map< int, Node > d_lits;
/** current cardinality */
context::CDO< int > d_curr_lit;
/** allocate literal */
Node getLiteral( QuantifiersEngine * qe, int i );
/** is ground */
bool isGround() { return d_inner_vars.empty(); }
};
/** the quantified formula stating the synthesis conjecture */
CegConjecture * d_conj;
private: //for enforcing fairness
/** measure functions */
std::map< TypeNode, Node > d_uf_measure;
/** register measured type */
void registerMeasuredType( TypeNode tn );
/** term -> size term */
std::map< Node, Node > d_size_term;
/** get size term */
Node getSizeTerm( Node n, TypeNode tn, std::vector< Node >& lems );
/** term x constructor -> lemma */
std::map< Node, std::map< int, Node > > d_size_term_lemma;
/** get measure lemmas */
void getMeasureLemmas( Node n, Node v, std::vector< Node >& lems );
private:
/** check conjecture */
void checkCegConjecture( CegConjecture * conj );
/** get model values */
bool getModelValues( CegConjecture * conj, std::vector< Node >& n, std::vector< Node >& v );
/** get model value */
Node getModelValue( Node n );
/** get model term */
Node getModelTerm( Node n );
private:
/** print sygus term */
void printSygusTerm( std::ostream& out, Node n );
public:
CegInstantiation( QuantifiersEngine * qe, context::Context* c );
public:
bool needsCheck( Theory::Effort e );
bool needsModel( Theory::Effort e );
bool needsFullModel( Theory::Effort e );
/* Call during quantifier engine's check */
void check( Theory::Effort e, unsigned quant_e );
/* Called for new quantifiers */
void registerQuantifier( Node q );
void assertNode( Node n );
Node getNextDecisionRequest();
/** Identify this module (for debugging, dynamic configuration, etc..) */
std::string identify() const { return "CegInstantiation"; }
/** print solution for synthesis conjectures */
void printSynthSolution( std::ostream& out );
};
}
}
}
#endif
|
