Skip to content

Commit

Permalink
Merge branch 'development' into pub/fmplex-qe
Browse files Browse the repository at this point in the history
  • Loading branch information
ValentinPromies committed Feb 5, 2024
2 parents 80eb3cb + 345f8f5 commit e467513
Show file tree
Hide file tree
Showing 3 changed files with 31 additions and 5 deletions.
8 changes: 4 additions & 4 deletions src/smtrat-qe/fm/FMQEStatistics.h
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ class FMQEStatistics : public Statistics
std::size_t m_output_constraints = 0;
std::size_t m_total_constraints = 0;
bool m_eq_conflict = false;
carl::statistics::timer m_qe_timer;
carl::statistics::Timer m_qe_timer;


public:
Expand All @@ -35,13 +35,13 @@ class FMQEStatistics : public Statistics
void vars(std::size_t n) { m_eliminated_vars = n; }
void elim_eq(std::size_t n) { m_eliminated_by_eq = m_eliminated_vars - n; }
void output(std::size_t n) { m_output_constraints = n; }
void node(std::size_t n) { ++m_visited_nodes; m_total_constraints += n; }
void node(std::size_t n) { m_total_constraints += n; }

void eq_conflict() { m_eq_conflict = true; }


static FMplexQEStatistics& get_instance() {
static FMplexQEStatistics & statistics = statistics_get<FMplexQEStatistics>("fm-qe");
static FMQEStatistics& get_instance() {
static FMQEStatistics & statistics = statistics_get<FMQEStatistics>("fm-qe");
return statistics;
}
};
Expand Down
2 changes: 1 addition & 1 deletion src/smtrat-qe/fmplex/FMplexQEStatistics.h
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ class FMplexQEStatistics : public Statistics
std::size_t m_split_tried = 0;
std::size_t m_split_done = 0;
bool m_eq_conflict = false;
carl::statistics::timer m_qe_timer;
carl::statistics::Timer m_qe_timer;


public:
Expand Down
26 changes: 26 additions & 0 deletions src/smtrat-strategies/strategies/CoveringNG/PPSATDefault.h
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
#pragma once

#include <smtrat-modules/CoveringNGModule/CoveringNGModule.h>
#include <smtrat-modules/FPPModule/FPPModule.h>
#include <smtrat-modules/SATModule/SATModule.h>
#include <smtrat-solver/Manager.h>

namespace smtrat {

/**
* The most efficient CoveringNG strategy with preprocessing.
*
*/
class CoveringNG_PPSATDefault: public Manager {
public:
CoveringNG_PPSATDefault() : Manager() {
setStrategy(
addBackend<FPPModule<FPPSettings1>>({
addBackend<SATModule<SATSettings1>>({
addBackend<CoveringNGModule<CoveringNGSettingsDefault>>()
})
})
);
}
};
} // namespace smtrat

0 comments on commit e467513

Please sign in to comment.