1 /********************* */
2 /*! \file abstraction.h
4 ** Original author: Liana Hadarean
5 ** Major contributors: none
6 ** Minor contributors (to current version): Morgan Deters
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2014 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief Bitvector theory.
18 #ifndef __CVC4__THEORY__BV__ABSTRACTION_H
19 #define __CVC4__THEORY__BV__ABSTRACTION_H
21 #include "cvc4_private.h"
22 #include <ext/hash_map>
23 #include <ext/hash_set>
24 #include "expr/node.h"
25 #include "theory/substitutions.h"
26 #include "util/statistics_registry.h"
33 typedef std::vector
<TNode
> ArgsVec
;
35 class AbstractionModule
{
38 IntStat d_numFunctionsAbstracted
;
39 IntStat d_numArgsSkolemized
;
40 TimerStat d_abstractionTime
;
46 class ArgsTableEntry
{
47 std::vector
<ArgsVec
> d_data
;
50 ArgsTableEntry(unsigned n
)
56 void addArguments(const ArgsVec
& args
);
57 typedef std::vector
<ArgsVec
>::iterator iterator
;
59 iterator
begin() { return d_data
.begin(); }
60 iterator
end() { return d_data
.end(); }
61 unsigned getArity() { return d_arity
; }
62 unsigned getNumEntries() { return d_data
.size(); }
63 ArgsVec
& getEntry(unsigned i
) { Assert (i
< d_data
.size()); return d_data
[i
]; }
67 __gnu_cxx::hash_map
<TNode
, ArgsTableEntry
, TNodeHashFunction
> d_data
;
68 bool hasEntry(TNode signature
) const;
70 typedef __gnu_cxx::hash_map
<TNode
, ArgsTableEntry
, TNodeHashFunction
>::iterator iterator
;
72 void addEntry(TNode signature
, const ArgsVec
& args
);
73 ArgsTableEntry
& getEntry(TNode signature
);
74 iterator
begin() { return d_data
.begin(); }
75 iterator
end() { return d_data
.end(); }
79 * Checks if one pattern is a generalization of the other
84 * @return 1 if s :> t, 2 if s <: t, 0 if they equivalent and -1 if they are incomparable
86 static int comparePatterns(TNode s
, TNode t
);
88 class LemmaInstantiatior
{
89 std::vector
<TNode
> d_functions
;
90 std::vector
<int> d_maxMatch
;
91 ArgsTable
& d_argsTable
;
92 context::Context
* d_ctx
;
93 theory::SubstitutionMap d_subst
;
95 std::vector
<Node
> d_lemmas
;
97 void backtrack(std::vector
<int>& stack
);
98 int next(int val
, int index
);
99 bool isConsistent(const std::vector
<int>& stack
);
100 bool accept(const std::vector
<int>& stack
);
103 LemmaInstantiatior(const std::vector
<TNode
>& functions
, ArgsTable
& table
, TNode conflict
)
104 : d_functions(functions
)
106 , d_ctx(new context::Context())
108 , d_conflict(conflict
)
111 Debug("bv-abstraction-gen") << "LemmaInstantiator conflict:" << conflict
<< "\n";
112 // initializing the search space
113 for (unsigned i
= 0; i
< functions
.size(); ++i
) {
114 TNode func_op
= functions
[i
].getOperator();
115 // number of matches for this function
116 unsigned maxCount
= table
.getEntry(func_op
).getNumEntries();
117 d_maxMatch
.push_back(maxCount
);
121 void generateInstantiations(std::vector
<Node
>& lemmas
);
125 typedef __gnu_cxx::hash_map
<Node
, std::vector
<Node
>, NodeHashFunction
> NodeVecMap
;
126 typedef __gnu_cxx::hash_map
<Node
, TNode
, NodeHashFunction
> NodeTNodeMap
;
127 typedef __gnu_cxx::hash_map
<TNode
, TNode
, TNodeHashFunction
> TNodeTNodeMap
;
128 typedef __gnu_cxx::hash_map
<Node
, Node
, NodeHashFunction
> NodeNodeMap
;
129 typedef __gnu_cxx::hash_map
<Node
, TNode
, NodeHashFunction
> TNodeNodeMap
;
130 typedef __gnu_cxx::hash_set
<TNode
, TNodeHashFunction
> TNodeSet
;
131 typedef __gnu_cxx::hash_map
<unsigned, Node
> IntNodeMap
;
132 typedef __gnu_cxx::hash_map
<unsigned, unsigned> IndexMap
;
133 typedef __gnu_cxx::hash_map
<unsigned, std::vector
<Node
> > SkolemMap
;
134 typedef __gnu_cxx::hash_map
<TNode
, unsigned, TNodeHashFunction
> SignatureMap
;
136 ArgsTable d_argsTable
;
138 // mapping between signature and uninterpreted function symbol used to
139 // abstract the signature
140 NodeNodeMap d_signatureToFunc
;
141 NodeNodeMap d_funcToSignature
;
143 NodeNodeMap d_assertionToSignature
;
144 SignatureMap d_signatures
;
145 NodeNodeMap d_sigToGeneralization
;
149 IndexMap d_signatureIndices
;
150 SkolemMap d_signatureSkolems
;
152 void collectArgumentTypes(TNode sig
, std::vector
<TypeNode
>& types
, TNodeSet
& seen
);
153 void collectArguments(TNode node
, TNode sig
, std::vector
<Node
>& args
, TNodeSet
& seen
);
154 void finalizeSignatures();
155 Node
abstractSignatures(TNode assertion
);
156 Node
computeSignature(TNode node
);
158 bool isConjunctionOfAtoms(TNode node
);
159 bool isConjunctionOfAtomsRec(TNode node
, TNodeSet
& seen
);
161 TNode
getGeneralization(TNode term
);
162 void storeGeneralization(TNode s
, TNode t
);
164 // signature skolem stuff
165 Node
getGeneralizedSignature(Node node
);
166 Node
getSignatureSkolem(TNode node
);
168 unsigned getBitwidthIndex(unsigned bitwidth
);
169 void resetSignatureIndex();
170 Node
computeSignatureRec(TNode
, NodeNodeMap
&);
171 void storeSignature(Node signature
, TNode assertion
);
172 bool hasSignature(Node node
);
174 Node
substituteArguments(TNode signature
, TNode apply
, unsigned& i
, TNodeTNodeMap
& seen
);
176 // crazy instantiation methods
177 void generateInstantiations(unsigned current
,
178 std::vector
<ArgsTableEntry
>& matches
,
179 std::vector
<std::vector
<ArgsVec
> >& instantiations
,
180 std::vector
<std::vector
<ArgsVec
> >& new_instantiations
);
182 Node
tryMatching(const std::vector
<Node
>& ss
, const std::vector
<TNode
>& tt
, TNode conflict
);
183 void makeFreshArgs(TNode func
, std::vector
<Node
>& fresh_args
);
184 void makeFreshSkolems(TNode node
, SubstitutionMap
& map
, SubstitutionMap
& reverse_map
);
186 void skolemizeArguments(std::vector
<Node
>& assertions
);
187 Node
reverseAbstraction(Node assertion
, NodeNodeMap
& seen
);
189 TNodeSet d_addedLemmas
;
190 TNodeSet d_lemmaAtoms
;
191 TNodeSet d_inputAtoms
;
192 void storeLemma(TNode lemma
);
194 Statistics d_statistics
;
199 , d_signatureToFunc()
200 , d_funcToSignature()
201 , d_assertionToSignature()
203 , d_sigToGeneralization()
205 , d_signatureIndices()
206 , d_signatureSkolems()
213 * returns true if there are new uninterepreted functions symbols in the output
216 * @param new_assertions
220 bool applyAbstraction(const std::vector
<Node
>& assertions
, std::vector
<Node
>& new_assertions
);
222 * Returns true if the node represents an abstraction predicate.
228 bool isAbstraction(TNode node
);
230 * Returns the interpretation of the abstraction predicate.
236 Node
getInterpretation(TNode node
);
237 Node
simplifyConflict(TNode conflict
);
238 void generalizeConflict(TNode conflict
, std::vector
<Node
>& lemmas
);
239 void addInputAtom(TNode atom
);
240 bool isLemmaAtom(TNode node
) const;