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 #include "context/cdhashset.h"
  29
  30 namespace CVC4 {
  31 namespace theory {
  32 namespace strings {
  33
  34 /**
  35  * Decision procedure for strings.
  36  *
  37  */
  38
  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;
  46
  47 public:
  48         TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
  49         ~TheoryStrings();
  50
  51         void setMasterEqualityEngine(eq::EqualityEngine* eq);
  52
  53         std::string identify() const { return std::string("TheoryStrings"); }
  54
  55 public:
  56         void propagate(Effort e);
  57         bool propagate(TNode literal);
  58         void explain( TNode literal, std::vector<TNode>& assumptions );
  59         Node explain( TNode literal );
  60
  61
  62         // NotifyClass for equality engine
  63         class NotifyClass : public eq::EqualityEngineNotify {
  64                 TheoryStrings& d_str;
  65         public:
  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;
  69                   if (value) {
  70                           return d_str.propagate(equality);
  71                   } else {
  72         // We use only literal triggers so taking not is safe
  73         return d_str.propagate(equality.notNode());
  74                   }
  75                 }
  76                 bool eqNotifyTriggerPredicate(TNode predicate, bool value) {
  77                   Debug("strings") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl;
  78                   if (value) {
  79         return d_str.propagate(predicate);
  80                   } else {
  81          return d_str.propagate(predicate.notNode());
  82                   }
  83                 }
  84                 bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
  85                   Debug("strings") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << ")" << std::endl;
  86                   if (value) {
  87                         return d_str.propagate(t1.eqNode(t2));
  88                   } else {
  89                         return d_str.propagate(t1.eqNode(t2).notNode());
  90                   }
  91                 }
  92                 void eqNotifyConstantTermMerge(TNode t1, TNode t2) {
  93                   Debug("strings") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
  94                   d_str.conflict(t1, t2);
  95                 }
  96                 void eqNotifyNewClass(TNode t) {
  97                   Debug("strings") << "NotifyClass::eqNotifyNewClass(" << t << std::endl;
  98                   d_str.eqNotifyNewClass(t);
  99                 }
 100                 void eqNotifyPreMerge(TNode t1, TNode t2) {
 101                   Debug("strings") << "NotifyClass::eqNotifyPreMerge(" << t1 << ", " << t2 << std::endl;
 102                   d_str.eqNotifyPreMerge(t1, t2);
 103                 }
 104                 void eqNotifyPostMerge(TNode t1, TNode t2) {
 105                   Debug("strings") << "NotifyClass::eqNotifyPostMerge(" << t1 << ", " << t2 << std::endl;
 106                   d_str.eqNotifyPostMerge(t1, t2);
 107                 }
 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);
 111                 }
 112         };/* class TheoryStrings::NotifyClass */
 113
 114 private:
 115         /**
 116          * Function symbol used to implement uninterpreted undefined string
 117          * semantics.  Needed to deal with partial charat/substr function.
 118          */
 119         Node d_ufSubstr;
 120
 121         // Constants
 122   Node d_emptyString;
 123         Node d_emptyRegexp;
 124   Node d_true;
 125   Node d_false;
 126   Node d_zero;
 127         Node d_one;
 128         // Options
 129         bool d_opt_fmf;
 130         bool d_opt_regexp_gcd;
 131         // Helper functions
 132         Node getRepresentative( Node t );
 133         bool hasTerm( Node a );
 134         bool areEqual( Node a, Node b );
 135         bool areDisequal( Node a, Node b );
 136         Node getLengthTerm( Node t );
 137         Node getLength( Node t );
 138
 139 private:
 140   /** The notify class */
 141   NotifyClass d_notify;
 142   /** Equaltity engine */
 143   eq::EqualityEngine d_equalityEngine;
 144   /** Are we in conflict */
 145   context::CDO<bool> d_conflict;
 146         //list of pairs of nodes to merge
 147         std::map< Node, Node > d_pending_exp;
 148         std::vector< Node > d_pending;
 149         std::vector< Node > d_lemma_cache;
 150         std::map< Node, bool > d_pending_req_phase;
 151         /** inferences */
 152         NodeList d_infer;
 153         NodeList d_infer_exp;
 154         /** normal forms */
 155         std::map< Node, Node > d_normal_forms_base;
 156         std::map< Node, std::vector< Node > > d_normal_forms;
 157         std::map< Node, std::vector< Node > > d_normal_forms_exp;
 158         //map of pairs of terms that have the same normal form
 159         NodeListMap d_nf_pairs;
 160         void addNormalFormPair( Node n1, Node n2 );
 161         bool isNormalFormPair( Node n1, Node n2 );
 162         bool isNormalFormPair2( Node n1, Node n2 );
 163         // loop ant
 164         NodeSet d_loop_antec;
 165         NodeSet d_length_intro_vars;
 166         // preReg cache
 167         NodeSet d_prereg_cached;
 168
 169         /////////////////////////////////////////////////////////////////////////////
 170         // MODEL GENERATION
 171         /////////////////////////////////////////////////////////////////////////////
 172 public:
 173         void collectModelInfo(TheoryModel* m, bool fullModel);
 174
 175         /////////////////////////////////////////////////////////////////////////////
 176         // NOTIFICATIONS
 177         /////////////////////////////////////////////////////////////////////////////
 178 public:
 179         void presolve();
 180         void shutdown() { }
 181
 182         /////////////////////////////////////////////////////////////////////////////
 183         // MAIN SOLVER
 184         /////////////////////////////////////////////////////////////////////////////
 185 private:
 186         void addSharedTerm(TNode n);
 187         EqualityStatus getEqualityStatus(TNode a, TNode b);
 188
 189 private:
 190         class EqcInfo {
 191         public:
 192                 EqcInfo( context::Context* c );
 193                 ~EqcInfo(){}
 194                 //constant in this eqc
 195                 context::CDO< Node > d_const_term;
 196                 context::CDO< Node > d_length_term;
 197                 context::CDO< unsigned > d_cardinality_lem_k;
 198                 // 1 = added length lemma
 199                 context::CDO< Node > d_normalized_length;
 200         };
 201         /** map from representatives to information necessary for equivalence classes */
 202         std::map< Node, EqcInfo* > d_eqc_info;
 203         EqcInfo * getOrMakeEqcInfo( Node eqc, bool doMake = true );
 204         //maintain which concat terms have the length lemma instantiated
 205         NodeSet d_length_nodes;
 206         NodeNodeMap d_length_inst;
 207 private:
 208         void mergeCstVec(std::vector< Node > &vec_strings);
 209   bool getNormalForms(Node &eqc, std::vector< Node > & visited, std::vector< Node > & nf,
 210         std::vector< std::vector< Node > > &normal_forms,
 211         std::vector< std::vector< Node > > &normal_forms_exp,
 212         std::vector< Node > &normal_form_src);
 213         bool detectLoop(std::vector< std::vector< Node > > &normal_forms,
 214         int i, int j, int index_i, int index_j,
 215         int &loop_in_i, int &loop_in_j);
 216         bool processLoop(std::vector< Node > &antec,
 217         std::vector< std::vector< Node > > &normal_forms,
 218         std::vector< Node > &normal_form_src,
 219         int i, int j, int loop_n_index, int other_n_index,
 220         int loop_index, int index, int other_index);
 221         bool processNEqc(std::vector< std::vector< Node > > &normal_forms,
 222         std::vector< std::vector< Node > > &normal_forms_exp,
 223         std::vector< Node > &normal_form_src);
 224         bool processReverseNEq(std::vector< std::vector< Node > > &normal_forms,
 225         std::vector< Node > &normal_form_src, std::vector< Node > &curr_exp, unsigned i, unsigned j );
 226         bool processSimpleNEq( std::vector< std::vector< Node > > &normal_forms,
 227         std::vector< Node > &normal_form_src, std::vector< Node > &curr_exp, unsigned i, unsigned j,
 228         unsigned& index_i, unsigned& index_j, bool isRev );
 229   bool normalizeEquivalenceClass( Node n, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< Node > & nf_exp );
 230   bool processDeq( Node n1, Node n2 );
 231         int processReverseDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj );
 232         int processSimpleDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj, unsigned& index, bool isRev );
 233         //bool unrollStar( Node atom );
 234         Node mkRegExpAntec(Node atom, Node ant);
 235
 236         bool checkSimple();
 237   bool checkNormalForms();
 238         void checkDeqNF();
 239         bool checkLengthsEqc();
 240   bool checkCardinality();
 241   bool checkInductiveEquations();
 242         bool checkMemberships();
 243         bool checkPDerivative(Node x, Node r, Node atom, bool &addedLemma,
 244                 std::vector< Node > &processed, std::vector< Node > &cprocessed,
 245                 std::vector< Node > &nf_exp);
 246         bool checkContains();
 247         bool checkPosContains();
 248         bool checkNegContains();
 249
 250 public:
 251         void preRegisterTerm(TNode n);
 252         Node expandDefinition(LogicRequest &logicRequest, Node n);
 253         void check(Effort e);
 254
 255         /** Conflict when merging two constants */
 256         void conflict(TNode a, TNode b);
 257         /** called when a new equivalence class is created */
 258         void eqNotifyNewClass(TNode t);
 259         /** called when two equivalence classes will merge */
 260         void eqNotifyPreMerge(TNode t1, TNode t2);
 261         /** called when two equivalence classes have merged */
 262         void eqNotifyPostMerge(TNode t1, TNode t2);
 263         /** called when two equivalence classes are made disequal */
 264         void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
 265 protected:
 266         /** compute care graph */
 267         void computeCareGraph();
 268
 269         //do pending merges
 270         void doPendingFacts();
 271         void doPendingLemmas();
 272
 273         void sendLemma( Node ant, Node conc, const char * c );
 274         void sendInfer( Node eq_exp, Node eq, const char * c );
 275         void sendSplit( Node a, Node b, const char * c, bool preq = true );
 276         /** mkConcat **/
 277         inline Node mkConcat( Node n1, Node n2 );
 278         inline Node mkConcat( std::vector< Node >& c );
 279         /** mkExplain **/
 280         Node mkExplain( std::vector< Node >& a );
 281         Node mkExplain( std::vector< Node >& a, std::vector< Node >& an );
 282         /** mkAnd **/
 283         Node mkAnd( std::vector< Node >& a );
 284         /** get concat vector */
 285         void getConcatVec( Node n, std::vector< Node >& c );
 286
 287         //get equivalence classes
 288         void getEquivalenceClasses( std::vector< Node >& eqcs );
 289         //get final normal form
 290         void getFinalNormalForm( Node n, std::vector< Node >& nf, std::vector< Node >& exp );
 291
 292         //separate into collections with equal length
 293         void separateByLength( std::vector< Node >& n, std::vector< std::vector< Node > >& col, std::vector< Node >& lts );
 294         void printConcat( std::vector< Node >& n, const char * c );
 295
 296 private:
 297         Node mkSplitEq( const char * c, const char * info, Node lhs, Node rhs, bool lgtZero );
 298
 299         // Special String Functions
 300         NodeList d_str_pos_ctn;
 301         NodeList d_str_neg_ctn;
 302         NodeSet d_neg_ctn_eqlen;
 303         NodeSet d_neg_ctn_ulen;
 304         NodeSet d_pos_ctn_cached;
 305         NodeSet d_neg_ctn_cached;
 306
 307         // Symbolic Regular Expression
 308 private:
 309         // regular expression memberships
 310         NodeList d_regexp_memberships;
 311         NodeSet d_regexp_ucached;
 312         NodeSet d_regexp_ccached;
 313         // intersection
 314         NodeListMap d_str_re_map;
 315         NodeNodeMap d_inter_cache;
 316         NodeIntMap d_inter_index;
 317         // antecedant for why regexp membership must be true
 318         NodeNodeMap d_regexp_ant;
 319         // membership length
 320         //std::map< Node, bool > d_membership_length;
 321         // regular expression operations
 322         RegExpOpr d_regexp_opr;
 323
 324         CVC4::String getHeadConst( Node x );
 325         bool deriveRegExp( Node x, Node r, Node ant );
 326         bool addMembershipLength(Node atom);
 327         void addMembership(Node assertion);
 328         Node getNormalString(Node x, std::vector<Node> &nf_exp);
 329         Node getNormalSymRegExp(Node r, std::vector<Node> &nf_exp);
 330
 331
 332         // Finite Model Finding
 333 private:
 334         NodeSet d_input_vars;
 335         context::CDO< Node > d_input_var_lsum;
 336         context::CDHashMap< int, Node > d_cardinality_lits;
 337         context::CDO< int > d_curr_cardinality;
 338 public:
 339         //for finite model finding
 340   Node getNextDecisionRequest();
 341         void assertNode( Node lit );
 342
 343 public:
 344 /** statistics class */
 345   class Statistics {
 346   public:
 347     IntStat d_splits;
 348     IntStat d_eq_splits;
 349     IntStat d_deq_splits;
 350     IntStat d_loop_lemmas;
 351     IntStat d_new_skolems;
 352     Statistics();
 353     ~Statistics();
 354   };/* class TheoryStrings::Statistics */
 355   Statistics d_statistics;
 356 };/* class TheoryStrings */
 357
 358 }/* CVC4::theory::strings namespace */
 359 }/* CVC4::theory namespace */
 360 }/* CVC4 namespace */
 361
 362 #endif /* __CVC4__THEORY__STRINGS__THEORY_STRINGS_H */