From 04868401c51b7f29c2b43ebc508dea59769dae93 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Wed, 16 Oct 2013 10:16:59 -0500 Subject: renames for strings fmf --- src/theory/strings/options | 2 +- src/theory/strings/theory_strings.cpp | 4 +++- 2 files changed, 4 insertions(+), 2 deletions(-) (limited to 'src/theory') diff --git a/src/theory/strings/options b/src/theory/strings/options index 2832c7833..58cbbc1b1 100644 --- a/src/theory/strings/options +++ b/src/theory/strings/options @@ -11,7 +11,7 @@ option stringCharCardinality str-alphabet-card --str-alphabet-card=N int16_t :de option stringRegExpUnrollDepth str-regexp-depth --str-regexp-depth=N int16_t :default 10 :read-write the depth of unrolloing regular expression used by the theory of strings, default 10 -option stringFMF fmf-strings --fmf-strings bool :default false +option stringFMF strings-fmf --str-fmf bool :default false the finite model finding used by the theory of strings endmodule diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 1aae55a83..c4ecd02cf 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -1908,7 +1908,7 @@ bool TheoryStrings::checkMemberships() { } Node TheoryStrings::getNextDecisionRequest() { - if(d_fmf) { + if(d_fmf && !d_conflict) { Trace("strings-decide") << "Get next decision request." << std::endl; Trace("strings-fmf-debug") << "Input variables: "; for(std::vector< Node >::iterator itr = d_in_vars.begin(); @@ -1916,6 +1916,8 @@ Node TheoryStrings::getNextDecisionRequest() { Trace("strings-fmf-debug") << " " << (*itr) ; } Trace("strings-fmf-debug") << std::endl; + + } return Node::null(); -- cgit v1.2.3