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
|
/********************* */
/*! \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 __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_INSTANTIATION_H
#define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_INSTANTIATION_H
#include "context/cdhashmap.h"
#include "context/cdchunk_list.h"
#include "theory/quantifiers_engine.h"
#include "theory/quantifiers/ce_guided_single_inv.h"
#include "theory/quantifiers/modes.h"
namespace CVC4 {
namespace theory {
namespace quantifiers {
/** a synthesis conjecture */
class CegConjecture {
private:
QuantifiersEngine * d_qe;
public:
CegConjecture( QuantifiersEngine * qe, context::Context* c );
/** is conjecture active */
context::CDO< bool > d_active;
/** is conjecture infeasible */
context::CDO< bool > d_infeasible;
/** quantified formula asserted */
Node d_assert_quant;
/** quantified formula (after processing) */
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( 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;
/** single invocation utility */
CegConjectureSingleInv * d_ceg_si;
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(); }
/** fairness */
CegqiFairMode getCegqiFairMode();
/** is single invocation */
bool isSingleInvocation();
/** needs check */
bool needsCheck();
/** preregister conjecture */
void preregisterConjecture( Node q );
};
class CegInstantiation : public QuantifiersModule
{
typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
private:
/** the quantified formula stating the synthesis conjecture */
CegConjecture * d_conj;
/** last instantiation by single invocation module? */
bool d_last_inst_si;
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 );
public:
CegInstantiation( QuantifiersEngine * qe, context::Context* c );
public:
bool needsCheck( Theory::Effort e );
unsigned needsModel( 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 );
/** collect disjuncts */
static void collectDisjuncts( Node n, std::vector< Node >& ex );
/** preregister assertion (before rewrite) */
void preregisterAssertion( Node n );
public:
class Statistics {
public:
IntStat d_cegqi_lemmas_ce;
IntStat d_cegqi_lemmas_refine;
IntStat d_cegqi_si_lemmas;
Statistics();
~Statistics();
};/* class CegInstantiation::Statistics */
Statistics d_statistics;
};
}
}
}
#endif
|
