From 3a358738071a330efda34671655979edf1d6d875 Mon Sep 17 00:00:00 2001
From: Liana Hadarean <lianahady@gmail.com>
Date: Mon, 24 Aug 2015 11:55:16 +0100
Subject: [PATCH] Added threshold for core bv cardinality lemmas

---
 src/theory/bv/bv_subtheory_core.cpp | 8 ++++++++
 src/theory/bv/bv_subtheory_core.h   | 3 ++-
 2 files changed, 10 insertions(+), 1 deletion(-)

diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index 9b8e0677e..6ae0ffb71 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -36,6 +36,7 @@ CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv)
     d_equalityEngine(d_notify, c, "theory::bv::TheoryBV", true),
     d_slicer(new Slicer()),
     d_isComplete(c, true),
+    d_lemmaThreshold(16),
     d_useSlicer(false),
     d_preregisterCalled(false),
     d_checkCalled(false),
@@ -286,11 +287,18 @@ void CoreSolver::buildModel() {
             }
           }
         }
+        // better off letting the SAT solver split on values
+        if (equalities.size() > d_lemmaThreshold) {
+          d_isComplete = false;
+          return;
+        }
+
         Node lemma = utils::mkOr(equalities);
         d_bv->lemma(lemma);
         Debug("bv-core") << "  lemma: " << lemma << "\n";
         return;
       }
+    
       Debug("bv-core-model") << "   " << repr << " => " << val <<"\n" ;
       constants.insert(val);
       d_modelValues[repr] = val;
diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h
index 5b9c54095..0ff193b41 100644
--- a/src/theory/bv/bv_subtheory_core.h
+++ b/src/theory/bv/bv_subtheory_core.h
@@ -74,9 +74,10 @@ class CoreSolver : public SubtheorySolver {
 
   Slicer* d_slicer;
   context::CDO<bool> d_isComplete;
+  unsigned d_lemmaThreshold;
   
   /** Used to ensure that the core slicer is used properly*/
-  bool d_useSlicer; 
+  bool d_useSlicer;
   bool d_preregisterCalled;
   bool d_checkCalled;
   
-- 
2.30.2