diff options
author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-10-16 10:16:59 -0500 |
---|---|---|
committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-10-16 10:16:59 -0500 |
commit | 04868401c51b7f29c2b43ebc508dea59769dae93 (patch) | |
tree | 30570664aa123972f3c4937ae306404cf9723102 | |
parent | 66401350d11abc0a161825a7af8927b48cc7038f (diff) |
renames for strings fmf
-rw-r--r-- | src/theory/strings/options | 2 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 4 |
2 files changed, 4 insertions, 2 deletions
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(); |