diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-06-24 12:15:42 -0400 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-06-25 13:42:38 -0400 |
commit | c57e0640f56ce5286870f27c9f1a9af6dd7e757f (patch) | |
tree | fd0f73deffe88ed7660a48a774cacd8cd5a15088 /src/theory/sets | |
parent | 58586bd4a33f32d02b84502cabb1e34107bb539d (diff) |
fix sets eager lemmas
Diffstat (limited to 'src/theory/sets')
-rw-r--r-- | src/theory/sets/options | 4 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/sets/options b/src/theory/sets/options index dc6c6e907..1c95e78e4 100644 --- a/src/theory/sets/options +++ b/src/theory/sets/options @@ -8,7 +8,7 @@ module SETS "theory/sets/options.h" Sets option setsPropagate --sets-propagate bool :default true determines whether to propagate learnt facts to Theory Engine / SAT solver -option setsEagerLemmas --sets-eager-lemmas bool :default false - if true, will add lemmas even if not at FULL_EFFORT +option setsEagerLemmas --sets-eager-lemmas bool :default true + add lemmas even at regular effort endmodule diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 0a7ecd14e..be2b48f81 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -97,7 +97,7 @@ void TheorySetsPrivate::check(Theory::Effort level) { Debug("sets") << "[sets] is complete = " << isComplete() << std::endl; } - if( (Theory::EFFORT_FULL || options::setsEagerLemmas() ) && !isComplete()) { + if( (level == Theory::EFFORT_FULL || options::setsEagerLemmas() ) && !isComplete()) { d_external.d_out->lemma(getLemma()); return; } |