miniBDD test: support lselect

tautschnig · tautschnig · commit 52cc55517b05 · 2023-11-01T20:21:05.000Z
We can support the select operation, it just wasn't implemented.
diff --git a/unit/solvers/bdd/miniBDD/miniBDD.cpp b/unit/solvers/bdd/miniBDD/miniBDD.cpp
@@ -126,10 +126,9 @@ class bdd_propt : public propt
     return {};
   }
 
-  literalt lselect(literalt, literalt, literalt) override
+  literalt lselect(literalt c, literalt t, literalt f) override
   {
-    UNREACHABLE;
-    return {};
+    return to_literal((to_bdd(!c) | to_bdd(t)) & (to_bdd(c) | to_bdd(f)));
   }
 
   void lcnf(const bvt &) override

Original file line number	Diff line number	Diff line change
`@@ -126,10 +126,9 @@ class bdd_propt : public propt`
`126`	`126`	`return {};`
`127`	`127`	`}`
`128`	`128`
`129`		`- literalt lselect(literalt, literalt, literalt) override`
	`129`	`+ literalt lselect(literalt c, literalt t, literalt f) override`
`130`	`130`	`{`
`131`		`- UNREACHABLE;`
`132`		`- return {};`
	`131`	`+ return to_literal((to_bdd(!c) \| to_bdd(t)) & (to_bdd(c) \| to_bdd(f)));`
`133`	`132`	`}`
`134`	`133`
`135`	`134`	`void lcnf(const bvt &) override`