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

#ifndef MAXPP_AMSLEX_HPP
#define MAXPP_AMSLEX_HPP

#include <vector>
#include <map>

#include "probleminstance.hpp"
#include "timer.hpp"

namespace maxPreprocessor{
class AMSLEX{
private:
	std::vector<int> ALU;
	std::vector<int> ALI;
	int ALIt;
	std::vector<int> ALF;
	const unsigned BSconst = 18; // magic constant
	
	struct vecP {
		unsigned B, E, O;
		unsigned size() const {
			return E - B;
		}
	};
	
	int* data;
	unsigned dataSize;
	const ProblemInstance& pi;
	bool isPrefix(const std::vector<int>& a, const std::vector<int>& b);
	bool isPrefix(vecP a, vecP b);
	void assumeSize(unsigned size);
	bool CSO1(const std::vector<vecP>& D, unsigned b, unsigned e, const vecP S, 
					   unsigned j, unsigned d, const std::vector<int>& d0Index);
	bool CSO2(const std::vector<int>& D, unsigned b, unsigned e, const std::vector<int>& S, unsigned j, unsigned d);
	std::vector<int> amsLexSEPerm(const std::vector<int>& clauses);
	std::vector<int> amsLexSENonPerm(const std::vector<int>& clauses);
	std::pair<std::vector<int>, std::vector<int> > amsLexSSRPerm(const std::vector<int>& c1, const std::vector<int>& c2, int var);
public:
	AMSLEX(const ProblemInstance& pi_);
	~AMSLEX();
	
	std::vector<int> amsLexSE(const std::vector<int>& clauses);
	std::pair<std::vector<int>, std::vector<int> > amsLexSSR(const std::vector<int>& c1, const std::vector<int>& c2, int var);
};
}
#endif