src/theory/strings/theory_strings.h

   1 /*********************                                                        */
   2 /*! \file theory_strings.h
   3  ** \verbatim
   4  ** Original author: Tianyi Liang
   5  ** Major contributors: Andrew Reynolds
   6  ** Minor contributors (to current version): Martin Brain <>, 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
  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 #include "expr/attribute.h"
  30
  31 #include <climits>
  32 #include <deque>
  33
  34 namespace CVC4 {
  35 namespace theory {
  36 namespace strings {
  37
  38 /**
  39  * Decision procedure for strings.
  40  *
  41  */
  42
  43 struct StringsProxyVarAttributeId {};
  44 typedef expr::Attribute< StringsProxyVarAttributeId, bool > StringsProxyVarAttribute;
  45
  46 class TheoryStrings : public Theory {
  47   typedef context::CDChunkList<Node> NodeList;
  48   typedef context::CDHashMap<Node, NodeList*, NodeHashFunction> NodeListMap;
  49   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
  50   typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
  51   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
  52   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
  53
  54 public:
  55   TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
  56   ~TheoryStrings();
  57
  58   void setMasterEqualityEngine(eq::EqualityEngine* eq);
  59
  60   std::string identify() const { return std::string("TheoryStrings"); }
  61
  62 public:
  63   void propagate(Effort e);
  64   bool propagate(TNode literal);
  65   void explain( TNode literal, std::vector<TNode>& assumptions );
  66   Node explain( TNode literal );
  67
  68
  69   // NotifyClass for equality engine
  70   class NotifyClass : public eq::EqualityEngineNotify {
  71     TheoryStrings& d_str;
  72   public:
  73     NotifyClass(TheoryStrings& t_str): d_str(t_str) {}
  74     bool eqNotifyTriggerEquality(TNode equality, bool value) {
  75       Debug("strings") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl;
  76       if (value) {
  77         return d_str.propagate(equality);
  78       } else {
  79         // We use only literal triggers so taking not is safe
  80         return d_str.propagate(equality.notNode());
  81       }
  82     }
  83     bool eqNotifyTriggerPredicate(TNode predicate, bool value) {
  84       Debug("strings") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl;
  85       if (value) {
  86         return d_str.propagate(predicate);
  87       } else {
  88          return d_str.propagate(predicate.notNode());
  89       }
  90     }
  91     bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
  92       Debug("strings") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << ")" << std::endl;
  93       if (value) {
  94       return d_str.propagate(t1.eqNode(t2));
  95       } else {
  96       return d_str.propagate(t1.eqNode(t2).notNode());
  97       }
  98     }
  99     void eqNotifyConstantTermMerge(TNode t1, TNode t2) {
 100       Debug("strings") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
 101       d_str.conflict(t1, t2);
 102     }
 103     void eqNotifyNewClass(TNode t) {
 104       Debug("strings") << "NotifyClass::eqNotifyNewClass(" << t << std::endl;
 105       d_str.eqNotifyNewClass(t);
 106     }
 107     void eqNotifyPreMerge(TNode t1, TNode t2) {
 108       Debug("strings") << "NotifyClass::eqNotifyPreMerge(" << t1 << ", " << t2 << std::endl;
 109       d_str.eqNotifyPreMerge(t1, t2);
 110     }
 111     void eqNotifyPostMerge(TNode t1, TNode t2) {
 112       Debug("strings") << "NotifyClass::eqNotifyPostMerge(" << t1 << ", " << t2 << std::endl;
 113       d_str.eqNotifyPostMerge(t1, t2);
 114     }
 115     void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
 116       Debug("strings") << "NotifyClass::eqNotifyDisequal(" << t1 << ", " << t2 << ", " << reason << std::endl;
 117       d_str.eqNotifyDisequal(t1, t2, reason);
 118     }
 119   };/* class TheoryStrings::NotifyClass */
 120
 121 private:
 122   /**
 123    * Function symbol used to implement uninterpreted undefined string
 124    * semantics.  Needed to deal with partial charat/substr function.
 125    */
 126   Node d_ufSubstr;
 127
 128   // Constants
 129   Node d_emptyString;
 130   Node d_emptyRegexp;
 131   Node d_true;
 132   Node d_false;
 133   Node d_zero;
 134   Node d_one;
 135   CVC4::Rational RMAXINT;
 136   unsigned d_card_size;
 137   // Options
 138   bool d_opt_fmf;
 139   bool d_opt_regexp_gcd;
 140   // Helper functions
 141   Node getRepresentative( Node t );
 142   bool hasTerm( Node a );
 143   bool areEqual( Node a, Node b );
 144   bool areDisequal( Node a, Node b );
 145   Node getLengthTerm( Node t );
 146   Node getLength( Node t, bool use_t = false );
 147
 148 private:
 149   /** The notify class */
 150   NotifyClass d_notify;
 151   /** Equaltity engine */
 152   eq::EqualityEngine d_equalityEngine;
 153   /** Are we in conflict */
 154   context::CDO<bool> d_conflict;
 155   //list of pairs of nodes to merge
 156   std::map< Node, Node > d_pending_exp;
 157   std::vector< Node > d_pending;
 158   std::vector< Node > d_lemma_cache;
 159   std::map< Node, bool > d_pending_req_phase;
 160   /** inferences: maintained to ensure ref count for internally introduced nodes */
 161   NodeList d_infer;
 162   NodeList d_infer_exp;
 163   /** normal forms */
 164   std::map< Node, Node > d_normal_forms_base;
 165   std::map< Node, std::vector< Node > > d_normal_forms;
 166   std::map< Node, std::vector< Node > > d_normal_forms_exp;
 167   //map of pairs of terms that have the same normal form
 168   NodeListMap d_nf_pairs;
 169   void addNormalFormPair( Node n1, Node n2 );
 170   bool isNormalFormPair( Node n1, Node n2 );
 171   bool isNormalFormPair2( Node n1, Node n2 );
 172   // loop ant
 173   NodeSet d_loop_antec;
 174   NodeSet d_length_intro_vars;
 175   // preReg cache
 176   NodeSet d_registered_terms_cache;
 177   // preprocess cache
 178   StringsPreprocess d_preproc;
 179   NodeBoolMap d_preproc_cache;
 180   // extended functions inferences cache
 181   NodeSet d_extf_infer_cache;
 182
 183   bool doPreprocess( Node atom );
 184   bool hasProcessed();
 185   void addToExplanation( Node a, Node b, std::vector< Node >& exp );
 186   void addToExplanation( Node lit, std::vector< Node >& exp );
 187
 188 private:
 189   std::vector< Node > d_congruent;
 190   std::map< Node, Node > d_eqc_to_const;
 191   std::map< Node, Node > d_eqc_to_const_base;
 192   std::map< Node, Node > d_eqc_to_const_exp;
 193   std::map< Node, Node > d_eqc_to_len_term;
 194   std::vector< Node > d_strings_eqc;
 195   Node d_emptyString_r;
 196   class TermIndex {
 197   public:
 198     Node d_data;
 199     std::map< Node, TermIndex > d_children;
 200     Node add( Node n, unsigned index, TheoryStrings* t, Node er, std::vector< Node >& c );
 201     void clear(){ d_children.clear(); }
 202   };
 203   std::map< Kind, TermIndex > d_term_index;
 204   //list of non-congruent concat terms in each eqc
 205   std::map< Node, std::vector< Node > > d_eqc;
 206   std::map< Node, std::vector< Node > > d_flat_form;
 207   std::map< Node, std::vector< int > > d_flat_form_index;
 208
 209   void debugPrintFlatForms( const char * tc );
 210   /////////////////////////////////////////////////////////////////////////////
 211   // MODEL GENERATION
 212   /////////////////////////////////////////////////////////////////////////////
 213 public:
 214   void collectModelInfo(TheoryModel* m, bool fullModel);
 215
 216   /////////////////////////////////////////////////////////////////////////////
 217   // NOTIFICATIONS
 218   /////////////////////////////////////////////////////////////////////////////
 219 public:
 220   void presolve();
 221   void shutdown() { }
 222
 223   /////////////////////////////////////////////////////////////////////////////
 224   // MAIN SOLVER
 225   /////////////////////////////////////////////////////////////////////////////
 226 private:
 227   void addSharedTerm(TNode n);
 228   EqualityStatus getEqualityStatus(TNode a, TNode b);
 229
 230 private:
 231   class EqcInfo {
 232   public:
 233     EqcInfo( context::Context* c );
 234     ~EqcInfo(){}
 235     //constant in this eqc
 236     context::CDO< Node > d_const_term;
 237     context::CDO< Node > d_length_term;
 238     context::CDO< unsigned > d_cardinality_lem_k;
 239     // 1 = added length lemma
 240     context::CDO< Node > d_normalized_length;
 241   };
 242   /** map from representatives to information necessary for equivalence classes */
 243   std::map< Node, EqcInfo* > d_eqc_info;
 244   EqcInfo * getOrMakeEqcInfo( Node eqc, bool doMake = true );
 245   //maintain which concat terms have the length lemma instantiated
 246   NodeNodeMap d_proxy_var;
 247   NodeNodeMap d_proxy_var_to_length;
 248 private:
 249   void mergeCstVec(std::vector< Node > &vec_strings);
 250   bool getNormalForms(Node &eqc, std::vector< Node > & visited, std::vector< Node > & nf,
 251         std::vector< std::vector< Node > > &normal_forms,
 252         std::vector< std::vector< Node > > &normal_forms_exp,
 253         std::vector< Node > &normal_form_src);
 254   bool detectLoop(std::vector< std::vector< Node > > &normal_forms,
 255         int i, int j, int index_i, int index_j,
 256         int &loop_in_i, int &loop_in_j);
 257   bool processLoop(std::vector< Node > &antec,
 258         std::vector< std::vector< Node > > &normal_forms,
 259         std::vector< Node > &normal_form_src,
 260         int i, int j, int loop_n_index, int other_n_index,
 261         int loop_index, int index, int other_index);
 262   bool processNEqc(std::vector< std::vector< Node > > &normal_forms,
 263         std::vector< std::vector< Node > > &normal_forms_exp,
 264         std::vector< Node > &normal_form_src);
 265   bool processReverseNEq(std::vector< std::vector< Node > > &normal_forms,
 266         std::vector< Node > &normal_form_src, std::vector< Node > &curr_exp, unsigned i, unsigned j );
 267   bool processSimpleNEq( std::vector< std::vector< Node > > &normal_forms,
 268         std::vector< Node > &normal_form_src, std::vector< Node > &curr_exp, unsigned i, unsigned j,
 269         unsigned& index_i, unsigned& index_j, bool isRev );
 270   bool normalizeEquivalenceClass( Node n, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< Node > & nf_exp );
 271   bool processDeq( Node n1, Node n2 );
 272   int processReverseDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj );
 273   int processSimpleDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj, unsigned& index, bool isRev );
 274   //bool unrollStar( Node atom );
 275   Node mkRegExpAntec(Node atom, Node ant);
 276
 277   void checkInit();
 278   void checkConstantEquivalenceClasses( TermIndex* ti, std::vector< Node >& vecc );
 279   void checkExtendedFuncsEval( int effort = 0 );
 280   void checkExtfInference( Node n, Node nr, int n_pol, int effort );
 281   void collectVars( Node n, std::map< Node, std::vector< Node > >& vars, std::map< Node, bool >& visited );
 282   void checkFlatForms();
 283   void checkNormalForms();
 284   Node checkCycles( Node eqc, std::vector< Node >& curr, std::vector< Node >& exp );
 285   void checkDeqNF();
 286   void checkLengthsEqc();
 287   void checkCardinality();
 288   bool checkInductiveEquations();
 289   //check membership constraints
 290   Node normalizeRegexp(Node r);
 291   bool normalizePosMemberships(std::map< Node, std::vector< Node > > &memb_with_exps);
 292   bool applyRConsume( CVC4::String &s, Node &r);
 293   Node applyRSplit(Node s1, Node s2, Node r);
 294   bool applyRLen(std::map< Node, std::vector< Node > > &XinR_with_exps);
 295   bool checkMembershipsWithoutLength(
 296     std::map< Node, std::vector< Node > > &memb_with_exps,
 297     std::map< Node, std::vector< Node > > &XinR_with_exps);
 298   void checkMemberships();
 299   //temp
 300   bool checkMemberships2();
 301   bool checkPDerivative(Node x, Node r, Node atom, bool &addedLemma,
 302     std::vector< Node > &processed, std::vector< Node > &cprocessed,
 303     std::vector< Node > &nf_exp);
 304   void checkExtendedFuncs();
 305   void checkPosContains( std::vector< Node >& posContains );
 306   void checkNegContains( std::vector< Node >& negContains );
 307   Node getSymbolicDefinition( Node n, std::vector< Node >& exp );
 308
 309 public:
 310   void preRegisterTerm(TNode n);
 311   Node expandDefinition(LogicRequest &logicRequest, Node n);
 312   void check(Effort e);
 313
 314   /** Conflict when merging two constants */
 315   void conflict(TNode a, TNode b);
 316   /** called when a new equivalence class is created */
 317   void eqNotifyNewClass(TNode t);
 318   /** called when two equivalence classes will merge */
 319   void eqNotifyPreMerge(TNode t1, TNode t2);
 320   /** called when two equivalence classes have merged */
 321   void eqNotifyPostMerge(TNode t1, TNode t2);
 322   /** called when two equivalence classes are made disequal */
 323   void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
 324   /** get preprocess */
 325   StringsPreprocess * getPreprocess() { return &d_preproc; }
 326 protected:
 327   /** compute care graph */
 328   void computeCareGraph();
 329
 330   //do pending merges
 331   void assertPendingFact(Node atom, bool polarity, Node exp);
 332   void doPendingFacts();
 333   void doPendingLemmas();
 334
 335   //register term
 336   bool registerTerm( Node n );
 337   //send lemma
 338   void sendLemma( Node ant, Node conc, const char * c );
 339   void sendInfer( Node eq_exp, Node eq, const char * c );
 340   void sendSplit( Node a, Node b, const char * c, bool preq = true );
 341   void sendLengthLemma( Node n );
 342   /** mkConcat **/
 343   inline Node mkConcat( Node n1, Node n2 );
 344   inline Node mkConcat( Node n1, Node n2, Node n3 );
 345   inline Node mkConcat( const std::vector< Node >& c );
 346   //mkSkolem
 347   inline Node mkSkolemS(const char * c, int isLenSplit = 0);
 348   //inline Node mkSkolemI(const char * c);
 349   /** mkExplain **/
 350   Node mkExplain( std::vector< Node >& a );
 351   Node mkExplain( std::vector< Node >& a, std::vector< Node >& an );
 352   /** mkAnd **/
 353   Node mkAnd( std::vector< Node >& a );
 354   /** get concat vector */
 355   void getConcatVec( Node n, std::vector< Node >& c );
 356
 357   //get equivalence classes
 358   void getEquivalenceClasses( std::vector< Node >& eqcs );
 359   //get final normal form
 360   void getFinalNormalForm( Node n, std::vector< Node >& nf, std::vector< Node >& exp );
 361
 362   //separate into collections with equal length
 363   void separateByLength( std::vector< Node >& n, std::vector< std::vector< Node > >& col, std::vector< Node >& lts );
 364   void printConcat( std::vector< Node >& n, const char * c );
 365
 366   void inferSubstitutionProxyVars( Node n, std::vector< Node >& vars, std::vector< Node >& subs, std::vector< Node >& unproc );
 367
 368   enum {
 369     sk_id_c_spt,
 370     sk_id_vc_spt,
 371     sk_id_v_spt,
 372     sk_id_ctn_pre,
 373     sk_id_ctn_post,
 374     sk_id_deq_x,
 375     sk_id_deq_y,
 376     sk_id_deq_z,
 377   };
 378   std::map< Node, std::map< Node, std::map< int, Node > > > d_skolem_cache;
 379   Node mkSkolemCached( Node a, Node b, int id, const char * c, int isLenSplit = 0 );
 380 private:
 381
 382   // Special String Functions
 383   NodeSet d_neg_ctn_eqlen;
 384   NodeSet d_neg_ctn_ulen;
 385   NodeSet d_pos_ctn_cached;
 386   NodeSet d_neg_ctn_cached;
 387   //extended string terms and whether they have been reduced
 388   NodeBoolMap d_ext_func_terms;
 389   std::map< Node, std::map< Node, std::vector< Node > > > d_extf_vars;
 390   class ExtfInfo {
 391   public:
 392     std::map< bool, std::vector< Node > > d_ctn;
 393     std::map< bool, std::vector< Node > > d_ctn_from;
 394   };
 395   std::map< Node, std::vector< Node > > d_extf_exp;
 396   std::map< Node, ExtfInfo > d_extf_info;
 397   //collect extended operator terms
 398   void collectExtendedFuncTerms( Node n, std::map< Node, bool >& visited );
 399
 400   // Symbolic Regular Expression
 401 private:
 402   // regular expression memberships
 403   NodeList d_regexp_memberships;
 404   NodeSet d_regexp_ucached;
 405   NodeSet d_regexp_ccached;
 406   // stored assertions
 407   NodeListMap d_pos_memberships;
 408   NodeListMap d_neg_memberships;
 409   // semi normal forms for symbolic expression
 410   std::map< Node, Node > d_nf_regexps;
 411   std::map< Node, std::vector< Node > > d_nf_regexps_exp;
 412   // intersection
 413   NodeNodeMap d_inter_cache;
 414   NodeIntMap d_inter_index;
 415   // processed memberships
 416   NodeSet d_processed_memberships;
 417   // antecedant for why regexp membership must be true
 418   NodeNodeMap d_regexp_ant;
 419   // membership length
 420   //std::map< Node, bool > d_membership_length;
 421   // regular expression operations
 422   RegExpOpr d_regexp_opr;
 423
 424   CVC4::String getHeadConst( Node x );
 425   bool deriveRegExp( Node x, Node r, Node ant );
 426   bool addMembershipLength(Node atom);
 427   void addMembership(Node assertion);
 428   Node getNormalString(Node x, std::vector<Node> &nf_exp);
 429   Node getNormalSymRegExp(Node r, std::vector<Node> &nf_exp);
 430
 431
 432   // Finite Model Finding
 433 private:
 434   NodeSet d_input_vars;
 435   context::CDO< Node > d_input_var_lsum;
 436   context::CDHashMap< int, Node > d_cardinality_lits;
 437   context::CDO< int > d_curr_cardinality;
 438 public:
 439   //for finite model finding
 440   Node getNextDecisionRequest();
 441   void assertNode( Node lit );
 442
 443 public:
 444 /** statistics class */
 445   class Statistics {
 446   public:
 447     IntStat d_splits;
 448     IntStat d_eq_splits;
 449     IntStat d_deq_splits;
 450     IntStat d_loop_lemmas;
 451     IntStat d_new_skolems;
 452     Statistics();
 453     ~Statistics();
 454   };/* class TheoryStrings::Statistics */
 455   Statistics d_statistics;
 456 };/* class TheoryStrings */
 457
 458 }/* CVC4::theory::strings namespace */
 459 }/* CVC4::theory namespace */
 460 }/* CVC4 namespace */
 461
 462 #endif /* __CVC4__THEORY__STRINGS__THEORY_STRINGS_H */