forked from karpiu/kp-minisatp
-
Notifications
You must be signed in to change notification settings - Fork 3
/
minisat.patch
99 lines (86 loc) · 4.57 KB
/
minisat.patch
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
96
97
98
99
diff -urB minisat/minisat/core/Solver.h minisat-new/minisat/core/Solver.h
--- minisat/minisat/core/Solver.h 2023-03-18 08:36:56.778969414 +0100
+++ minisat-new/minisat/core/Solver.h 2023-03-16 10:45:53.000000000 +0100
@@ -110,6 +110,10 @@
void budgetOff();
void interrupt(); // Trigger a (potentially asynchronous) interruption of the solver.
void clearInterrupt(); // Clear interrupt indicator flag.
+ // IPASIR:
+ //
+ inline void setTermCallback(void *state, int (*termCallback)(void *));
+
// Memory managment:
//
@@ -236,6 +240,10 @@
int64_t propagation_budget; // -1 means no budget.
bool asynch_interrupt;
+ // IPASIR data
+ void *termCallbackState;
+ int (*termCallback)(void *state);
+
// Main internal methods:
//
void insertVarOrder (Var x); // Insert a variable in the decision order priority queue.
@@ -374,7 +382,8 @@
inline bool Solver::withinBudget() const {
return !asynch_interrupt &&
(conflict_budget < 0 || conflicts < (uint64_t)conflict_budget) &&
- (propagation_budget < 0 || propagations < (uint64_t)propagation_budget); }
+ (propagation_budget < 0 || propagations < (uint64_t)propagation_budget) &&
+ (termCallback == 0 || 0 == termCallback(termCallbackState)); }
// FIXME: after the introduction of asynchronous interrruptions the solve-versions that return a
// pure bool do not give a safe interface. Either interrupts must be possible to turn off here, or
@@ -398,6 +407,9 @@
inline void Solver::toDimacs (const char* file, Lit p, Lit q){ vec<Lit> as; as.push(p); as.push(q); toDimacs(file, as); }
inline void Solver::toDimacs (const char* file, Lit p, Lit q, Lit r){ vec<Lit> as; as.push(p); as.push(q); as.push(r); toDimacs(file, as); }
+// IPASIR
+void Solver::setTermCallback(void *state, int (*termcallback)(void *)) {
+ termCallbackState = state; termCallback = termcallback; }
//=================================================================================================
// Debug etc:
diff -urB minisat/minisat/core/SolverTypes.h minisat-new/minisat/core/SolverTypes.h
--- minisat/minisat/core/SolverTypes.h 2023-03-18 08:36:56.778969414 +0100
+++ minisat-new/minisat/core/SolverTypes.h 2023-03-16 10:31:54.000000000 +0100
@@ -52,7 +52,7 @@
int x;
// Use this as a constructor:
- friend Lit mkLit(Var var, bool sign = false);
+ friend Lit mkLit(Var var, bool sign);
bool operator == (Lit p) const { return x == p.x; }
bool operator != (Lit p) const { return x != p.x; }
@@ -60,7 +60,7 @@
};
-inline Lit mkLit (Var var, bool sign) { Lit p; p.x = var + var + (int)sign; return p; }
+inline Lit mkLit (Var var, bool sign = false) { Lit p; p.x = var + var + (int)sign; return p; }
inline Lit operator ~(Lit p) { Lit q; q.x = p.x ^ 1; return q; }
inline Lit operator ^(Lit p, bool b) { Lit q; q.x = p.x ^ (unsigned int)b; return q; }
inline bool sign (Lit p) { return p.x & 1; }
diff -urB minisat/minisat/mtl/IntMap.h minisat-new/minisat/mtl/IntMap.h
--- minisat/minisat/mtl/IntMap.h 2023-03-18 08:36:56.778969414 +0100
+++ minisat-new/minisat/mtl/IntMap.h 2023-03-16 13:28:55.000000000 +0100
@@ -83,6 +83,7 @@
void insert (K k) { in_set.reserve(k, 0); if (!in_set[k]) { in_set[k] = 1; xs.push(k); } }
bool has (K k) { in_set.reserve(k, 0); return in_set[k]; }
+ void copyTo (vec<K>& to) { to.clear(); for (int i = 0; i < size() ; i++) if (in_set[xs[i]]) to.push(xs[i]); }
};
#if 0
diff -urB minisat/minisat/utils/Options.h minisat-new/minisat/utils/Options.h
--- minisat/minisat/utils/Options.h 2023-03-18 08:36:56.782969458 +0100
+++ minisat-new/minisat/utils/Options.h 2023-03-16 10:57:14.000000000 +0100
@@ -282,15 +282,15 @@
if (range.begin == INT64_MIN)
fprintf(stderr, "imin");
else
- fprintf(stderr, "%4"PRIi64, range.begin);
+ fprintf(stderr, "%4" PRIi64, range.begin);
fprintf(stderr, " .. ");
if (range.end == INT64_MAX)
fprintf(stderr, "imax");
else
- fprintf(stderr, "%4"PRIi64, range.end);
+ fprintf(stderr, "%4" PRIi64, range.end);
- fprintf(stderr, "] (default: %"PRIi64")\n", value);
+ fprintf(stderr, "] (default: %" PRIi64")\n", value);
if (verbose){
fprintf(stderr, "\n %s\n", description);
fprintf(stderr, "\n");