summaryrefslogtreecommitdiff
path: root/src/theory/strings/theory_strings.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/strings/theory_strings.h')
-rw-r--r--src/theory/strings/theory_strings.h49
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 );
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback