From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Fri, 13 Jan 2017 15:40:15 +0000 (-0600)
Subject: Do not rewrite explanations in strings.
X-Git-Tag: cvc5-1.0.0~5917
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=52b431e92ea7596f369399cd9c1c20c06ad61e60;p=cvc5.git

Do not rewrite explanations in strings.
---

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 6c4a00541..bf999806f 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -259,6 +259,8 @@ void TheoryStrings::explain(TNode literal, std::vector<TNode>& assumptions) {
   std::vector< TNode > tassumptions;
   if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
     if( atom[0]!=atom[1] ){
+      Assert( hasTerm( atom[0] ) );
+      Assert( hasTerm( atom[1] ) );
       d_equalityEngine.explainEquality(atom[0], atom[1], polarity, tassumptions);
     }
   } else {
@@ -276,6 +278,7 @@ void TheoryStrings::explain(TNode literal, std::vector<TNode>& assumptions) {
 }
 
 Node TheoryStrings::explain( TNode literal ){
+  Debug("strings-explain") << "explain called on " << literal << std::endl;
   std::vector< TNode > assumptions;
   explain( literal, assumptions );
   if( assumptions.empty() ){
@@ -3286,10 +3289,10 @@ void TheoryStrings::sendInference( std::vector< Node >& exp, Node eq, const char
 
 void TheoryStrings::sendLemma( Node ant, Node conc, const char * c ) {
   if( conc.isNull() || conc == d_false ) {
-    d_out->conflict(ant);
     Trace("strings-conflict") << "Strings::Conflict : " << c << " : " << ant << std::endl;
     Trace("strings-lemma") << "Strings::Conflict : " << c << " : " << ant << std::endl;
     Trace("strings-assert") << "(assert (not " << ant << ")) ; conflict " << c << std::endl;
+    d_out->conflict(ant);
     d_conflict = true;
   } else {
     Node lem;
@@ -3533,7 +3536,7 @@ Node TheoryStrings::mkExplain( std::vector< Node >& a, std::vector< Node >& an )
   } else {
     ant = NodeManager::currentNM()->mkNode( kind::AND, antec_exp );
   }
-  ant = Rewriter::rewrite( ant );
+  //ant = Rewriter::rewrite( ant );
   return ant;
 }