diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-20 10:56:20 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-20 10:59:46 +0100 |
| commit | f70804a7159390fcb01d8c1ec208fbfd8e544fba (patch) | |
| tree | a16f6ae65eda646ab5f80ef4633b3199c648d853 /src/theory/strings/theory_strings.h | |
| parent | eebaff108e57f15cf19c78d3b9eb27ac1d90dc11 (diff) | |
Disable constants sharing in eq engine, disable hack in theory engine. Changes to strings solver : modify lemmas/splits to avoid constants, minor refactoring. Fix assertion failure in quantifiers engine.
Diffstat (limited to 'src/theory/strings/theory_strings.h')
| -rw-r--r-- | src/theory/strings/theory_strings.h | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 95eba27bc..d9326c316 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -2,7 +2,7 @@ /*! \file theory_strings.h ** \verbatim ** Original author: Tianyi Liang - ** Major contributors: none + ** Major contributors: Andrew Reynolds ** Minor contributors (to current version): Martin Brain <>, Morgan Deters ** This file is part of the CVC4 project. ** Copyright (c) 2009-2014 New York University and The University of Iowa @@ -209,7 +209,6 @@ private: std::map< Node, EqcInfo* > d_eqc_info; EqcInfo * getOrMakeEqcInfo( Node eqc, bool doMake = true ); //maintain which concat terms have the length lemma instantiated - NodeSet d_length_nodes; NodeNodeMap d_length_inst; private: void mergeCstVec(std::vector< Node > &vec_strings); @@ -240,7 +239,7 @@ private: //bool unrollStar( Node atom ); Node mkRegExpAntec(Node atom, Node ant); - bool checkSimple(); + //bool checkSimple(); bool checkNormalForms(); void checkDeqNF(); bool checkLengthsEqc(); @@ -284,6 +283,7 @@ protected: 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 ); + void sendLengthLemma( Node n ); /** mkConcat **/ inline Node mkConcat( Node n1, Node n2 ); inline Node mkConcat( Node n1, Node n2, Node n3 ); |