-
Notifications
You must be signed in to change notification settings - Fork 2
/
IncrementalData.h
41 lines (34 loc) · 1.47 KB
/
IncrementalData.h
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
#ifndef INCREMENTALDATA_H
#define INCREMENTALDATA_H
#include <cstdint>
#include "clausedatabase.h"
class IncrementalData
{
private:
IncrementalData(const IncrementalData& other) = delete;
virtual bool operator==(const IncrementalData& other) const;
public:
IncrementalData();
virtual ~IncrementalData();
virtual void encodeNewGeq(int64_t newGeq, ClauseDatabase & formula, AuxVarManager & auxVars, std::vector< int32_t > conditionals) = 0;
virtual void encodeNewLeq(int64_t newLeq, ClauseDatabase & formula, AuxVarManager & auxVars, std::vector< int32_t > conditionals) = 0;
};
class IncrementalDontCare : public IncrementalData
{
public:
virtual void encodeNewGeq(int64_t newGeq, ClauseDatabase& formula, AuxVarManager& auxVars, std::vector< int32_t > conditionals);
virtual void encodeNewLeq(int64_t newLeq, ClauseDatabase& formula, AuxVarManager& auxVars, std::vector< int32_t > conditionals);
IncrementalDontCare();
virtual ~IncrementalDontCare();
};
class AMOIncrementalData : public IncrementalData
{
private:
std::vector<int32_t> geqOneClause;
public:
virtual void encodeNewGeq(int64_t newGeq, ClauseDatabase& formula, AuxVarManager& auxVars, std::vector< int32_t > conditionals);
virtual void encodeNewLeq(int64_t newLeq, ClauseDatabase& formula, AuxVarManager& auxVars, std::vector< int32_t > conditionals);
AMOIncrementalData (std::vector<int32_t> & geqOneClause);
virtual ~AMOIncrementalData ();
};
#endif // INCREMENTALDATA_H