Fix wrong behavior on true assumption in satcheck_minisat2

peterschrammel · peterschrammel · commit 0f79d7935c29 · 2019-06-18T11:29:18.000+01:00
A true assumption literal shall have no effect,
whereas it, until now, disabled the assumptions.
diff --git a/src/solvers/sat/satcheck_minisat2.cpp b/src/solvers/sat/satcheck_minisat2.cpp
@@ -328,14 +328,16 @@ bool satcheck_minisat2_baset<T>::is_in_conflict(literalt a) const
 template<typename T>
 void satcheck_minisat2_baset<T>::set_assumptions(const bvt &bv)
 {
-  assumptions=bv;
-
-  forall_literals(it, assumptions)
-    if(it->is_true())
+  // We filter out 'true' assumptions which cause an assertion violation
+  // in Minisat2.
+  assumptions.clear();
+  for(const auto &assumption : bv)
+  {
+    if(!assumption.is_true())
     {
-      assumptions.clear();
-      break;
+      assumptions.push_back(assumption);
     }
+  }
 }
 
 satcheck_minisat_no_simplifiert::satcheck_minisat_no_simplifiert(

Original file line number	Diff line number	Diff line change
`@@ -328,14 +328,16 @@ bool satcheck_minisat2_baset<T>::is_in_conflict(literalt a) const`
`328`	`328`	`template<typename T>`
`329`	`329`	`void satcheck_minisat2_baset<T>::set_assumptions(const bvt &bv)`
`330`	`330`	`{`
`331`		`- assumptions=bv;`
`332`		`-`
`333`		`- forall_literals(it, assumptions)`
`334`		`- if(it->is_true())`
	`331`	`+ // We filter out 'true' assumptions which cause an assertion violation`
	`332`	`+ // in Minisat2.`
	`333`	`+ assumptions.clear();`
	`334`	`+ for(const auto &assumption : bv)`
	`335`	`+ {`
	`336`	`+ if(!assumption.is_true())`
`335`	`337`	`{`
`336`		`- assumptions.clear();`
`337`		`- break;`
	`338`	`+ assumptions.push_back(assumption);`
`338`	`339`	`}`
	`340`	`+ }`
`339`	`341`	`}`
`340`	`342`
`341`	`343`	`satcheck_minisat_no_simplifiert::satcheck_minisat_no_simplifiert(`