updating assertions

muhos · muhos · commit e49f0009678a · 2025-09-05T11:14:53.000+02:00
diff --git a/src/gpu/assume.cpp b/src/gpu/assume.cpp
@@ -249,7 +249,7 @@ void Solver::iunassume()
 void Solver::idecide()
 {
 	assert(inf.unassigned);
-	assert(sp->propagated == trail.size());
+	assert(isPropagated());
 	assert(conflict == NOREF);
 	assert(UNSOLVED(cnfstate));
 	int level = DL();
diff --git a/src/gpu/cnf.cuh b/src/gpu/cnf.cuh
@@ -96,29 +96,29 @@ namespace ParaFROST {
 			_data.size += SCBUCKETS(src.size());
 
 		}
-		_PFROST_H_D_		void		print		(const uint32& off = 0, const bool& p_ref = true) {
+		_PFROST_H_D_		void		print		(const uint32& off = 0, const bool& p_ref = true) const {
 			for (uint32 i = off; i < size(); i++) {
-				SCLAUSE& c = clause(i);
+				const SCLAUSE& c = clause(i);
 				if (c.size()) {
 					if (p_ref) printf("c  C(%d, r: %lld)->", i, uint64(_refs[i]));
 					else printf("c  C(%d)->", i);
 					c.print();
 				}
 			}
 		}
-		_PFROST_H_D_		void		printAdded	(const uint32& off = 0, const bool& p_ref = true) {
+		_PFROST_H_D_		void		printAdded	(const uint32& off = 0, const bool& p_ref = true) const {
 			for (uint32 i = off; i < size(); i++) {
-				SCLAUSE& c = clause(i);
+				const SCLAUSE& c = clause(i);
 				if (c.size() && c.added()) {
 					if (p_ref) printf("c  C(%d, r: %lld)->", i, uint64(_refs[i]));
 					else printf("c  C(%d)->", i);
 					c.print();
 				}
 			}
 		}
-		_PFROST_H_D_		void		printDeleted(const uint32& off = 0, const bool& p_ref = true) {
+		_PFROST_H_D_		void		printDeleted(const uint32& off = 0, const bool& p_ref = true) const {
 			for (uint32 i = off; i < size(); i++) {
-				SCLAUSE& c = clause(i);
+				const SCLAUSE& c = clause(i);
 				if (c.size() && c.deleted()) {
 					if (p_ref) printf("c  C(%d, r: %lld)->", i, uint64(_refs[i]));
 					else printf("c  C(%d)->", i);
diff --git a/src/gpu/debinary.cpp b/src/gpu/debinary.cpp
@@ -24,7 +24,7 @@ void Solver::debinary() {
 	if (!cnfstate) return;
 	assert(!DL());
 	assert(!wt.empty());
-	assert(sp->propagated == trail.size());
+	assert(isPropagated());
 	stats.debinary.calls++;
 	uVec1D& marked = minimized;
 	int64 subsumed = 0, units = 0;
diff --git a/src/gpu/decide.cpp b/src/gpu/decide.cpp
@@ -63,7 +63,7 @@ uint32 Solver::makeAssign(const uint32& v, const bool& tphase)
 void Solver::decide()
 {
 	assert(inf.unassigned);
-	assert(sp->propagated == trail.size());
+	assert(isPropagated());
 	assert(conflict == NOREF);
 	assert(UNSOLVED(cnfstate));
 	uint32 cand = vsidsEnabled() ? nextVSIDS() : nextVMFQ();
diff --git a/src/gpu/equivalence.cpp b/src/gpu/equivalence.cpp
@@ -42,7 +42,7 @@ bool Solver::decompose()
 {
 	if (!cnfstate) return false;
 	assert(!DL());
-	assert(sp->propagated == trail.size());
+	assert(isPropagated());
 	assert(analyzed.empty());
 	assert(minimized.empty());
 	stats.decompose.calls++;
diff --git a/src/gpu/lcve.cu b/src/gpu/lcve.cu
@@ -132,33 +132,13 @@ void Solver::varReorder()
 bool Solver::LCVE()
 {
 	// reorder variables
-	uint32* evars = vars->eligible;
-	uint32* eend = evars + inf.maxVar;
-	LOGN2(2, " Finding eligible variables for LCVE..");
-	assert(cuhist.d_hist != NULL);
-	// NOTE: OT creation will be synced in calcScores call
-	if (vars->nUnits) calcScores(vars, cuhist.d_hist, ot); // update d_hist & calc scores
-	else calcScores(vars, cuhist.d_hist);
-	cuhist.cacheHist(inf.nDualVars, streams[2]);
-	if (gopts.profile_gpu) cutimer->start(streams[3]);
-	cacher.insert(cumm.scatter(), cumm.scatterCap());
-	thrust::sort(thrust::cuda::par(tca).on(streams[3]), evars, eend, GPU_LCV_CMP(vars->scores));
-	cacher.erase(cumm.scatterCap());
-	LOGDONE(2, 5);
-	vars->nUnits = 0;
-	SYNC(streams[2]);
-	if (gopts.profile_gpu) cutimer->stop(streams[3]), cutimer->vo += cutimer->gpuTime();
-	if (verbose == 4) {
-		LOG0(" Eligible variables:");
-		for (uint32 v = 0; v < inf.maxVar; v++) {
-			uint32 x = evars[v], p = V2L(x), n = NEG(p);
-			LOG1("  e[%d]->(v: %d, p: %d, n: %d, s: %d)", v, x, cuhist[p], cuhist[n], vars->scores[x]);
-		}
-	}
+	varReorder();
 
 	// extended LCVE
 	LOGN2(2, " Electing variables (p-mu: %d, n-mu: %d)..", opts.mu_pos << multiplier, opts.mu_neg << multiplier);
 	sp->stacktail = sp->tmpstack;
+	uint32* evars = vars->eligible;
+	uint32* eend = evars + inf.maxVar;
 	uint32*& tail = sp->stacktail;
 	LIT_ST* frozen = sp->frozen;
 	const uint32 maxoccurs = opts.lcve_max_occurs;
diff --git a/src/gpu/mdm.cpp b/src/gpu/mdm.cpp
@@ -130,7 +130,7 @@ void Solver::MDMInit()
 {
 	if (!last.mdm.rounds) return;
 	assert(inf.unassigned);
-	assert(sp->propagated == trail.size());
+	assert(isPropagated());
 	assert(conflict == NOREF);
 	assert(UNSOLVED(cnfstate));
 	if (opts.mdm_walk_en) {
@@ -207,7 +207,7 @@ void Solver::MDM()
 		return;
 	}
 	assert(inf.unassigned);
-	assert(sp->propagated == trail.size());
+	assert(isPropagated());
 	assert(conflict == NOREF);
 	assert(UNSOLVED(cnfstate));
 	stats.mdm.calls++;
diff --git a/src/gpu/probe.cpp b/src/gpu/probe.cpp
@@ -111,7 +111,7 @@ void Solver::FLE()
 {
 	if (!cnfstate) return;
 	assert(!DL());
-	assert(sp->propagated == trail.size());
+	assert(isPropagated());
 	SLEEPING(sleep.probe, opts.probe_sleep_en);
 	SET_BOUNDS(this, probe_limit, probe, probeticks, searchticks, nlogn(maxActive()));
 	VSTATE* states = sp->vstate;
@@ -137,7 +137,7 @@ void Solver::FLE()
 		{
 			assert(!DL());
 			assert(unassigned(probe));
-			assert(sp->propagated == trail.size());
+			assert(isPropagated());
 			unmarkProbe(probe);
 			if (currfailed && vhist[probe] == currfailed)
 				continue;
@@ -150,7 +150,7 @@ void Solver::FLE()
 			}
 			else {
 				assert(DL() == 1);
-				assert(sp->propagated == trail.size());
+				assert(isPropagated());
 				for (uint32 i = propagated; i < trail.size(); i++)
 					vhist[trail[i]] = currfailed;
 				backtrack();
diff --git a/src/gpu/recycle.cpp b/src/gpu/recycle.cpp
@@ -145,7 +145,7 @@ void Solver::recycle(CMM& new_cm)
 
 void Solver::recycle() 
 {
-	assert(sp->propagated == trail.size());
+	assert(isPropagated());
 	assert(conflict == NOREF);
 	assert(UNSOLVED(cnfstate));
 	shrink();
diff --git a/src/gpu/reduce.cpp b/src/gpu/reduce.cpp
@@ -48,7 +48,7 @@ bool Solver::chronoHasRoot() {
 
 void Solver::reduce()
 {
-	assert(sp->propagated == trail.size());
+	assert(isPropagated());
 	assert(conflict == NOREF);
 	assert(UNSOLVED(cnfstate));
 	assert(learnts.size());
diff --git a/src/gpu/restart.cpp b/src/gpu/restart.cpp
@@ -30,7 +30,7 @@ bool Solver::canRestart()
 
 void Solver::restart()
 {
-	assert(sp->propagated == trail.size());
+	assert(isPropagated());
 	assert(conflict == NOREF);
 	assert(UNSOLVED(cnfstate));
 	stats.restart.all++;
diff --git a/src/gpu/shrink.cpp b/src/gpu/shrink.cpp
@@ -131,7 +131,7 @@ bool Solver::shrink()
 	assert(trail.size());
 	assert(conflict == NOREF);
 	assert(UNSOLVED(cnfstate));
-	assert(sp->propagated == trail.size());
+	assert(isPropagated());
 	assert(!unassigned(trail.back()));
 #ifdef STATISTICS
 	stats.shrink.calls++;
@@ -155,7 +155,7 @@ void Solver::shrinkTop(const bool& conditional)
 	assert(UNSOLVED(cnfstate));
 	assert(conflict == NOREF);
 	assert(UNSOLVED(cnfstate));
-	assert(sp->propagated == trail.size());
+	assert(isPropagated());
 	LOGN2(2, " Shrinking all clauses on top level..");
 	if (sp->simplified < inf.maxFrozen) sp->simplified = inf.maxFrozen;
 #ifdef STATISTICS
diff --git a/src/gpu/simplify.cu b/src/gpu/simplify.cu
@@ -88,7 +88,7 @@ void Solver::awaken()
 {
 	assert(conflict == NOREF);
 	assert(UNSOLVED(cnfstate));
-	assert(sp->propagated == trail.size());
+	assert(isPropagated());
 	initSimplifier();
 	// overapproximate the size of new formula and saved witnesses
 	size_t numCls = maxClauses(), numLits = maxLiterals();
@@ -207,7 +207,7 @@ void Solver::simplifying(const bool& keep_gpu_mem)
 		// one can append them to the trail and continue solving.
 		LOGERROR("unit clauses are pending and reallocation of CNF/OT failed");
 	}
-	assert(sp->propagated == trail.size());
+	assert(isPropagated());
 	cacheEliminated(streams[5]);             	// if ERE is enabled, this transfer would be already done
 	cumm.updateMaxCap(), cacher.updateMaxCap(); // for reporting GPU memory only
 	markEliminated(streams[5]);              	// must be executed before map()
diff --git a/src/gpu/solver.hpp b/src/gpu/solver.hpp
@@ -190,9 +190,10 @@ namespace ParaFROST {
 				|| (termCallback && termCallback(termCallbackState))
 				|| (opts.boundsearch_en && (stats.conflicts >= opts.conflict_out || stats.decisions.single >= opts.decision_out));
 		}
+		inline bool		isPropagated		() const { return sp->propagated == trail.size(); }
 		inline void		rootify				() {
 			assert(UNSOLVED(cnfstate));
-			assert(sp->propagated == trail.size());
+			assert(isPropagated());
 			backtrack();
 			if (BCP()) learnEmpty();
 		}
@@ -523,6 +524,8 @@ namespace ParaFROST {
 			inf.unassigned--;
 			inf.maxSubstituted++;
 		}
+		inline LIT_ST*	getValues			() { return sp->value; }
+		inline int*		getLevels			() { return sp->level; }
 		//==============================================
 		bool			keeping				(CLAUSE&);
 		CL_ST			rooted				(CLAUSE&);
diff --git a/src/gpu/ternary.cpp b/src/gpu/ternary.cpp
@@ -229,7 +229,7 @@ void Solver::ternary()
     if (!canTernary()) return;
     assert(!DL());
     assert(!last.ternary.resolvents);
-    assert(sp->propagated == trail.size());
+    assert(isPropagated());
     SLEEPING(sleep.ternary, opts.ternary_sleep_en);
     stats.ternary.calls++;
     wt.clear(true);
diff --git a/src/gpu/transitive.cpp b/src/gpu/transitive.cpp
@@ -110,7 +110,7 @@ void Solver::transitive()
 	if (!opts.transitive_en) return;
 	assert(probed);
 	assert(!DL());
-	assert(sp->propagated == trail.size());
+	assert(isPropagated());
 	sortWT();
 	SET_BOUNDS(this, limit, transitive, transitiveticks, searchticks, 0);
 	assert(last.transitive.literals < inf.nDualVars);
diff --git a/src/gpu/vivify.cpp b/src/gpu/vivify.cpp
@@ -410,7 +410,7 @@ void Solver::schedule2viv(BCNF& schedule, const bool& tier2, const bool& learnt)
 void Solver::vivifying(const CL_ST& type)
 {
 	assert(!DL());
-	assert(sp->propagated == trail.size());
+	assert(isPropagated());
 	const bool tier2 = ISVIVIFYTIER2(type);
 	const bool learnt = tier2 || ISVIVIFYTIER1(type);
 	BCNF schedule;
diff --git a/src/gpu/walk.cpp b/src/gpu/walk.cpp
@@ -73,7 +73,7 @@ void Solver::walk()
 {
 	assert(!DL());
 	assert(UNSOLVED(cnfstate));
-	assert(sp->propagated == trail.size());
+	assert(isPropagated());
 	stats.walk.calls++;
 	wt.clear(true);
 	shrinkTop(true);

Original file line number	Diff line number	Diff line change
`@@ -249,7 +249,7 @@ void Solver::iunassume()`
`249`	`249`	`void Solver::idecide()`
`250`	`250`	`{`
`251`	`251`	`assert(inf.unassigned);`
`252`		`- assert(sp->propagated == trail.size());`
	`252`	`+ assert(isPropagated());`
`253`	`253`	`assert(conflict == NOREF);`
`254`	`254`	`assert(UNSOLVED(cnfstate));`
`255`	`255`	`int level = DL();`
Original file line number	Diff line number	Diff line change
`@@ -96,29 +96,29 @@ namespace ParaFROST {`
`96`	`96`	`_data.size += SCBUCKETS(src.size());`
`97`	`97`
`98`	`98`	`}`
`99`		`- _PFROST_H_D_ void print (const uint32& off = 0, const bool& p_ref = true) {`
	`99`	`+ _PFROST_H_D_ void print (const uint32& off = 0, const bool& p_ref = true) const {`
`100`	`100`	`for (uint32 i = off; i < size(); i++) {`
`101`		`- SCLAUSE& c = clause(i);`
	`101`	`+ const SCLAUSE& c = clause(i);`
`102`	`102`	`if (c.size()) {`
`103`	`103`	`if (p_ref) printf("c C(%d, r: %lld)->", i, uint64(_refs[i]));`
`104`	`104`	`else printf("c C(%d)->", i);`
`105`	`105`	`c.print();`
`106`	`106`	`}`
`107`	`107`	`}`
`108`	`108`	`}`
`109`		`- _PFROST_H_D_ void printAdded (const uint32& off = 0, const bool& p_ref = true) {`
	`109`	`+ _PFROST_H_D_ void printAdded (const uint32& off = 0, const bool& p_ref = true) const {`
`110`	`110`	`for (uint32 i = off; i < size(); i++) {`
`111`		`- SCLAUSE& c = clause(i);`
	`111`	`+ const SCLAUSE& c = clause(i);`
`112`	`112`	`if (c.size() && c.added()) {`
`113`	`113`	`if (p_ref) printf("c C(%d, r: %lld)->", i, uint64(_refs[i]));`
`114`	`114`	`else printf("c C(%d)->", i);`
`115`	`115`	`c.print();`
`116`	`116`	`}`
`117`	`117`	`}`
`118`	`118`	`}`
`119`		`- _PFROST_H_D_ void printDeleted(const uint32& off = 0, const bool& p_ref = true) {`
	`119`	`+ _PFROST_H_D_ void printDeleted(const uint32& off = 0, const bool& p_ref = true) const {`
`120`	`120`	`for (uint32 i = off; i < size(); i++) {`
`121`		`- SCLAUSE& c = clause(i);`
	`121`	`+ const SCLAUSE& c = clause(i);`
`122`	`122`	`if (c.size() && c.deleted()) {`
`123`	`123`	`if (p_ref) printf("c C(%d, r: %lld)->", i, uint64(_refs[i]));`
`124`	`124`	`else printf("c C(%d)->", i);`
Original file line number	Diff line number	Diff line change
`@@ -63,7 +63,7 @@ uint32 Solver::makeAssign(const uint32& v, const bool& tphase)`
`63`	`63`	`void Solver::decide()`
`64`	`64`	`{`
`65`	`65`	`assert(inf.unassigned);`
`66`		`- assert(sp->propagated == trail.size());`
	`66`	`+ assert(isPropagated());`
`67`	`67`	`assert(conflict == NOREF);`
`68`	`68`	`assert(UNSOLVED(cnfstate));`
`69`	`69`	`uint32 cand = vsidsEnabled() ? nextVSIDS() : nextVMFQ();`
Original file line number	Diff line number	Diff line change
`@@ -42,7 +42,7 @@ bool Solver::decompose()`
`42`	`42`	`{`
`43`	`43`	`if (!cnfstate) return false;`
`44`	`44`	`assert(!DL());`
`45`		`- assert(sp->propagated == trail.size());`
	`45`	`+ assert(isPropagated());`
`46`	`46`	`assert(analyzed.empty());`
`47`	`47`	`assert(minimized.empty());`
`48`	`48`	`stats.decompose.calls++;`
Original file line number	Diff line number	Diff line change
`@@ -145,7 +145,7 @@ void Solver::recycle(CMM& new_cm)`
`145`	`145`
`146`	`146`	`void Solver::recycle()`
`147`	`147`	`{`
`148`		`- assert(sp->propagated == trail.size());`
	`148`	`+ assert(isPropagated());`
`149`	`149`	`assert(conflict == NOREF);`
`150`	`150`	`assert(UNSOLVED(cnfstate));`
`151`	`151`	`shrink();`
Original file line number	Diff line number	Diff line change
`@@ -48,7 +48,7 @@ bool Solver::chronoHasRoot() {`
`48`	`48`
`49`	`49`	`void Solver::reduce()`
`50`	`50`	`{`
`51`		`- assert(sp->propagated == trail.size());`
	`51`	`+ assert(isPropagated());`
`52`	`52`	`assert(conflict == NOREF);`
`53`	`53`	`assert(UNSOLVED(cnfstate));`
`54`	`54`	`assert(learnts.size());`