From 72732b7653a35fc59cce2af77ab6a375b9eed890 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 23 Jan 2019 22:45:16 -0800 Subject: experiment --- src/theory/strings/theory_strings.cpp | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) 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; -- cgit v1.2.3