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
|
/********************* */
/*! \file quantifiers_rewriter.h
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds, Morgan Deters, Tim King
** This file is part of the CVC4 project.
** Copyright (c) 2009-2018 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 Rewriter for the theory of inductive quantifiers
**
** Rewriter for the theory of inductive quantifiers.
**/
#include "cvc4_private.h"
#ifndef __CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H
#define __CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H
#include "theory/rewriter.h"
#include "theory/quantifiers_engine.h"
namespace CVC4 {
namespace theory {
namespace quantifiers {
struct QAttributes;
class QuantifiersRewriter {
private:
static int getPurifyIdLit2( Node n, std::map< Node, int >& visited );
public:
static bool isClause( Node n );
static bool isLiteral( Node n );
static bool isCube( Node n );
private:
static bool addCheckElimChild( std::vector< Node >& children, Node c, Kind k, std::map< Node, bool >& lit_pol, bool& childrenChanged );
static void addNodeToOrBuilder( Node n, NodeBuilder<>& t );
static void computeArgs( std::vector< Node >& args, std::map< Node, bool >& activeMap, Node n, std::map< Node, bool >& visited );
static void computeArgVec( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n );
static void computeArgVec2( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n, Node ipl );
static Node computeProcessTerms2( Node body, bool hasPol, bool pol, std::map< Node, bool >& currCond, int nCurrCond,
std::map< Node, Node >& cache, std::map< Node, Node >& icache,
std::vector< Node >& new_vars, std::vector< Node >& new_conds, bool elimExtArith );
static void computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons, std::vector< Node >& conj );
static bool isConditionalVariableElim( Node n, int pol=0 );
static bool isVariableElim( Node v, Node s );
static void isVariableBoundElig( Node n, std::map< Node, int >& exclude, std::map< Node, std::map< int, bool > >& visited, bool hasPol, bool pol,
std::map< Node, bool >& elig_vars );
static bool computeVariableElimLit( Node n, bool pol, std::vector< Node >& args, std::vector< Node >& var, std::vector< Node >& subs,
std::map< Node, std::map< bool, std::map< Node, bool > > >& num_bounds );
static Node computeVarElimination2( Node body, std::vector< Node >& args, QAttributes& qa );
/** variable eliminate for bit-vector literals
*
* If this returns a non-null value ret, then var is updated to a member of
* args, and lit is equivalent to ( var = ret ).
*/
static Node computeVariableElimLitBv(Node lit,
std::vector<Node>& args,
Node& var);
public:
static Node computeElimSymbols( Node body );
static Node computeMiniscoping( std::vector< Node >& args, Node body, QAttributes& qa );
static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body );
//cache is dependent upon currCond, icache is not, new_conds are negated conditions
static Node computeProcessTerms( Node body, std::vector< Node >& new_vars, std::vector< Node >& new_conds, Node q, QAttributes& qa );
static Node computeCondSplit( Node body, QAttributes& qa );
static Node computePrenex( Node body, std::vector< Node >& args, std::vector< Node >& nargs, bool pol, bool prenexAgg );
static Node computePrenexAgg( Node n, bool topLevel, std::map< unsigned, std::map< Node, Node > >& visited );
static Node computeSplit( std::vector< Node >& args, Node body, QAttributes& qa );
static Node computeVarElimination( Node body, std::vector< Node >& args, QAttributes& qa );
private:
enum{
COMPUTE_ELIM_SYMBOLS = 0,
COMPUTE_MINISCOPING,
COMPUTE_AGGRESSIVE_MINISCOPING,
COMPUTE_PROCESS_TERMS,
COMPUTE_PRENEX,
COMPUTE_VAR_ELIMINATION,
COMPUTE_COND_SPLIT,
//COMPUTE_FLATTEN_ARGS_UF,
//COMPUTE_CNF,
COMPUTE_LAST
};
static Node computeOperation( Node f, int computeOption, QAttributes& qa );
public:
static RewriteResponse preRewrite(TNode in);
static RewriteResponse postRewrite(TNode in);
static inline void init() {}
static inline void shutdown() {}
private:
/** options */
static bool doOperation( Node f, int computeOption, QAttributes& qa );
private:
static Node preSkolemizeQuantifiers(Node n, bool polarity, std::vector< TypeNode >& fvTypes, std::vector<TNode>& fvs);
public:
static Node rewriteRewriteRule( Node r );
static bool containsQuantifiers( Node n );
static bool isPrenexNormalForm( Node n );
/** preprocess
*
* This returns the result of applying simple quantifiers-specific
* preprocessing to n, including but not limited to:
* - rewrite rule elimination,
* - pre-skolemization,
* - aggressive prenexing.
* The argument isInst is set to true if n is an instance of a previously
* registered quantified formula. If this flag is true, we do not apply
* certain steps like pre-skolemization since we know they will have no
* effect.
*/
static Node preprocess( Node n, bool isInst = false );
static Node mkForAll( std::vector< Node >& args, Node body, QAttributes& qa );
static Node mkForall( std::vector< Node >& args, Node body, bool marked = false );
static Node mkForall( std::vector< Node >& args, Node body, std::vector< Node >& iplc, bool marked = false );
};/* class QuantifiersRewriter */
}/* CVC4::theory::quantifiers namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
#endif /* __CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H */
|
