diff options
| author | Liana Hadarean <lianahady@gmail.com> | 2015-08-24 11:55:16 +0100 |
|---|---|---|
| committer | Liana Hadarean <lianahady@gmail.com> | 2015-08-24 17:50:49 +0100 |
| commit | 3a358738071a330efda34671655979edf1d6d875 (patch) | |
| tree | f18a6968c0875a574c03c5ed2ba9008272f3fe33 /src | |
| parent | 531e7931a33079c4f1213ac56d285c578710ed49 (diff) | |
Added threshold for core bv cardinality lemmas
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/bv/bv_subtheory_core.cpp | 8 | ||||
| -rw-r--r-- | src/theory/bv/bv_subtheory_core.h | 3 |
2 files changed, 10 insertions, 1 deletions
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; |