diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-01-13 09:40:15 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-01-13 09:40:32 -0600 |
| commit | 52b431e92ea7596f369399cd9c1c20c06ad61e60 (patch) | |
| tree | 4ea5b01196d58a61a614eb1a2dc6de7cc3c55f70 /src | |
| parent | f167e765f04a898931b6a40b887fb491a546303f (diff) | |
Do not rewrite explanations in strings.
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 7 |
1 files changed, 5 insertions, 2 deletions
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; } |