Skip to content

GitLab

  • Menu
Projects Groups Snippets
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • C cduce
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 15
    • Issues 15
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 3
    • Merge requests 3
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Environments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • cduce
  • cduce
  • Issues
  • #13

Closed
Open
Created Apr 01, 2016 by Tommaso Petrucciani@petruccianiDeveloper

Tallying: failure in recursive calls inside merge make the whole merge fail

Currently Type_tallying.merge raises an exception if a constraint set is unsolvable. This exception is handled by Type_tallying.type_tallying but not by merge itself. Thus, if a recursive call inside merge fails, the whole call fails.

In particular, tallying fails on the constraint set

'a <= 'b -> 'c
1 <= 'b
'a -> 'c <= ('f -> 'f) -> 'e

(which admits a solution 'a := (1 -> 1), other variables := 1).

Test with

debug tallying [] ( 'a , ( 1 , ('a -> 'c) ) ) ( ('b -> 'c), ( 'b , (('f -> 'f) -> 1) ) );;

(here tallying finds only the solution 'a := Empty and not the other one).

Normalization generates two constraints, one for 'a := Empty, the other

{ 'f -> 'f <= 'a <= 'b -> 'c, 1 <= 'b <= Any, Empty <= 'c <= 1 }

which is not solved correctly. In merge, the contraint 'f -> 'f <= 'b -> 'c is generated and normalised into

{ { Empty <= 'b <= 'f, 'f <= 'c <= Any }, { Empty <= 'b <= Empty } }

only the first of which is solvable (since 1 <= 'b, 'b <= Empty is impossible). The case 'b <= Empty is considered first and merge fails completely instead of considering the other case.

Replacing line 605

let m1' = merge delta cache m1 in

with

let m1' = try merge delta cache m1 with UnSatConstr _ -> ConstrSet.unsat in

solves this. I'm not sure if it breaks anything else, but it seems to be what the specification of tallying says (the recursive calls are in union with each other, so empty sets are ignored).

Edited May 02, 2021 by Kim Nguyễn
Assignee
Assign to
Time tracking