Added threshold for core bv cardinality lemmas

diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index 9b8e0677e53d9b2e008fa340f4b47844bfa3944f..6ae0ffb71569b34f946d522c0f4cccbd43a71864 100644 (file)
--- 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 5b9c54095ed496b4142518c81a1870e25449d839..0ff193b4136a5cc8a245097d87ca9101506799b2 100644 (file)
--- 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;