diff options
author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-12-03 13:53:47 -0600 |
---|---|---|
committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-12-03 13:53:47 -0600 |
commit | 359258592d0b048645f53a6f77d52a72177c128f (patch) | |
tree | 23ff65eb66716e2a96a3d2a665295a8c8e384a70 | |
parent | 59bde437d57769331f3408ab37efc5b536e9131d (diff) |
string fmf perfomance fix
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 4e20ac248..a4c0c00b8 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -356,12 +356,12 @@ void TheoryStrings::preRegisterTerm(TNode n) { if(n.getKind() == kind::VARIABLE || n.getKind()==kind::SKOLEM) { if( std::find( d_length_intro_vars.begin(), d_length_intro_vars.end(), n )==d_length_intro_vars.end() ){ Node n_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n); - //Node n_len_geq_zero = NodeManager::currentNM()->mkNode( kind::GEQ, n_len, d_zero); - Node n_len_geq_zero = NodeManager::currentNM()->mkNode( kind::OR, - n_len.eqNode( d_zero ), - NodeManager::currentNM()->mkNode( kind::GT, n_len, d_zero) ); + Node n_len_eq_z = n_len.eqNode( d_zero ); + Node n_len_geq_zero = NodeManager::currentNM()->mkNode( kind::OR, n_len_eq_z, + NodeManager::currentNM()->mkNode( kind::GT, n_len, d_zero) ); Trace("strings-lemma") << "Strings::Lemma LENGTH geq 0 : " << n_len_geq_zero << std::endl; d_out->lemma(n_len_geq_zero); + d_out->requirePhase( n_len_eq_z, true ); } // FMF if( n.getKind() == kind::VARIABLE ) {//options::stringFMF() && |