diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-03-13 15:55:57 -0700 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-03-13 19:23:57 -0700 |
commit | c97077abcefd18dce9510f169a5c530f6b4cc5ce (patch) | |
tree | 6331339beb0fae6aa888294d1ab8d9c7d296d513 | |
parent | ea1f76a2c9fc700aab017526a6232d6b03ed3194 (diff) |
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index d643fac70..db1f388ad 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -24,6 +24,7 @@ #include "smt/logic_exception.h" #include "smt/smt_statistics_registry.h" #include "theory/ext_theory.h" +#include "theory/quantifiers/extended_rewrite.h" #include "theory/rewriter.h" #include "theory/strings/theory_strings_rewriter.h" #include "theory/strings/type_enumerator.h" @@ -2843,6 +2844,7 @@ void TheoryStrings::processNEqc( std::vector< std::vector< Node > > &normal_form if( isNormalFormPair( normal_form_src[i], normal_form_src[j] ) ) { Trace("strings-solve") << "Strings: Already cached." << std::endl; }else{ + /* Node eq = nm->mkNode( EQUAL, TheoryStringsRewriter::mkConcat(STRING_CONCAT, normal_forms[i]), @@ -2869,6 +2871,7 @@ void TheoryStrings::processNEqc( std::vector< std::vector< Node > > &normal_form sendInternalInference(antec, eqr, "__equality_rew"); } } + */ //process the reverse direction first (check for easy conflicts and inferences) unsigned rindex = 0; @@ -4026,7 +4029,7 @@ void TheoryStrings::sendInternalInference(std::vector<Node>& exp, } void TheoryStrings::sendInference( std::vector< Node >& exp, std::vector< Node >& exp_n, Node eq, const char * c, bool asLemma ) { - eq = eq.isNull() ? d_false : Rewriter::rewrite( eq ); + eq = eq.isNull() ? d_false : Rewriter::rewrite(eq); if( eq!=d_true ){ if( Trace.isOn("strings-infer-debug") ){ Trace("strings-infer-debug") << "By " << c << ", infer : " << eq << " from: " << std::endl; |