Skip to content

Issues with union-atom #302

@rTreutlein

Description

@rTreutlein

I have the following line in my code:

(tracem (u $premises ((CPU $formula ($tv $tve) $ntv) (: $prfelem $elem $tve))) (union-atom ((CPU $formula ($tv $tve) $ntv) (: $prfelem $elem $tve)) $premises))

With the following trace output (formatted nicely by hand):

((u ((CPU and-formula ($69246720 $69246726) $69246642) (: $69246750 b $69246726) (: $69246780 a $69246720)) ;$premises
     ((CPU and-formula ($69246642 $69246672) $69247020) (: $69246660 c $69246672))) ;$stuff to append to $premises
     ((: $69246660 c $69246672) (CPU and-formula ($69246720 $69246726) $69246642) (: $69246750 b $69246726) (: $69246780 a $69246720))) ;$result

Now for some reason there is only one (CPU and-fromula ...) in the output when there should be 2. I can't reproduce it when i just call union-atom in with those inputs in an otherwise empty file. But changing to my own custom union implementation fixes it. So i am guessing soemthing about those internal variables causes the the 2 CPU statments to be unifed resutling in only 1 in the output.

Metadata

Metadata

Assignees

Labels

No labels
No labels

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions