@@ -199,6 +199,15 @@ fn log_bits(x: usize) -> usize {
199199}
200200
201201fn sat_at_most_one ( solver : & mut impl varisat:: ExtendFormula , vars : & [ varisat:: Var ] ) {
202+ if vars. len ( ) <= 1 {
203+ return ;
204+ } else if vars. len ( ) == 2 {
205+ solver. add_clause ( & [ vars[ 0 ] . negative ( ) , vars[ 1 ] . negative ( ) ] ) ;
206+ } else if vars. len ( ) == 3 {
207+ solver. add_clause ( & [ vars[ 0 ] . negative ( ) , vars[ 1 ] . negative ( ) ] ) ;
208+ solver. add_clause ( & [ vars[ 0 ] . negative ( ) , vars[ 2 ] . negative ( ) ] ) ;
209+ solver. add_clause ( & [ vars[ 1 ] . negative ( ) , vars[ 2 ] . negative ( ) ] ) ;
210+ }
202211 // use the "Binary Encoding" from
203212 // https://www.it.uu.se/research/group/astra/ModRef10/papers/Alan%20M.%20Frisch%20and%20Paul%20A.%20Giannoros.%20SAT%20Encodings%20of%20the%20At-Most-k%20Constraint%20-%20ModRef%202010.pdf
204213 let bits: Vec < varisat:: Var > = solver. new_var_iter ( log_bits ( vars. len ( ) ) ) . collect ( ) ;
@@ -229,8 +238,7 @@ impl SatResolve {
229238 let mut solver = varisat:: Solver :: new ( ) ;
230239 let var_for_is_packages_used: HashMap < PackageId , varisat:: Var > = registry
231240 . iter ( )
232- . map ( |s| s. package_id ( ) )
233- . zip ( solver. new_var_iter ( registry. len ( ) ) )
241+ . map ( |s| ( s. package_id ( ) , solver. new_var ( ) ) )
234242 . collect ( ) ;
235243
236244 // no two packages with the same links set
@@ -270,23 +278,113 @@ impl SatResolve {
270278
271279 let empty_vec = vec ! [ ] ;
272280
281+ let mut version_selected_for: HashMap <
282+ ( PackageId , Dependency ) ,
283+ HashMap < PackageId , varisat:: Var > ,
284+ > = HashMap :: new ( ) ;
273285 // active packages need each of there `deps` to be satisfied
274286 for p in registry. iter ( ) {
275287 for dep in p. dependencies ( ) {
276- let mut matches : Vec < varisat:: Lit > = by_name
288+ let version : HashMap < PackageId , varisat:: Var > = by_name
277289 . get ( dep. package_name ( ) . as_str ( ) )
278290 . unwrap_or ( & empty_vec)
279291 . iter ( )
280292 . filter ( |& p| dep. matches_id ( * p) )
281- . map ( |p| var_for_is_packages_used[ & p] . positive ( ) )
293+ . map ( |& p| ( p, solver. new_var ( ) ) )
294+ . collect ( ) ;
295+ // if `p` is active then we need to select one of the versions
296+ let matches: Vec < _ > = version
297+ . values ( )
298+ . map ( |v| v. positive ( ) )
299+ . chain ( Some ( var_for_is_packages_used[ & p. package_id ( ) ] . negative ( ) ) )
282300 . collect ( ) ;
283- // ^ the `dep` is satisfied or `p` is not active
284- matches. push ( var_for_is_packages_used[ & p. package_id ( ) ] . negative ( ) ) ;
285301 solver. add_clause ( & matches) ;
302+ for ( pid, var) in version. iter ( ) {
303+ // if a version is selected then it needs to be activated
304+ solver. add_clause ( & [ var. negative ( ) , var_for_is_packages_used[ pid] . positive ( ) ] ) ;
305+ }
306+ version_selected_for. insert ( ( p. package_id ( ) , dep. clone ( ) ) , version) ;
286307 }
287308 }
288309
289- // TODO: public & private deps
310+ let publicly_exports: HashMap < PackageId , HashMap < PackageId , varisat:: Var > > = registry
311+ . iter ( )
312+ . map ( |s| {
313+ (
314+ s. package_id ( ) ,
315+ registry
316+ . iter ( )
317+ . map ( |s| ( s. package_id ( ) , solver. new_var ( ) ) )
318+ . collect ( ) ,
319+ )
320+ } )
321+ . collect ( ) ;
322+
323+ for s in registry. iter ( ) {
324+ // everything publicly depends on itself
325+ solver. add_clause ( & [ publicly_exports[ & s. package_id ( ) ] [ & s. package_id ( ) ] . positive ( ) ] ) ;
326+ }
327+
328+ // if a `dep` is public then `p` `publicly_exports` all the things that the selected version `publicly_exports`
329+ for p in registry. iter ( ) {
330+ for dep in p. dependencies ( ) . iter ( ) . filter ( |d| d. is_public ( ) ) {
331+ for ( ver, sel) in version_selected_for[ & ( p. package_id ( ) , dep. clone ( ) ) ] . iter ( ) {
332+ for export in registry. iter ( ) {
333+ solver. add_clause ( & [
334+ sel. negative ( ) ,
335+ publicly_exports[ ver] [ & export. package_id ( ) ] . negative ( ) ,
336+ publicly_exports[ & p. package_id ( ) ] [ & export. package_id ( ) ] . positive ( ) ,
337+ ] ) ;
338+ }
339+ }
340+ }
341+ }
342+
343+ let can_see: HashMap < PackageId , HashMap < PackageId , varisat:: Var > > = registry
344+ . iter ( )
345+ . map ( |s| {
346+ (
347+ s. package_id ( ) ,
348+ registry
349+ . iter ( )
350+ . map ( |s| ( s. package_id ( ) , solver. new_var ( ) ) )
351+ . collect ( ) ,
352+ )
353+ } )
354+ . collect ( ) ;
355+
356+ // if `p` `publicly_exports` `export` then it `can_see` `export`
357+ for p in registry. iter ( ) {
358+ for export in registry. iter ( ) {
359+ solver. add_clause ( & [
360+ publicly_exports[ & p. package_id ( ) ] [ & export. package_id ( ) ] . negative ( ) ,
361+ can_see[ & p. package_id ( ) ] [ & export. package_id ( ) ] . positive ( ) ,
362+ ] ) ;
363+ }
364+ }
365+
366+ // if `p` has a `dep` that selected `ver` then it `can_see` all the things that the selected version `publicly_exports`
367+ for p in registry. iter ( ) {
368+ for dep in p. dependencies ( ) . iter ( ) {
369+ for ( ver, sel) in version_selected_for[ & ( p. package_id ( ) , dep. clone ( ) ) ] . iter ( ) {
370+ for export in registry. iter ( ) {
371+ solver. add_clause ( & [
372+ sel. negative ( ) ,
373+ publicly_exports[ ver] [ & export. package_id ( ) ] . negative ( ) ,
374+ can_see[ & p. package_id ( ) ] [ & export. package_id ( ) ] . positive ( ) ,
375+ ] ) ;
376+ }
377+ }
378+ }
379+ }
380+
381+ // a package `can_see` only one version by each name
382+ for ( _, see) in can_see. iter ( ) {
383+ for ( _, vers) in by_name. iter ( ) {
384+ let same_name: Vec < _ > = vers. iter ( ) . map ( |p| see[ p] ) . collect ( ) ;
385+ sat_at_most_one ( & mut solver, & same_name) ;
386+ }
387+ }
290388
291389 SatResolve {
292390 solver,
@@ -686,7 +784,7 @@ pub fn registry_strategy(
686784 // => Kind::Development, // Development has no impact so don't gen
687785 _ => panic ! ( "bad index for Kind" ) ,
688786 } ,
689- p,
787+ p && k == 0 ,
690788 ) )
691789 }
692790
0 commit comments