From c57e0640f56ce5286870f27c9f1a9af6dd7e757f Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Tue, 24 Jun 2014 12:15:42 -0400 Subject: [PATCH] fix sets eager lemmas --- src/theory/sets/options | 4 ++-- 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; } -- 2.30.2