diff options
Diffstat (limited to 'src/theory/strings/theory_strings.h')
-rw-r--r-- | src/theory/strings/theory_strings.h | 49 |
1 files changed, 26 insertions, 23 deletions
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index fef2983fd..b9da524de 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -1,13 +1,13 @@ /********************* */ /*! \file theory_strings.h ** \verbatim - ** Original author: Tianyi Liang - ** Major contributors: Andrew Reynolds - ** Minor contributors (to current version): Martin Brain <>, Morgan Deters + ** Top contributors (to current version): + ** Tianyi Liang, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Theory of strings ** @@ -158,6 +158,7 @@ private: std::map< Node, Node > d_normal_forms_base; std::map< Node, std::vector< Node > > d_normal_forms; std::map< Node, std::vector< Node > > d_normal_forms_exp; + std::map< Node, std::map< Node, std::map< bool, int > > > d_normal_forms_exp_depend; //map of pairs of terms that have the same normal form NodeListMap d_nf_pairs; void addNormalFormPair( Node n1, Node n2 ); @@ -174,7 +175,7 @@ private: NodeBoolMap d_preproc_cache; // extended functions inferences cache NodeSet d_extf_infer_cache; - + std::vector< Node > d_empty_vec; private: NodeSet d_congruent; std::map< Node, Node > d_eqc_to_const; @@ -236,7 +237,6 @@ private: NodeNodeMap d_proxy_var; NodeNodeMap d_proxy_var_to_length; private: - //initial check void checkInit(); void checkConstantEquivalenceClasses( TermIndex* ti, std::vector< Node >& vecc ); @@ -254,30 +254,31 @@ private: //normal forms check void checkNormalForms(); bool normalizeEquivalenceClass( Node n, std::vector< Node > & nf, std::vector< Node > & nf_exp ); - bool getNormalForms( Node &eqc, std::vector< Node > & nf, - std::vector< std::vector< Node > > &normal_forms, - std::vector< std::vector< Node > > &normal_forms_exp, - std::vector< Node > &normal_form_src); + bool getNormalForms( Node &eqc, std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src, + std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend); bool detectLoop(std::vector< std::vector< Node > > &normal_forms, - int i, int j, int index_i, int index_j, - int &loop_in_i, int &loop_in_j); + int i, int j, int index, int &loop_in_i, int &loop_in_j); bool processLoop(std::vector< Node > &antec, std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src, int i, int j, int loop_n_index, int other_n_index, - int loop_index, int index, int other_index); - bool processNEqc(std::vector< std::vector< Node > > &normal_forms, - std::vector< std::vector< Node > > &normal_forms_exp, - std::vector< Node > &normal_form_src); - bool processReverseNEq(std::vector< std::vector< Node > > &normal_forms, - std::vector< Node > &normal_form_src, std::vector< Node > &curr_exp, unsigned i, unsigned j ); - bool processSimpleNEq( std::vector< std::vector< Node > > &normal_forms, - std::vector< Node > &normal_form_src, std::vector< Node > &curr_exp, unsigned i, unsigned j, - unsigned& index_i, unsigned& index_j, bool isRev ); + int loop_index, int index); + bool processNEqc( std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src, + std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend ); + bool processReverseNEq( std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src, + std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend, + unsigned i, unsigned j ); + bool processSimpleNEq( std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src, + std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend, + unsigned i, unsigned j, unsigned& index, bool isRev ); bool processDeq( Node n1, Node n2 ); int processReverseDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj ); int processSimpleDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj, unsigned& index, bool isRev ); void checkDeqNF(); + + void getExplanationVectorForPrefix( std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src, + std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend, + unsigned i, unsigned j, int index, bool isRev, std::vector< Node >& curr_exp ); //check for extended functions void checkExtendedFuncs(); @@ -337,6 +338,8 @@ protected: //register term void registerTerm( Node n, int effort ); //send lemma + void sendInference( std::vector< Node >& exp, std::vector< Node >& exp_n, Node eq, const char * c, bool asLemma = false ); + void sendInference( std::vector< Node >& exp, Node eq, const char * c, bool asLemma = false ); void sendLemma( Node ant, Node conc, const char * c ); void sendInfer( Node eq_exp, Node eq, const char * c ); void sendSplit( Node a, Node b, const char * c, bool preq = true ); |