diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-10-21 12:29:48 -0500 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-10-21 12:29:48 -0500 |
| commit | 730e88ecb2b3ae6fdb9148c096820516c61356f3 (patch) | |
| tree | b33d824ffa32ac178bab5836bdb15a83f3aa07d9 | |
| parent | f695f7e29caa1bfbf6824f0f2a1377cdc6b4b638 (diff) | |
string fix
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 435be2ba4..910447589 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -548,8 +548,13 @@ void TheoryStrings::doPendingFacts() { bool polarity = fact.getKind() != kind::NOT; TNode atom = polarity ? fact : fact[0]; if (atom.getKind() == kind::EQUAL) { - Assert( d_equalityEngine.hasTerm( atom[0] ) ); - Assert( d_equalityEngine.hasTerm( atom[1] ) ); + //Assert( d_equalityEngine.hasTerm( atom[0] ) ); + //Assert( d_equalityEngine.hasTerm( atom[1] ) ); + for( unsigned j=0; j<2; j++ ){ + if( !d_equalityEngine.hasTerm( atom[j] ) ){ + d_equalityEngine.addTerm( atom[j] ); + } + } d_equalityEngine.assertEquality( atom, polarity, exp ); }else{ d_equalityEngine.assertPredicate( atom, polarity, exp ); @@ -797,7 +802,7 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v } Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, d_emptyString, normal_forms[k][index_k] ); Trace("strings-lemma") << "Strings : Infer " << eq << " from " << eq_exp << std::endl; - Assert( !d_equalityEngine.areEqual( d_emptyString, normal_forms[k][index_k] ) ); + Assert( !areEqual( d_emptyString, normal_forms[k][index_k] ) ); d_pending.push_back( eq ); d_pending_exp[eq] = eq_exp; d_infer.push_back(eq); |