summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
authorTianyi Liang <tianyi-liang@uiowa.edu>2013-10-16 10:16:59 -0500
committerTianyi Liang <tianyi-liang@uiowa.edu>2013-10-16 10:16:59 -0500
commit04868401c51b7f29c2b43ebc508dea59769dae93 (patch)
tree30570664aa123972f3c4937ae306404cf9723102 /src/theory
parent66401350d11abc0a161825a7af8927b48cc7038f (diff)
renames for strings fmf
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/strings/options2
-rw-r--r--src/theory/strings/theory_strings.cpp4
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();
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback