maxpre 0.2.5

Rust bindings for the (MO-)MaxSAT preprocessor MaxPre
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57

#ifndef MAXPP_LOG_HPP
#define MAXPP_LOG_HPP

#include <iostream>
#include <cstdint>

#include "timer.hpp"

namespace maxPreprocessor {
class LogT {
public:
	int rClauses, rVariables, rLiterals, rLabels;
	LogT();
	void print(std::ostream& out);
};

class Log {
public:
	enum Technique {none, BCE, UP, BVE, SE, SSR, SLE, BCR, SIE, EE, BVA, GSLE, FLP, UH, LS, AM1, TMS, BBTMS, LRED, CRED, MRED, URED, HARD, FLE};
	std::vector<double> eTime;
	std::vector<double> tTimeLimit;
	std::vector<Technique> askHistory;
	const double infTime = 1e9;
	double toReallocate;
	double timeLimit;
	Technique activeTechnique;
	Timer totalTimer;
	std::vector<LogT> tLog;
	std::vector<Timer> tTimer;
	int gatesExtracted;
	int labelsMatched;
	int binaryCoresFound;
	Log();
	Technique charToTechnique(char t);
	void startTechnique(Technique t);
	void stopTechnique(Technique t);
	void removeClause(int c);
	void removeVariable(int c);
	void removeLiteral(int c);
	void removeLabel(int c);
	void print(std::ostream& out);
	double getTime(Technique t);
	void startTimer();
	void stopTimer();
	void timePlan(double timeLimit_, std::string useTechniques);
	bool requestTime(Technique t);
	double allocatedTimeLeft(Technique t);
	void newRequest(Technique t);
	void neverAgain(char t);
	bool isTimeLimit();
	void printTime(std::ostream& out);
	void printInfo(std::ostream& out);
	std::vector<uint64_t> initialWeightRange;
	std::vector<uint64_t> weightRange;
};
}
#endif