src/theory/strings/theory_strings.h

   1 /*********************                                                        */
   2 /*! \file theory_strings.h
   3  ** \verbatim
   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
  11  **
  12  ** \brief Theory of strings
  13  **
  14  ** Theory of strings.
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #ifndef __CVC4__THEORY__STRINGS__THEORY_STRINGS_H
  20 #define __CVC4__THEORY__STRINGS__THEORY_STRINGS_H
  21
  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"
  26
  27 #include "context/cdchunk_list.h"
  28
  29 namespace CVC4 {
  30 namespace theory {
  31 namespace strings {
  32
  33 /**
  34  * Decision procedure for strings.
  35  *
  36  */
  37
  38 class TheoryStrings : public Theory {
  39         typedef context::CDChunkList<Node> NodeList;
  40         typedef context::CDHashMap<Node, NodeList*, NodeHashFunction> NodeListMap;
  41         typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
  42         typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
  43
  44 public:
  45         TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
  46         ~TheoryStrings();
  47
  48         void setMasterEqualityEngine(eq::EqualityEngine* eq);
  49
  50         std::string identify() const { return std::string("TheoryStrings"); }
  51
  52 public:
  53         void propagate(Effort e);
  54         bool propagate(TNode literal);
  55         void explain( TNode literal, std::vector<TNode>& assumptions );
  56         Node explain( TNode literal );
  57
  58
  59         // NotifyClass for equality engine
  60         class NotifyClass : public eq::EqualityEngineNotify {
  61                 TheoryStrings& d_str;
  62         public:
  63                 NotifyClass(TheoryStrings& t_str): d_str(t_str) {}
  64                 bool eqNotifyTriggerEquality(TNode equality, bool value) {
  65                   Debug("strings") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl;
  66                   if (value) {
  67                         return d_str.propagate(equality);
  68                   } else {
  69                         // We use only literal triggers so taking not is safe
  70                         return d_str.propagate(equality.notNode());
  71                   }
  72                 }
  73                 bool eqNotifyTriggerPredicate(TNode predicate, bool value) {
  74                   Debug("strings") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl;
  75                   if (value) {
  76                         return d_str.propagate(predicate);
  77                   } else {
  78                    return d_str.propagate(predicate.notNode());
  79                   }
  80                 }
  81                 bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
  82                   Debug("strings") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << ")" << std::endl;
  83                   if (value) {
  84                         return d_str.propagate(t1.eqNode(t2));
  85                   } else {
  86                         return d_str.propagate(t1.eqNode(t2).notNode());
  87                   }
  88                 }
  89                 void eqNotifyConstantTermMerge(TNode t1, TNode t2) {
  90                   Debug("strings") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
  91                   d_str.conflict(t1, t2);
  92                 }
  93                 void eqNotifyNewClass(TNode t) {
  94                   Debug("strings") << "NotifyClass::eqNotifyNewClass(" << t << std::endl;
  95                   d_str.eqNotifyNewClass(t);
  96                 }
  97                 void eqNotifyPreMerge(TNode t1, TNode t2) {
  98                   Debug("strings") << "NotifyClass::eqNotifyPreMerge(" << t1 << ", " << t2 << std::endl;
  99                   d_str.eqNotifyPreMerge(t1, t2);
 100                 }
 101                 void eqNotifyPostMerge(TNode t1, TNode t2) {
 102                   Debug("strings") << "NotifyClass::eqNotifyPostMerge(" << t1 << ", " << t2 << std::endl;
 103                   d_str.eqNotifyPostMerge(t1, t2);
 104                 }
 105                 void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
 106                   Debug("strings") << "NotifyClass::eqNotifyDisequal(" << t1 << ", " << t2 << ", " << reason << std::endl;
 107                   d_str.eqNotifyDisequal(t1, t2, reason);
 108                 }
 109         };/* class TheoryStrings::NotifyClass */
 110
 111 private:
 112         // Constants
 113     Node d_emptyString;
 114     Node d_true;
 115     Node d_false;
 116     Node d_zero;
 117         // Options
 118         bool d_all_warning;
 119         bool d_opt_fmf;
 120         bool d_opt_regexp_gcd;
 121         // Helper functions
 122         Node getRepresentative( Node t );
 123         bool hasTerm( Node a );
 124         bool areEqual( Node a, Node b );
 125         bool areDisequal( Node a, Node b );
 126         Node getLengthTerm( Node t );
 127         Node getLength( Node t );
 128
 129 private:
 130     /** The notify class */
 131     NotifyClass d_notify;
 132     /** Equaltity engine */
 133     eq::EqualityEngine d_equalityEngine;
 134     /** Are we in conflict */
 135     context::CDO<bool> d_conflict;
 136         std::vector< Node > d_length_intro_vars;
 137         //list of pairs of nodes to merge
 138         std::map< Node, Node > d_pending_exp;
 139         std::vector< Node > d_pending;
 140         std::vector< Node > d_lemma_cache;
 141         std::map< Node, bool > d_pending_req_phase;
 142         /** inferences */
 143         NodeList d_infer;
 144         NodeList d_infer_exp;
 145         /** normal forms */
 146         std::map< Node, Node > d_normal_forms_base;
 147         std::map< Node, std::vector< Node > > d_normal_forms;
 148         std::map< Node, std::vector< Node > > d_normal_forms_exp;
 149         //map of pairs of terms that have the same normal form
 150         NodeListMap d_nf_pairs;
 151         void addNormalFormPair( Node n1, Node n2 );
 152         bool isNormalFormPair( Node n1, Node n2 );
 153         bool isNormalFormPair2( Node n1, Node n2 );
 154         // loop ant
 155         std::map< Node, bool > d_loop_antec;
 156
 157         /////////////////////////////////////////////////////////////////////////////
 158         // MODEL GENERATION
 159         /////////////////////////////////////////////////////////////////////////////
 160 public:
 161         void collectModelInfo(TheoryModel* m, bool fullModel);
 162
 163         /////////////////////////////////////////////////////////////////////////////
 164         // NOTIFICATIONS
 165         /////////////////////////////////////////////////////////////////////////////
 166 public:
 167         void presolve();
 168         void shutdown() { }
 169
 170         /////////////////////////////////////////////////////////////////////////////
 171         // MAIN SOLVER
 172         /////////////////////////////////////////////////////////////////////////////
 173 private:
 174         void addSharedTerm(TNode n);
 175         EqualityStatus getEqualityStatus(TNode a, TNode b);
 176
 177 private:
 178         class EqcInfo {
 179         public:
 180                 EqcInfo( context::Context* c );
 181                 ~EqcInfo(){}
 182                 //constant in this eqc
 183                 context::CDO< Node > d_const_term;
 184                 context::CDO< Node > d_length_term;
 185                 context::CDO< unsigned > d_cardinality_lem_k;
 186                 // 1 = added length lemma
 187                 context::CDO< Node > d_normalized_length;
 188         };
 189         /** map from representatives to information necessary for equivalence classes */
 190         std::map< Node, EqcInfo* > d_eqc_info;
 191         EqcInfo * getOrMakeEqcInfo( Node eqc, bool doMake = true );
 192         //maintain which concat terms have the length lemma instantiated
 193         std::map< Node, bool > d_length_inst;
 194         NodeBoolMap d_length_nodes;
 195 private:
 196         void mergeCstVec(std::vector< Node > &vec_strings);
 197     bool getNormalForms(Node &eqc, std::vector< Node > & visited, std::vector< Node > & nf,
 198                                                 std::vector< std::vector< Node > > &normal_forms,
 199                                                 std::vector< std::vector< Node > > &normal_forms_exp,
 200                                                 std::vector< Node > &normal_form_src);
 201         bool detectLoop(std::vector< std::vector< Node > > &normal_forms,
 202                                         int i, int j, int index_i, int index_j,
 203                                         int &loop_in_i, int &loop_in_j);
 204         bool processLoop(std::vector< Node > &antec,
 205                                          std::vector< std::vector< Node > > &normal_forms,
 206                                          std::vector< Node > &normal_form_src,
 207                                          int i, int j, int loop_n_index, int other_n_index,
 208                                          int loop_index, int index, int other_index);
 209         bool processNEqc(std::vector< std::vector< Node > > &normal_forms,
 210                                          std::vector< std::vector< Node > > &normal_forms_exp,
 211                                          std::vector< Node > &normal_form_src);
 212     bool normalizeEquivalenceClass( Node n, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< Node > & nf_exp );
 213     bool normalizeDisequality( Node n1, Node n2 );
 214         bool unrollStar( Node atom );
 215
 216         bool checkLengths();
 217     bool checkNormalForms();
 218         bool checkLengthsEqc();
 219     bool checkCardinality();
 220     bool checkInductiveEquations();
 221         bool checkMemberships();
 222         bool checkContains();
 223         bool checkPosContains();
 224         bool checkNegContains();
 225
 226 public:
 227         void preRegisterTerm(TNode n);
 228         void check(Effort e);
 229
 230         /** Conflict when merging two constants */
 231         void conflict(TNode a, TNode b);
 232         /** called when a new equivalence class is created */
 233         void eqNotifyNewClass(TNode t);
 234         /** called when two equivalence classes will merge */
 235         void eqNotifyPreMerge(TNode t1, TNode t2);
 236         /** called when two equivalence classes have merged */
 237         void eqNotifyPostMerge(TNode t1, TNode t2);
 238         /** called when two equivalence classes are made disequal */
 239         void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
 240 protected:
 241         /** compute care graph */
 242         void computeCareGraph();
 243
 244         //do pending merges
 245         void doPendingFacts();
 246         void doPendingLemmas();
 247
 248         void sendLemma( Node ant, Node conc, const char * c );
 249         void sendSplit( Node a, Node b, const char * c, bool preq = true );
 250         /** mkConcat **/
 251         Node mkConcat( Node n1, Node n2 );
 252         Node mkConcat( std::vector< Node >& c );
 253         /** mkExplain **/
 254         Node mkExplain( std::vector< Node >& a );
 255         Node mkExplain( std::vector< Node >& a, std::vector< Node >& an );
 256         /** get concat vector */
 257         void getConcatVec( Node n, std::vector< Node >& c );
 258
 259         //get equivalence classes
 260         void getEquivalenceClasses( std::vector< Node >& eqcs );
 261         //get final normal form
 262         void getFinalNormalForm( Node n, std::vector< Node >& nf, std::vector< Node >& exp );
 263
 264         //separate into collections with equal length
 265         void separateByLength( std::vector< Node >& n, std::vector< std::vector< Node > >& col, std::vector< Node >& lts );
 266         void printConcat( std::vector< Node >& n, const char * c );
 267
 268         // Measurement
 269 private:
 270         //NodeIntMap d_var_lmin;
 271         //NodeIntMap d_var_lmax;
 272         std::map< Node, Node > d_var_split_graph_lhs;
 273         std::map< Node, Node > d_var_split_graph_rhs;
 274         std::map< Node, bool > d_var_lgtz;
 275         Node mkSplitEq( const char * c, const char * info, Node lhs, Node rhs, bool lgtZero );
 276         int getMaxPossibleLength( Node x );
 277
 278         // Special String Functions
 279         Node d_charAtUF;
 280         NodeList d_str_pos_ctn;
 281         NodeList d_str_neg_ctn;
 282         std::map< Node, bool > d_str_ctn_eqlen;
 283         std::map< Node, bool > d_str_pos_ctn_rewritten;
 284         std::map< Node, bool > d_str_neg_ctn_rewritten;
 285
 286         // Regular Expression
 287 private:
 288         // regular expression memberships
 289         NodeList d_reg_exp_mem;
 290         // antecedant for why reg exp membership must be true
 291         std::map< Node, Node > d_reg_exp_ant;
 292         std::map< Node, bool > d_reg_exp_unroll;
 293         std::map< Node, int > d_reg_exp_unroll_depth;
 294         bool d_regexp_incomplete;
 295         int d_regexp_unroll_depth;
 296         int d_regexp_max_depth;
 297         // membership length
 298         std::map< Node, bool > d_membership_length;
 299         // regular expression derivative
 300         std::map< Node, bool > d_reg_exp_deriv;
 301         // regular expression operations
 302         RegExpOpr d_regexp_opr;
 303
 304         CVC4::String getHeadConst( Node x );
 305         bool splitRegExp( Node x, Node r, Node ant );
 306         bool addMembershipLength(Node atom);
 307
 308
 309         // Finite Model Finding
 310 private:
 311         std::vector< Node > d_in_vars;
 312         Node d_in_var_lsum;
 313         std::map< int, Node > d_cardinality_lits;
 314         context::CDO< int > d_curr_cardinality;
 315 public:
 316         //for finite model finding
 317     Node getNextDecisionRequest();
 318         void assertNode( Node lit );
 319
 320 };/* class TheoryStrings */
 321
 322 }/* CVC4::theory::strings namespace */
 323 }/* CVC4::theory namespace */
 324 }/* CVC4 namespace */
 325
 326 #endif /* __CVC4__THEORY__STRINGS__THEORY_STRINGS_H */