From 37a080c02e769cc2fe5427c11a5f0dc362c25465 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sun, 15 Apr 2018 20:52:46 -0500 Subject: [PATCH] Make strings fmf apply to all but internally generated Skolems (#1780) --- src/theory/strings/theory_strings.cpp | 11 +++++++++-- src/theory/strings/theory_strings.h | 2 ++ 2 files changed, 11 insertions(+), 2 deletions(-) diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 713c346e0..fe6f7ea77 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -648,8 +648,14 @@ void TheoryStrings::preRegisterTerm(TNode n) { TypeNode tn = n.getType(); if( tn.isString() ) { registerTerm( n, 0 ); - // FMF - if( n.getKind() == kind::VARIABLE && options::stringFMF() ){ + // if finite model finding is enabled, + // then we minimize the length of this term if it is a variable + // but not an internally generated Skolem, or a term that does + // not belong to this theory. + if (options::stringFMF() + && (n.isVar() ? d_all_skolems.find(n) == d_all_skolems.end() + : kindToTheoryId(n.getKind()) != THEORY_STRINGS)) + { d_input_vars.insert(n); } d_equalityEngine.addTerm(n); @@ -3569,6 +3575,7 @@ Node TheoryStrings::mkSkolemCached( Node a, Node b, int id, const char * c, int //isLenSplit: -1-ignore, 0-no restriction, 1-greater than one, 2-one Node TheoryStrings::mkSkolemS( const char *c, int isLenSplit ) { Node n = NodeManager::currentNM()->mkSkolem( c, NodeManager::currentNM()->stringType(), "string sko" ); + d_all_skolems.insert(n); d_length_lemma_terms_cache.insert( n ); ++(d_statistics.d_new_skolems); if( isLenSplit==0 ){ diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index cff49ccb8..22406adef 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -489,6 +489,8 @@ private: sk_id_deq_z, }; std::map > > d_skolem_cache; + /** the set of all skolems we have generated */ + std::unordered_set d_all_skolems; Node mkSkolemCached( Node a, Node b, int id, const char* c, int isLenSplit = 0); inline Node mkSkolemS(const char* c, int isLenSplit = 0); -- 2.30.2