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

#ifndef MAXPP_TOUCHEDLIST_HPP
#define MAXPP_TOUCHEDLIST_HPP
#include <vector>
#include <deque>
#include <cstdint>
#include <map>
#include <string>

namespace maxPreprocessor {
class ProblemInstance;

class TouchedList {
private:
	std::deque<std::pair<uint64_t, int> > touchedLiterals;
	std::deque<std::pair<uint64_t, int> > modLiterals;
	std::deque<std::pair<uint64_t, int> > touchedClauses;
	std::deque<std::pair<uint64_t, int> > modClauses;
	std::map<std::string, uint64_t> techniqueItr;
	void getTouchedLiteralsCh(uint64_t eitr, std::vector<int>& ret);
	void getModLiteralsCh(uint64_t eitr, std::vector<int>& ret);
	void getTouchedVarsCh(uint64_t eitr, std::vector<int>& ret);
	void getModVarsCh(uint64_t eitr, std::vector<int>& ret);
	std::vector<int> getI;
	uint64_t itr;
	uint64_t frontItr;
	int getItr;
	int vars;
	const ProblemInstance& pi;
public:
	TouchedList(const ProblemInstance& pi_);
	void init(int vars_);
	
	void shrink(bool log);
	
	void addVar();
	void modClause(int c);
	void modLiteral(int l);
	void touchClause(int c);
	void touchLiteral(int l);
	
	void setItr(std::string technique);
	
	std::vector<int> getModClauses(std::string technique);
	std::vector<int> getModLiterals(std::string technique);
	std::vector<int> getModVariables(std::string technique);
	std::vector<int> getTouchedLiterals(std::string technique);
	std::vector<int> getTouchedVariables(std::string technique);
	std::vector<int> getBinaryLiterals(std::string technique);
};
}

#endif