diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2017-11-30 15:50:00 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-11-30 15:50:00 -0800 |
commit | 4c1f1cad720a94226f7834874cf59478de35b74a (patch) | |
tree | b97655661092e2597b31c089ec9bc52e77d33ec9 /src/smt | |
parent | 89b6c052e96cc907800650de93d2f238e19acd38 (diff) |
Add Gaussian Elimination as a preprocessing pass for BV. (#1342)
This adds Gaussian Elimination as a preprocessing pass for BV. Gaussian Elimination is only applied if the given bit-width guarantees that no overflows can occur.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 15 |
1 files changed, 14 insertions, 1 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 3a0cb297e..f9d3c9909 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -86,6 +86,7 @@ #include "theory/arith/arith_msum.h" #include "theory/arith/pseudoboolean_proc.h" #include "theory/booleans/circuit_propagator.h" +#include "theory/bv/bvgauss.h" #include "theory/bv/bvintropow2.h" #include "theory/bv/theory_bv_rewriter.h" #include "theory/logic_info.h" @@ -185,6 +186,8 @@ public: };/* class AssertionPipeline */ struct SmtEngineStatistics { + /** time spent in gaussian elimination */ + TimerStat d_gaussElimTime; /** time spent in definition-expansion */ TimerStat d_definitionExpansionTime; /** time spent in non-clausal simplification */ @@ -232,6 +235,7 @@ struct SmtEngineStatistics { ReferenceStat<uint64_t> d_resourceUnitsUsed; SmtEngineStatistics() : + d_gaussElimTime("smt::SmtEngine::gaussElimTime"), d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"), d_nonclausalSimplificationTime("smt::SmtEngine::nonclausalSimplificationTime"), d_miplibPassTime("smt::SmtEngine::miplibPassTime"), @@ -256,6 +260,7 @@ struct SmtEngineStatistics { d_resourceUnitsUsed("smt::SmtEngine::resourceUnitsUsed") { + smtStatisticsRegistry()->registerStat(&d_gaussElimTime); smtStatisticsRegistry()->registerStat(&d_definitionExpansionTime); smtStatisticsRegistry()->registerStat(&d_nonclausalSimplificationTime); smtStatisticsRegistry()->registerStat(&d_miplibPassTime); @@ -281,6 +286,7 @@ struct SmtEngineStatistics { } ~SmtEngineStatistics() { + smtStatisticsRegistry()->unregisterStat(&d_gaussElimTime); smtStatisticsRegistry()->unregisterStat(&d_definitionExpansionTime); smtStatisticsRegistry()->unregisterStat(&d_nonclausalSimplificationTime); smtStatisticsRegistry()->unregisterStat(&d_miplibPassTime); @@ -1427,9 +1433,10 @@ void SmtEngine::setDefaults() { if(options::bvIntroducePow2.wasSetByUser()) { throw OptionException("bv-intro-pow2 not supported with unsat cores"); } - Notice() << "SmtEngine: turning off bv-introduce-pow2 to support unsat-cores" << endl; + Notice() << "SmtEngine: turning off bv-intro-pow2 to support unsat-cores" << endl; setOption("bv-intro-pow2", false); } + if(options::repeatSimp()) { if(options::repeatSimp.wasSetByUser()) { throw OptionException("repeat-simp not supported with unsat cores"); @@ -4006,6 +4013,12 @@ void SmtEnginePrivate::processAssertions() { return; } + if(options::bvGaussElim()) + { + TimerStat::CodeTimer gaussElimTimer(d_smt.d_stats->d_gaussElimTime); + theory::bv::BVGaussElim::gaussElimRewrite(d_assertions.ref()); + } + if (d_assertionsProcessed && options::incrementalSolving()) { // TODO(b/1255): Substitutions in incremental mode should be managed with a // proper data structure. |