diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-01-23 22:45:16 -0800 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-01-23 22:45:16 -0800 |
| commit | 72732b7653a35fc59cce2af77ab6a375b9eed890 (patch) | |
| tree | bdf0063d8faf4c0cfe973d5691452fad995dfdae | |
| parent | efdcb3cf578530e179a61386f1ec047be576d000 (diff) | |
experimentoverlap
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 23b818984..24b1887f3 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -3075,7 +3075,17 @@ void TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal Node length_eq = NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j ); length_eq = Rewriter::rewrite( length_eq ); //set info - info.d_conc = NodeManager::currentNM()->mkNode( kind::OR, length_eq, length_eq.negate() ); + if (TheoryStringsRewriter::checkEntailArith(length_term_i, length_term_j, true)) { + info.d_conc = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::GT, length_term_i, length_term_j)); + } else if (TheoryStringsRewriter::checkEntailArith(length_term_i, length_term_j, false)) { + info.d_conc = NodeManager::currentNM()->mkNode(kind::OR, length_eq, Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::GT, length_term_i, length_term_j))); + } else if (TheoryStringsRewriter::checkEntailArith(length_term_j, length_term_i, true)) { + info.d_conc = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::GT, length_term_j, length_term_i)); + } else if (TheoryStringsRewriter::checkEntailArith(length_term_i, length_term_j, false)) { + info.d_conc = NodeManager::currentNM()->mkNode(kind::OR, length_eq, Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::GT, length_term_j, length_term_i))); + } else { + info.d_conc = NodeManager::currentNM()->mkNode(kind::OR, length_eq, length_eq.negate()); + } info.d_pending_phase[ length_eq ] = true; info.d_id = INFER_LEN_SPLIT; info_valid = true; |