diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2015-03-16 11:04:43 -0500 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2015-03-16 11:04:43 -0500 |
| commit | 973cbd67611a2943714fd9544d098ec1472a40b8 (patch) | |
| tree | aa7cbe26ec868e0ccfd154498989d16d828c8b6c | |
| parent | f591f7c1671b8345b56c8d3e3adef9627c5fa8c1 (diff) | |
Add requirePhase len(x) = 0.
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 862f5c7bc..6d2dc3138 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -1947,11 +1947,13 @@ void TheoryStrings::sendLengthLemma( Node n ){ //registerTerm( d_emptyString ); Node n_len_eq_z_2 = n.eqNode( d_emptyString ); n_len_eq_z = Rewriter::rewrite( n_len_eq_z ); + n_len_eq_z_2 = Rewriter::rewrite( n_len_eq_z_2 ); Node n_len_geq_zero = NodeManager::currentNM()->mkNode( kind::OR, NodeManager::currentNM()->mkNode( kind::AND, n_len_eq_z, n_len_eq_z_2 ), NodeManager::currentNM()->mkNode( kind::GT, n_len, d_zero) ); Trace("strings-lemma") << "Strings::Lemma LENGTH >= 0 : " << n_len_geq_zero << std::endl; d_out->lemma(n_len_geq_zero); d_out->requirePhase( n_len_eq_z, true ); + d_out->requirePhase( n_len_eq_z_2, true ); } Node TheoryStrings::mkConcat( Node n1, Node n2 ) { |