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

#ifndef MAXPP_TRACE_HPP
#define MAXPP_TRACE_HPP

#include <vector>
#include <iostream>
#include <cstdint>

namespace maxPreprocessor {
class Trace {
public:
	std::vector<uint64_t> removedWeight;
	std::vector<int> operations;
	std::vector<std::vector<int> > data;

	void setVar(int var, bool value);
	void BVE(int var, const std::vector<std::vector<int> >& nClauses);
	void BCE(int lit, const std::vector<int>& clause);
	void BCR(int lbl1, int lbl2, const std::vector<std::vector<int> >& nClauses);
	void setEqual(int lit1, int lit2);
	void LS(int lbl, int lit, const std::vector<int>& clause);
	void labelEliminate(int lbl1, int lbl2, int tautli);
	void removeWeight(uint64_t weight, int objective);
	void removeWeight(const std::vector<uint64_t>& weight);
	std::pair<std::vector<int>, uint64_t> getSolution(const std::vector<int>& trueLits, uint64_t weight, int vars, int originalVars);
	std::vector<int> getFixed();
	void printSolution(std::ostream& output, const std::vector<int>& trueLits, uint64_t weight, int vars, int originalVars, int outputFormat);
	void setNbObjectives(int n);
};
}
#endif