From: Liana Hadarean <lianahady@gmail.com>
Date: Mon, 24 Aug 2015 10:55:16 +0000 (+0100)
Subject: Added threshold for core bv cardinality lemmas
X-Git-Tag: cvc5-1.0.0~6252^2~7
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3a358738071a330efda34671655979edf1d6d875;p=cvc5.git

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 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;