diff options
author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-05-18 21:06:29 -0500 |
---|---|---|
committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-05-18 21:06:29 -0500 |
commit | 3ce2f2590ba541e901403707e924ad10f0b5f7d5 (patch) | |
tree | e57b3856f235d56563883fcce2044515578faaea /src | |
parent | 035047b15cfe72cd82410b68c5cfff601e4f9203 (diff) |
minor fix for string equality engine assertion.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 13 |
1 files changed, 11 insertions, 2 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 0b161570a..0f9def3ea 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -732,6 +732,15 @@ void TheoryStrings::assertPendingFact(Node fact, Node exp) { } d_equalityEngine.assertEquality( atom, polarity, exp ); } else { + if ( atom.getKind() == kind::STRING_IN_REGEXP ) { + addMembership(fact); + } else if (atom.getKind() == kind::STRING_STRCTN) { + if(polarity) { + d_str_pos_ctn.push_back( atom ); + } else { + d_str_neg_ctn.push_back( atom ); + } + } d_equalityEngine.assertPredicate( atom, polarity, exp ); } } @@ -741,7 +750,7 @@ void TheoryStrings::doPendingFacts() { while( !d_conflict && i<d_pending.size() ) { Node fact = d_pending[i]; Node exp = d_pending_exp[ fact ]; - if(fact.getKind() == kind::STRING_CONCAT) { + if(fact.getKind() == kind::AND) { for(size_t j=0; j<fact.getNumChildren(); j++) { assertPendingFact(fact[j], exp); } @@ -1128,7 +1137,7 @@ bool TheoryStrings::processLoop(std::vector< Node > &antec, d_regexp_ant[str_in_re] = ant; } - //if(conc.isNull() || conc.getKind() == kind::OR) { + //if(conc.isNull() || conc == d_false || conc.getKind() == kind::OR) { sendLemma( ant, conc, "LOOP-BREAK" ); //} else { //sendInfer( ant, conc, "LOOP-BREAK" ); |