1 /********************* */
2 /*! \file theory_strings.h
4 ** Original author: Tianyi Liang
5 ** Major contributors: none
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2013 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 Theory of strings
17 #include "cvc4_private.h"
19 #ifndef __CVC4__THEORY__STRINGS__THEORY_STRINGS_H
20 #define __CVC4__THEORY__STRINGS__THEORY_STRINGS_H
22 #include "theory/theory.h"
23 #include "theory/uf/equality_engine.h"
24 #include "theory/strings/theory_strings_preprocess.h"
25 #include "theory/strings/regexp_operation.h"
27 #include "context/cdchunk_list.h"
28 #include "context/cdhashset.h"
35 * Decision procedure for strings.
39 class TheoryStrings
: public Theory
{
40 typedef context::CDChunkList
<Node
> NodeList
;
41 typedef context::CDHashMap
<Node
, NodeList
*, NodeHashFunction
> NodeListMap
;
42 typedef context::CDHashMap
<Node
, bool, NodeHashFunction
> NodeBoolMap
;
43 typedef context::CDHashMap
<Node
, int, NodeHashFunction
> NodeIntMap
;
44 typedef context::CDHashMap
<Node
, Node
, NodeHashFunction
> NodeNodeMap
;
45 typedef context::CDHashSet
<Node
, NodeHashFunction
> NodeSet
;
48 TheoryStrings(context::Context
* c
, context::UserContext
* u
, OutputChannel
& out
, Valuation valuation
, const LogicInfo
& logicInfo
);
51 void setMasterEqualityEngine(eq::EqualityEngine
* eq
);
53 std::string
identify() const { return std::string("TheoryStrings"); }
56 void propagate(Effort e
);
57 bool propagate(TNode literal
);
58 void explain( TNode literal
, std::vector
<TNode
>& assumptions
);
59 Node
explain( TNode literal
);
62 // NotifyClass for equality engine
63 class NotifyClass
: public eq::EqualityEngineNotify
{
66 NotifyClass(TheoryStrings
& t_str
): d_str(t_str
) {}
67 bool eqNotifyTriggerEquality(TNode equality
, bool value
) {
68 Debug("strings") << "NotifyClass::eqNotifyTriggerEquality(" << equality
<< ", " << (value
? "true" : "false" )<< ")" << std::endl
;
70 return d_str
.propagate(equality
);
72 // We use only literal triggers so taking not is safe
73 return d_str
.propagate(equality
.notNode());
76 bool eqNotifyTriggerPredicate(TNode predicate
, bool value
) {
77 Debug("strings") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate
<< ", " << (value
? "true" : "false") << ")" << std::endl
;
79 return d_str
.propagate(predicate
);
81 return d_str
.propagate(predicate
.notNode());
84 bool eqNotifyTriggerTermEquality(TheoryId tag
, TNode t1
, TNode t2
, bool value
) {
85 Debug("strings") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag
<< ", " << t1
<< ", " << t2
<< ")" << std::endl
;
87 return d_str
.propagate(t1
.eqNode(t2
));
89 return d_str
.propagate(t1
.eqNode(t2
).notNode());
92 void eqNotifyConstantTermMerge(TNode t1
, TNode t2
) {
93 Debug("strings") << "NotifyClass::eqNotifyConstantTermMerge(" << t1
<< ", " << t2
<< ")" << std::endl
;
94 d_str
.conflict(t1
, t2
);
96 void eqNotifyNewClass(TNode t
) {
97 Debug("strings") << "NotifyClass::eqNotifyNewClass(" << t
<< std::endl
;
98 d_str
.eqNotifyNewClass(t
);
100 void eqNotifyPreMerge(TNode t1
, TNode t2
) {
101 Debug("strings") << "NotifyClass::eqNotifyPreMerge(" << t1
<< ", " << t2
<< std::endl
;
102 d_str
.eqNotifyPreMerge(t1
, t2
);
104 void eqNotifyPostMerge(TNode t1
, TNode t2
) {
105 Debug("strings") << "NotifyClass::eqNotifyPostMerge(" << t1
<< ", " << t2
<< std::endl
;
106 d_str
.eqNotifyPostMerge(t1
, t2
);
108 void eqNotifyDisequal(TNode t1
, TNode t2
, TNode reason
) {
109 Debug("strings") << "NotifyClass::eqNotifyDisequal(" << t1
<< ", " << t2
<< ", " << reason
<< std::endl
;
110 d_str
.eqNotifyDisequal(t1
, t2
, reason
);
112 };/* class TheoryStrings::NotifyClass */
124 bool d_opt_regexp_gcd
;
126 Node
getRepresentative( Node t
);
127 bool hasTerm( Node a
);
128 bool areEqual( Node a
, Node b
);
129 bool areDisequal( Node a
, Node b
);
130 Node
getLengthTerm( Node t
);
131 Node
getLength( Node t
);
134 /** The notify class */
135 NotifyClass d_notify
;
136 /** Equaltity engine */
137 eq::EqualityEngine d_equalityEngine
;
138 /** Are we in conflict */
139 context::CDO
<bool> d_conflict
;
140 //list of pairs of nodes to merge
141 std::map
< Node
, Node
> d_pending_exp
;
142 std::vector
< Node
> d_pending
;
143 std::vector
< Node
> d_lemma_cache
;
144 std::map
< Node
, bool > d_pending_req_phase
;
147 NodeList d_infer_exp
;
149 std::map
< Node
, Node
> d_normal_forms_base
;
150 std::map
< Node
, std::vector
< Node
> > d_normal_forms
;
151 std::map
< Node
, std::vector
< Node
> > d_normal_forms_exp
;
152 //map of pairs of terms that have the same normal form
153 NodeListMap d_nf_pairs
;
154 void addNormalFormPair( Node n1
, Node n2
);
155 bool isNormalFormPair( Node n1
, Node n2
);
156 bool isNormalFormPair2( Node n1
, Node n2
);
158 NodeSet d_loop_antec
;
159 NodeSet d_length_intro_vars
;
161 /////////////////////////////////////////////////////////////////////////////
163 /////////////////////////////////////////////////////////////////////////////
165 void collectModelInfo(TheoryModel
* m
, bool fullModel
);
167 /////////////////////////////////////////////////////////////////////////////
169 /////////////////////////////////////////////////////////////////////////////
174 /////////////////////////////////////////////////////////////////////////////
176 /////////////////////////////////////////////////////////////////////////////
178 void addSharedTerm(TNode n
);
179 EqualityStatus
getEqualityStatus(TNode a
, TNode b
);
184 EqcInfo( context::Context
* c
);
186 //constant in this eqc
187 context::CDO
< Node
> d_const_term
;
188 context::CDO
< Node
> d_length_term
;
189 context::CDO
< unsigned > d_cardinality_lem_k
;
190 // 1 = added length lemma
191 context::CDO
< Node
> d_normalized_length
;
193 /** map from representatives to information necessary for equivalence classes */
194 std::map
< Node
, EqcInfo
* > d_eqc_info
;
195 EqcInfo
* getOrMakeEqcInfo( Node eqc
, bool doMake
= true );
196 //maintain which concat terms have the length lemma instantiated
197 NodeSet d_length_inst
;
198 NodeBoolMap d_length_nodes
;
200 void mergeCstVec(std::vector
< Node
> &vec_strings
);
201 bool getNormalForms(Node
&eqc
, std::vector
< Node
> & visited
, std::vector
< Node
> & nf
,
202 std::vector
< std::vector
< Node
> > &normal_forms
,
203 std::vector
< std::vector
< Node
> > &normal_forms_exp
,
204 std::vector
< Node
> &normal_form_src
);
205 bool detectLoop(std::vector
< std::vector
< Node
> > &normal_forms
,
206 int i
, int j
, int index_i
, int index_j
,
207 int &loop_in_i
, int &loop_in_j
);
208 bool processLoop(std::vector
< Node
> &antec
,
209 std::vector
< std::vector
< Node
> > &normal_forms
,
210 std::vector
< Node
> &normal_form_src
,
211 int i
, int j
, int loop_n_index
, int other_n_index
,
212 int loop_index
, int index
, int other_index
);
213 bool processNEqc(std::vector
< std::vector
< Node
> > &normal_forms
,
214 std::vector
< std::vector
< Node
> > &normal_forms_exp
,
215 std::vector
< Node
> &normal_form_src
);
216 bool processReverseNEq(std::vector
< std::vector
< Node
> > &normal_forms
,
217 std::vector
< Node
> &normal_form_src
, std::vector
< Node
> &curr_exp
, unsigned i
, unsigned j
);
218 bool processSimpleNEq( std::vector
< std::vector
< Node
> > &normal_forms
,
219 std::vector
< Node
> &normal_form_src
, std::vector
< Node
> &curr_exp
, unsigned i
, unsigned j
,
220 unsigned& index_i
, unsigned& index_j
, bool isRev
);
221 bool normalizeEquivalenceClass( Node n
, std::vector
< Node
> & visited
, std::vector
< Node
> & nf
, std::vector
< Node
> & nf_exp
);
222 bool processDeq( Node n1
, Node n2
);
223 int processReverseDeq( std::vector
< Node
>& nfi
, std::vector
< Node
>& nfj
, Node ni
, Node nj
);
224 int processSimpleDeq( std::vector
< Node
>& nfi
, std::vector
< Node
>& nfj
, Node ni
, Node nj
, unsigned& index
, bool isRev
);
225 //bool unrollStar( Node atom );
226 Node
mkRegExpAntec(Node atom
, Node ant
);
229 bool checkNormalForms();
231 bool checkLengthsEqc();
232 bool checkCardinality();
233 bool checkInductiveEquations();
234 bool checkMemberships();
235 bool checkPDerivative(Node x
, Node r
, Node atom
, bool &addedLemma
, std::vector
< Node
> &processed
, std::vector
< Node
> &cprocessed
);
236 bool checkContains();
237 bool checkPosContains();
238 bool checkNegContains();
241 void preRegisterTerm(TNode n
);
242 void check(Effort e
);
244 /** Conflict when merging two constants */
245 void conflict(TNode a
, TNode b
);
246 /** called when a new equivalence class is created */
247 void eqNotifyNewClass(TNode t
);
248 /** called when two equivalence classes will merge */
249 void eqNotifyPreMerge(TNode t1
, TNode t2
);
250 /** called when two equivalence classes have merged */
251 void eqNotifyPostMerge(TNode t1
, TNode t2
);
252 /** called when two equivalence classes are made disequal */
253 void eqNotifyDisequal(TNode t1
, TNode t2
, TNode reason
);
255 /** compute care graph */
256 void computeCareGraph();
259 void doPendingFacts();
260 void doPendingLemmas();
262 void sendLemma( Node ant
, Node conc
, const char * c
);
263 void sendInfer( Node eq_exp
, Node eq
, const char * c
);
264 void sendSplit( Node a
, Node b
, const char * c
, bool preq
= true );
266 Node
mkConcat( Node n1
, Node n2
);
267 Node
mkConcat( std::vector
< Node
>& c
);
269 Node
mkExplain( std::vector
< Node
>& a
);
270 Node
mkExplain( std::vector
< Node
>& a
, std::vector
< Node
>& an
);
272 Node
mkAnd( std::vector
< Node
>& a
);
273 /** get concat vector */
274 void getConcatVec( Node n
, std::vector
< Node
>& c
);
276 //get equivalence classes
277 void getEquivalenceClasses( std::vector
< Node
>& eqcs
);
278 //get final normal form
279 void getFinalNormalForm( Node n
, std::vector
< Node
>& nf
, std::vector
< Node
>& exp
);
281 //separate into collections with equal length
282 void separateByLength( std::vector
< Node
>& n
, std::vector
< std::vector
< Node
> >& col
, std::vector
< Node
>& lts
);
283 void printConcat( std::vector
< Node
>& n
, const char * c
);
286 Node
mkSplitEq( const char * c
, const char * info
, Node lhs
, Node rhs
, bool lgtZero
);
288 // Special String Functions
289 NodeList d_str_pos_ctn
;
290 NodeList d_str_neg_ctn
;
291 NodeSet d_neg_ctn_eqlen
;
292 NodeSet d_neg_ctn_ulen
;
293 NodeSet d_pos_ctn_cached
;
294 NodeSet d_neg_ctn_cached
;
296 // Regular Expression
298 // regular expression memberships
299 NodeList d_regexp_memberships
;
300 NodeSet d_regexp_ucached
;
301 NodeSet d_regexp_ccached
;
302 // antecedant for why regexp membership must be true
303 NodeNodeMap d_regexp_ant
;
305 //std::map< Node, bool > d_membership_length;
306 // regular expression operations
307 RegExpOpr d_regexp_opr
;
309 CVC4::String
getHeadConst( Node x
);
310 bool splitRegExp( Node x
, Node r
, Node ant
);
311 bool addMembershipLength(Node atom
);
314 // Finite Model Finding
316 NodeSet d_input_vars
;
317 context::CDO
< Node
> d_input_var_lsum
;
318 context::CDHashMap
< int, Node
> d_cardinality_lits
;
319 context::CDO
< int > d_curr_cardinality
;
321 //for finite model finding
322 Node
getNextDecisionRequest();
323 void assertNode( Node lit
);
326 /** statistics class */
331 IntStat d_deq_splits
;
332 IntStat d_loop_lemmas
;
333 IntStat d_new_skolems
;
336 };/* class TheoryStrings::Statistics */
337 Statistics d_statistics
;
338 };/* class TheoryStrings */
340 }/* CVC4::theory::strings namespace */
341 }/* CVC4::theory namespace */
342 }/* CVC4 namespace */
344 #endif /* __CVC4__THEORY__STRINGS__THEORY_STRINGS_H */