From 973cbd67611a2943714fd9544d098ec1472a40b8 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Mon, 16 Mar 2015 11:04:43 -0500 Subject: [PATCH] Add requirePhase len(x) = 0. --- src/theory/strings/theory_strings.cpp | 2 ++ 1 file changed, 2 insertions(+) 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 ) { -- 2.30.2