-
Notifications
You must be signed in to change notification settings - Fork 2
/
IncSimplePBConstraint.cpp
97 lines (75 loc) · 2.56 KB
/
IncSimplePBConstraint.cpp
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
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
#include "IncSimplePBConstraint.h"
using namespace PBLib;
using namespace std;
IncSimplePBConstraint::IncSimplePBConstraint(int64_t max_sum, int64_t max_weight, int64_t normalizedOffset, PBTYPE type, vector< WeightedLit >& literals, Comparator comparator, int64_t less_eq, int64_t greater_eq): SimplePBConstraint(max_sum, max_weight, type, literals, comparator, less_eq, greater_eq)
{
this->normalized_offset = normalizedOffset;
init_leq = less_eq;
init_geq = greater_eq;
}
IncSimplePBConstraint::IncSimplePBConstraint(int64_t max_sum, int64_t max_weight,int64_t normalizedOffset, PBTYPE type, vector< WeightedLit >& literals, Comparator comparator, int64_t bound): SimplePBConstraint(max_sum, max_weight,type, literals, comparator, bound)
{
this->normalized_offset = normalizedOffset;
assert(comparator == LEQ);
init_leq = bound;
init_geq = 0;
}
void IncSimplePBConstraint::encodeNewGeq(int64_t newGeq, ClauseDatabase& formula, AuxVarManager& auxVars)
{
assert(comparator == BOTH);
geq = newGeq + normalized_offset; // add the offset from the normalization to the new bound
if (geq <= init_geq)
{
geq = init_geq;
return;
}
if ((leq < geq))
{
formula.addConditionals(conditionals);
formula.addUnsat();
for (int i = 0; i < conditionals.size(); ++i)
formula.getConditionals().pop_back();
return;
}
if (geq <= 0)
return;
incremental_data->encodeNewGeq(geq, formula, auxVars, conditionals);
}
void IncSimplePBConstraint::encodeNewLeq(int64_t newLeq, ClauseDatabase& formula, AuxVarManager& auxVars)
{
leq = newLeq + normalized_offset; // add the offset from the normalization to the new bound
if (leq >= init_leq)
{
leq = init_leq;
return;
}
// check if constraint became trivial
if (leq < 0 || (leq < geq))
{
formula.addConditionals(conditionals);
formula.addUnsat();
for (int i = 0; i < conditionals.size(); ++i)
formula.getConditionals().pop_back();
return;
}
else if (leq == 0)
{
// set all literals to false to satisfied == 0
for (int i = 0; i < (int)weighted_literals.size(); ++i)
{
formula.addConditionals(conditionals);
formula.addClause(-weighted_literals[i].lit);
for (int i = 0; i < conditionals.size(); ++i)
formula.getConditionals().pop_back();
}
return;
}
incremental_data->encodeNewLeq(leq, formula, auxVars, conditionals);
}
void IncSimplePBConstraint::setIncrementalData(shared_ptr< IncrementalData > incrementalData)
{
incremental_data = incrementalData;
}
IncSimplePBConstraint::~IncSimplePBConstraint()
{
}